[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
C : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
H_zero : C 0
H_basic : ∀ (i : ι) (x : β i), C (↑(of β i) x)
H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)
⊢ C x
[PROOFSTEP]
apply DFinsupp.induction x H_zero
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
C : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
H_zero : C 0
H_basic : ∀ (i : ι) (x : β i), C (↑(of β i) x)
H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)
⊢ ∀ (i : ι) (b : (fun i => β i) i) (f : Π₀ (i : ι), (fun i => β i) i),
    ↑f i = 0 → b ≠ 0 → C f → C (DFinsupp.single i b + f)
[PROOFSTEP]
intro i b f h1 h2 ih
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
C : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
H_zero : C 0
H_basic : ∀ (i : ι) (x : β i), C (↑(of β i) x)
H_plus : ∀ (x y : ⨁ (i : ι), β i), C x → C y → C (x + y)
i : ι
b : β i
f : Π₀ (i : ι), (fun i => β i) i
h1 : ↑f i = 0
h2 : b ≠ 0
ih : C f
⊢ C (DFinsupp.single i b + f)
[PROOFSTEP]
solve_by_elim
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ↑ψ f = ↑(toAddMonoid fun i => AddMonoidHom.comp ψ (of β i)) f
[PROOFSTEP]
congr
  -- Porting note: ext applies addHom_ext' here, which isn't what we want.
[GOAL]
case e_a
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ψ = toAddMonoid fun i => AddMonoidHom.comp ψ (of β i)
[PROOFSTEP]
apply DFinsupp.addHom_ext'
[GOAL]
case e_a.H
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ∀ (x : ι),
    AddMonoidHom.comp ψ (DFinsupp.singleAddHom (fun i => (fun i => β i) i) x) =
      AddMonoidHom.comp (toAddMonoid fun i => AddMonoidHom.comp ψ (of β i))
        (DFinsupp.singleAddHom (fun i => (fun i => β i) i) x)
[PROOFSTEP]
simp [toAddMonoid, of]
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
⊢ ↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f) = AddMonoidHom.comp (of β i) f
[PROOFSTEP]
rw [fromAddMonoid, toAddMonoid_of]
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
⊢ ↑(↑AddMonoidHom.compHom (of β i)) f = AddMonoidHom.comp (of β i) f
[PROOFSTEP]
rfl
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
x : γ
⊢ ↑(↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f)) x = ↑(of β i) (↑f x)
[PROOFSTEP]
rw [fromAddMonoid_of, AddMonoidHom.coe_comp, Function.comp]
[GOAL]
ι✝ : Type v
dec_ι : DecidableEq ι✝
β : ι✝ → Type w
inst✝³ : (i : ι✝) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type v
ι : optParam (Type u_1) PUnit
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
src✝ : (⨁ (i : ι), M) →+ M := toAddMonoid fun x => AddMonoidHom.id M
x : ⨁ (x : ι), M
⊢ ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) 0) = 0
[PROOFSTEP]
rw [AddMonoidHom.map_zero, AddMonoidHom.map_zero]
[GOAL]
ι✝ : Type v
dec_ι : DecidableEq ι✝
β : ι✝ → Type w
inst✝³ : (i : ι✝) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type v
ι : optParam (Type u_1) PUnit
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
src✝ : (⨁ (i : ι), M) →+ M := toAddMonoid fun x => AddMonoidHom.id M
x✝ : ⨁ (x : ι), M
p : ι
x : M
⊢ ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (↑(of (fun i => M) p) x)) =
    ↑(of (fun i => M) p) x
[PROOFSTEP]
rw [Unique.default_eq p, toAddMonoid_of]
[GOAL]
ι✝ : Type v
dec_ι : DecidableEq ι✝
β : ι✝ → Type w
inst✝³ : (i : ι✝) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type v
ι : optParam (Type u_1) PUnit
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
src✝ : (⨁ (i : ι), M) →+ M := toAddMonoid fun x => AddMonoidHom.id M
x✝ : ⨁ (x : ι), M
p : ι
x : M
⊢ ↑(of (fun x => M) p) (↑(AddMonoidHom.id M) x) = ↑(of (fun i => M) p) x
[PROOFSTEP]
rfl
[GOAL]
ι✝ : Type v
dec_ι : DecidableEq ι✝
β : ι✝ → Type w
inst✝³ : (i : ι✝) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type v
ι : optParam (Type u_1) PUnit
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
src✝ : (⨁ (i : ι), M) →+ M := toAddMonoid fun x => AddMonoidHom.id M
x✝ x y : ⨁ (i : ι), M
ihx : ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) x) = x
ihy : ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) y) = y
⊢ ↑(of (fun x => M) default) (↑(toAddMonoid fun x => AddMonoidHom.id M) (x + y)) = x + y
[PROOFSTEP]
rw [AddMonoidHom.map_add, AddMonoidHom.map_add, ihx, ihy]
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
κ : Type u_1
h : ι ≃ κ
f : ⨁ (i : ι), β i
k : κ
⊢ ↑(↑(equivCongrLeft h) f) k = ↑f (↑h.symm k)
[PROOFSTEP]
exact DFinsupp.comapDomain'_apply _ h.right_inv _ _
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝⁴ : AddCommMonoid γ
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : { x // x ∈ A i }
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) j) = ↑(if i = j then x else 0)
[PROOFSTEP]
obtain rfl | h := Decidable.eq_or_ne i j
[GOAL]
case inl
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝⁴ : AddCommMonoid γ
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i : ι
x : { x // x ∈ A i }
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) i) = ↑(if i = i then x else 0)
[PROOFSTEP]
rw [DirectSum.of_eq_same, if_pos rfl]
[GOAL]
case inr
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝⁴ : AddCommMonoid γ
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : { x // x ∈ A i }
h : i ≠ j
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) j) = ↑(if i = j then x else 0)
[PROOFSTEP]
rw [DirectSum.of_eq_of_ne _ _ _ _ h, if_neg h, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ iSup A = ⊤
[PROOFSTEP]
rw [AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom, AddMonoidHom.mrange_top_iff_surjective]
[GOAL]
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝² : AddCommMonoid γ
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ Function.Surjective ↑(DFinsupp.sumAddHom fun i => AddSubmonoid.subtype (A i))
[PROOFSTEP]
exact Function.Bijective.surjective h
