ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
C0 : C 0
⊢ C z
ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
⊢ C z
have C0 : C 0 := by
  have h₁ := @C1 0 0
  rwa [zero_tprodCoeff] at h₁
ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
C0 : C 0
x : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))
⊢ ∀ (x : R × ((i : ι) → (fun i => s i) i)) (xs : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))),
    C ↑xs → C ↑(FreeAddMonoid.of x + xs)
ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
C0 : C 0
⊢ C z
refine' AddCon.induction_on z fun x ↦ FreeAddMonoid.recOn x C0 _
ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
C0 : C 0
x : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))
⊢ ∀ (x : R × ((i : ι) → (fun i => s i) i)) (xs : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))),
    C ↑xs → C (↑(FreeAddMonoid.of x) + ↑xs)
ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
C0 : C 0
x : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))
⊢ ∀ (x : R × ((i : ι) → (fun i => s i) i)) (xs : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))),
    C ↑xs → C ↑(FreeAddMonoid.of x + xs)
simp_rw [AddCon.coe_add]
ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
C0 : C 0
x : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))
f : R × ((i : ι) → (fun i => s i) i)
y : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))
ih : C ↑y
⊢ C ↑(FreeAddMonoid.of f)
ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
C0 : C 0
x : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))
⊢ ∀ (x : R × ((i : ι) → (fun i => s i) i)) (xs : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))),
    C ↑xs → C (↑(FreeAddMonoid.of x) + ↑xs)
refine' fun f y ih ↦ Cp _ ih
no goals
ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
C0 : C 0
x : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))
f : R × ((i : ι) → (fun i => s i) i)
y : FreeAddMonoid (R × ((i : ι) → (fun i => s i) i))
ih : C ↑y
⊢ C ↑(FreeAddMonoid.of f)
convert@C1 f.1 f.2
ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
h₁ : C (tprodCoeff R 0 0)
⊢ C 0
ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
⊢ C 0
have h₁ := @C1 0 0
no goals
ι : Type u_1
ι₂ : Type ?u.91649
ι₃ : Type ?u.91652
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.91661
R₂ : Type ?u.91664
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.91854
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.91988
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.92122
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
h₁ : C (tprodCoeff R 0 0)
⊢ C 0
rwa [zero_tprodCoeff] at h₁