ι : 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)
ι : 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
apply Dfinsupp.induction x H_zero
ι : 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)
ι : 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)
intro i b f h1 h2 ih
no goals
ι : 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)
solve_by_elim