[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹² : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹¹ : (i : ι) → AddCommMonoid (s i)
inst✝¹⁰ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
E : Type u_9
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
F : Type u_10
inst✝⁵ : AddCommMonoid F
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
⊢ tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r • z) f
[PROOFSTEP]
have h₁ : r • z = r • (1 : R) * z := by rw [smul_mul_assoc, one_mul]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹² : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹¹ : (i : ι) → AddCommMonoid (s i)
inst✝¹⁰ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
E : Type u_9
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
F : Type u_10
inst✝⁵ : AddCommMonoid F
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
⊢ r • z = r • 1 * z
[PROOFSTEP]
rw [smul_mul_assoc, one_mul]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹² : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹¹ : (i : ι) → AddCommMonoid (s i)
inst✝¹⁰ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
E : Type u_9
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
F : Type u_10
inst✝⁵ : AddCommMonoid F
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
h₁ : r • z = r • 1 * z
⊢ tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r • z) f
[PROOFSTEP]
have h₂ : r • f i = (r • (1 : R)) • f i := (smul_one_smul _ _ _).symm
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹² : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹¹ : (i : ι) → AddCommMonoid (s i)
inst✝¹⁰ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
E : Type u_9
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
F : Type u_10
inst✝⁵ : AddCommMonoid F
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
h₁ : r • z = r • 1 * z
h₂ : r • f i = (r • 1) • f i
⊢ tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r • z) f
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹² : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹¹ : (i : ι) → AddCommMonoid (s i)
inst✝¹⁰ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
E : Type u_9
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
F : Type u_10
inst✝⁵ : AddCommMonoid F
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
h₁ : r • z = r • 1 * z
h₂ : r • f i = (r • 1) • f i
⊢ tprodCoeff R z (update f i ((r • 1) • f i)) = tprodCoeff R (r • 1 * z) f
[PROOFSTEP]
exact smul_tprodCoeff_aux z f i _
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
r' : R
f : (i : ι) → s i
i : ι
hf : f i = 0
⊢ ↑(↑FreeAddMonoid.lift φ) (FreeAddMonoid.of (r', f)) = ↑(↑FreeAddMonoid.lift φ) 0
[PROOFSTEP]
simp [FreeAddMonoid.lift_eval_of, C0 r' f i hf]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
f : (i : ι) → s i
⊢ ↑(↑FreeAddMonoid.lift φ) (FreeAddMonoid.of (0, f)) = ↑(↑FreeAddMonoid.lift φ) 0
[PROOFSTEP]
simp [FreeAddMonoid.lift_eval_of, C0']
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
inst : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
m₁ m₂ : s i
⊢ ↑(↑FreeAddMonoid.lift φ) (FreeAddMonoid.of (z, update f i m₁) + FreeAddMonoid.of (z, update f i m₂)) =
    ↑(↑FreeAddMonoid.lift φ) (FreeAddMonoid.of (z, update f i (m₁ + m₂)))
[PROOFSTEP]
simp [FreeAddMonoid.lift_eval_of, @C_add inst]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
z₁ z₂ : R
f : (i : ι) → s i
⊢ ↑(↑FreeAddMonoid.lift φ) (FreeAddMonoid.of (z₁, f) + FreeAddMonoid.of (z₂, f)) =
    ↑(↑FreeAddMonoid.lift φ) (FreeAddMonoid.of (z₁ + z₂, f))
[PROOFSTEP]
simp [FreeAddMonoid.lift_eval_of, C_add_scalar]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
inst : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r' : R
⊢ ↑(↑FreeAddMonoid.lift φ) (FreeAddMonoid.of (z, update f i (r' • f i))) =
    ↑(↑FreeAddMonoid.lift φ) (FreeAddMonoid.of (r' * z, f))
[PROOFSTEP]
simp [FreeAddMonoid.lift_eval_of, @C_smul inst]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x✝ y✝ : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x✝ y✝
x y : FreeAddMonoid (R × ((i : ι) → s i))
⊢ ↑(↑FreeAddMonoid.lift φ) (x + y) = ↑(↑FreeAddMonoid.lift φ) (y + x)
[PROOFSTEP]
simp_rw [AddMonoidHom.map_add, add_comm]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
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
[PROOFSTEP]
have C0 : C 0 := by
  have h₁ := @C1 0 0
  rwa [zero_tprodCoeff] at h₁ 
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
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
[PROOFSTEP]
have h₁ := @C1 0 0
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
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
[PROOFSTEP]
rwa [zero_tprodCoeff] at h₁ 
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
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
[PROOFSTEP]
refine' AddCon.induction_on z fun x ↦ FreeAddMonoid.recOn x C0 _
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
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)
[PROOFSTEP]
simp_rw [AddCon.coe_add]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
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)
[PROOFSTEP]
refine' fun f y ih ↦ Cp _ ih
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
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)
[PROOFSTEP]
convert @C1 f.1 f.2
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
r : R₁
r' : R
f : (i : ι) → s i
i : ι
hf : f i = 0
⊢ (fun f => tprodCoeff R (r • f.fst) f.snd) (r', f) = 0
[PROOFSTEP]
simp_rw [zero_tprodCoeff' _ f i hf]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
r : R₁
f : (i : ι) → s i
⊢ (fun f => tprodCoeff R (r • f.fst) f.snd) (0, f) = 0
[PROOFSTEP]
simp [zero_tprodCoeff]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁴ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹³ : (i : ι) → AddCommMonoid (s i)
inst✝¹² : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
E : Type u_9
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module R E
F : Type u_10
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Monoid R₁
inst✝⁵ : DistribMulAction R₁ R
inst✝⁴ : SMulCommClass R₁ R R
inst✝³ : Monoid R₂
inst✝² : DistribMulAction R₂ R
inst✝¹ : SMulCommClass R₂ R R
r : R₁
inst✝ : DecidableEq ι
r' : R
f : (i : ι) → s i
i : ι
m₁ m₂ : s i
⊢ (fun f => tprodCoeff R (r • f.fst) f.snd) (r', update f i m₁) +
      (fun f => tprodCoeff R (r • f.fst) f.snd) (r', update f i m₂) =
    (fun f => tprodCoeff R (r • f.fst) f.snd) (r', update f i (m₁ + m₂))
[PROOFSTEP]
simp [add_tprodCoeff]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
r : R₁
r' r'' : R
f : (i : ι) → s i
⊢ (fun f => tprodCoeff R (r • f.fst) f.snd) (r', f) + (fun f => tprodCoeff R (r • f.fst) f.snd) (r'', f) =
    (fun f => tprodCoeff R (r • f.fst) f.snd) (r' + r'', f)
[PROOFSTEP]
simp [add_tprodCoeff', mul_add]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁴ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹³ : (i : ι) → AddCommMonoid (s i)
inst✝¹² : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
E : Type u_9
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module R E
F : Type u_10
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Monoid R₁
inst✝⁵ : DistribMulAction R₁ R
inst✝⁴ : SMulCommClass R₁ R R
inst✝³ : Monoid R₂
inst✝² : DistribMulAction R₂ R
inst✝¹ : SMulCommClass R₂ R R
r : R₁
inst✝ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r' : R
⊢ (fun f => tprodCoeff R (r • f.fst) f.snd) (z, update f i (r' • f i)) =
    (fun f => tprodCoeff R (r • f.fst) f.snd) (r' * z, f)
[PROOFSTEP]
simp [smul_tprodCoeff, mul_smul_comm]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ 1 • tprodCoeff R r f = tprodCoeff R r f
[PROOFSTEP]
rw [smul_tprodCoeff', one_smul]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
x z y : ⨂[R] (i : ι), s i
ihz : 1 • z = z
ihy : 1 • y = y
⊢ 1 • (z + y) = z + y
[PROOFSTEP]
simp_rw [PiTensorProduct.smul_add, ihz, ihy]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
r r' : R₁
x : ⨂[R] (i : ι), s i
r'' : R
f : (i : ι) → s i
⊢ (r * r') • tprodCoeff R r'' f = r • r' • tprodCoeff R r'' f
[PROOFSTEP]
simp [smul_tprodCoeff', smul_smul]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹³ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹² : (i : ι) → AddCommMonoid (s i)
inst✝¹¹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
E : Type u_9
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module R E
F : Type u_10
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
r r' : R₁
x✝ x y : ⨂[R] (i : ι), s i
ihx : (r * r') • x = r • r' • x
ihy : (r * r') • y = r • r' • y
⊢ (r * r') • (x + y) = r • r' • (x + y)
[PROOFSTEP]
simp_rw [PiTensorProduct.smul_add, ihx, ihy]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁴ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹³ : (i : ι) → AddCommMonoid (s i)
inst✝¹² : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
E : Type u_9
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module R E
F : Type u_10
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Monoid R₁
inst✝⁵ : DistribMulAction R₁ R
inst✝⁴ : SMulCommClass R₁ R R
inst✝³ : Monoid R₂
inst✝² : DistribMulAction R₂ R
inst✝¹ : SMulCommClass R₂ R R
inst✝ : SMulCommClass R₁ R₂ R
r' : R₁
r'' : R₂
x : ⨂[R] (i : ι), s i
xr : R
xf : (i : ι) → s i
⊢ r' • r'' • tprodCoeff R xr xf = r'' • r' • tprodCoeff R xr xf
[PROOFSTEP]
simp only [smul_tprodCoeff', smul_comm]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁴ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹³ : (i : ι) → AddCommMonoid (s i)
inst✝¹² : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
E : Type u_9
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module R E
F : Type u_10
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Monoid R₁
inst✝⁵ : DistribMulAction R₁ R
inst✝⁴ : SMulCommClass R₁ R R
inst✝³ : Monoid R₂
inst✝² : DistribMulAction R₂ R
inst✝¹ : SMulCommClass R₂ R R
inst✝ : SMulCommClass R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : r' • r'' • z = r'' • r' • z
ihy : r' • r'' • y = r'' • r' • y
⊢ r' • r'' • (z + y) = r'' • r' • (z + y)
[PROOFSTEP]
simp_rw [PiTensorProduct.smul_add, ihz, ihy]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁵ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁴ : (i : ι) → AddCommMonoid (s i)
inst✝¹³ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
E : Type u_9
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
F : Type u_10
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Monoid R₁
inst✝⁶ : DistribMulAction R₁ R
inst✝⁵ : SMulCommClass R₁ R R
inst✝⁴ : Monoid R₂
inst✝³ : DistribMulAction R₂ R
inst✝² : SMulCommClass R₂ R R
inst✝¹ : SMul R₁ R₂
inst✝ : IsScalarTower R₁ R₂ R
r' : R₁
r'' : R₂
x : ⨂[R] (i : ι), s i
xr : R
xf : (i : ι) → s i
⊢ (r' • r'') • tprodCoeff R xr xf = r' • r'' • tprodCoeff R xr xf
[PROOFSTEP]
simp only [smul_tprodCoeff', smul_assoc]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁵ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁴ : (i : ι) → AddCommMonoid (s i)
inst✝¹³ : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
E : Type u_9
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
F : Type u_10
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Monoid R₁
inst✝⁶ : DistribMulAction R₁ R
inst✝⁵ : SMulCommClass R₁ R R
inst✝⁴ : Monoid R₂
inst✝³ : DistribMulAction R₂ R
inst✝² : SMulCommClass R₂ R R
inst✝¹ : SMul R₁ R₂
inst✝ : IsScalarTower R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : (r' • r'') • z = r' • r'' • z
ihy : (r' • r'') • y = r' • r'' • y
⊢ (r' • r'') • (z + y) = r' • r'' • (z + y)
[PROOFSTEP]
simp_rw [PiTensorProduct.smul_add, ihz, ihy]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
src✝ : DistribMulAction R₁ (⨂[R] (i : ι), s i) := distribMulAction'
r✝ r' : R₁
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ (r✝ + r') • tprodCoeff R r f = r✝ • tprodCoeff R r f + r' • tprodCoeff R r f
[PROOFSTEP]
simp_rw [smul_tprodCoeff', add_smul, add_tprodCoeff']
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
src✝ : DistribMulAction R₁ (⨂[R] (i : ι), s i) := distribMulAction'
r r' : R₁
x✝ x y : ⨂[R] (i : ι), s i
ihx : (r + r') • x = r • x + r' • x
ihy : (r + r') • y = r • y + r' • y
⊢ (r + r') • (x + y) = r • (x + y) + r' • (x + y)
[PROOFSTEP]
simp_rw [PiTensorProduct.smul_add, ihx, ihy, add_add_add_comm]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
src✝ : DistribMulAction R₁ (⨂[R] (i : ι), s i) := distribMulAction'
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ 0 • tprodCoeff R r f = 0
[PROOFSTEP]
simp_rw [smul_tprodCoeff', zero_smul, zero_tprodCoeff]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
src✝ : DistribMulAction R₁ (⨂[R] (i : ι), s i) := distribMulAction'
x✝ x y : ⨂[R] (i : ι), s i
ihx : 0 • x = 0
ihy : 0 • y = 0
⊢ 0 • (x + y) = 0
[PROOFSTEP]
simp_rw [PiTensorProduct.smul_add, ihx, ihy, add_zero]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
x✝ : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
⊢ tprodCoeff R 1 (update f i (r • x)) = r • tprodCoeff R 1 (update f i x)
[PROOFSTEP]
rw [smul_tprodCoeff', ← smul_tprodCoeff (1 : R) _ i, update_idem, update_same]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
z : R
f : (i : ι) → s i
⊢ tprodCoeff R z f = z • ↑(tprod R) f
[PROOFSTEP]
have : z = z • (1 : R) := by simp only [mul_one, Algebra.id.smul_eq_mul]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
z : R
f : (i : ι) → s i
⊢ z = z • 1
[PROOFSTEP]
simp only [mul_one, Algebra.id.smul_eq_mul]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
z : R
f : (i : ι) → s i
this : z = z • 1
⊢ tprodCoeff R z f = z • ↑(tprod R) f
[PROOFSTEP]
conv_lhs => rw [this]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
z : R
f : (i : ι) → s i
this : z = z • 1
| tprodCoeff R z f
[PROOFSTEP]
rw [this]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
z : R
f : (i : ι) → s i
this : z = z • 1
| tprodCoeff R z f
[PROOFSTEP]
rw [this]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
z : R
f : (i : ι) → s i
this : z = z • 1
| tprodCoeff R z f
[PROOFSTEP]
rw [this]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (r • ↑(tprod R) f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
⊢ C z
[PROOFSTEP]
simp_rw [← tprodCoeff_eq_smul_tprod] at C1 
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
⊢ C z
[PROOFSTEP]
exact PiTensorProduct.induction_on' z @C1 @Cp
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
⊢ φ₁ = φ₂
[PROOFSTEP]
refine' LinearMap.ext _
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
⊢ ∀ (x : ⨂[R] (i : ι), s i), ↑φ₁ x = ↑φ₂ x
[PROOFSTEP]
refine' fun z ↦ PiTensorProduct.induction_on' z _ fun {x y} hx hy ↦ by rw [φ₁.map_add, φ₂.map_add, hx, hy]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z x y : ⨂[R] (i : ι), s i
hx : ↑φ₁ x = ↑φ₂ x
hy : ↑φ₁ y = ↑φ₂ y
⊢ ↑φ₁ (x + y) = ↑φ₂ (x + y)
[PROOFSTEP]
rw [φ₁.map_add, φ₂.map_add, hx, hy]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
⊢ ∀ {r : R} {f : (i : ι) → s i}, ↑φ₁ (tprodCoeff R r f) = ↑φ₂ (tprodCoeff R r f)
[PROOFSTEP]
intro r f
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ ↑φ₁ (tprodCoeff R r f) = ↑φ₂ (tprodCoeff R r f)
[PROOFSTEP]
rw [tprodCoeff_eq_smul_tprod, φ₁.map_smul, φ₂.map_smul]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ r • ↑φ₁ (↑(tprod R) f) = r • ↑φ₂ (↑(tprod R) f)
[PROOFSTEP]
apply _root_.congr_arg
[GOAL]
case h
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : LinearMap.compMultilinearMap φ₁ (tprod R) = LinearMap.compMultilinearMap φ₂ (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ ↑φ₁ (↑(tprod R) f) = ↑φ₂ (↑(tprod R) f)
[PROOFSTEP]
exact MultilinearMap.congr_fun H f
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
z : R
f : (i : ι) → s i
i : ι
hf : f i = 0
⊢ (fun p => p.fst • ↑φ p.snd) (z, f) = 0
[PROOFSTEP]
simp_rw [map_coord_zero φ i hf, smul_zero]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ (fun p => p.fst • ↑φ p.snd) (0, f) = 0
[PROOFSTEP]
simp_rw [zero_smul]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
m₁ m₂ : s i
⊢ (fun p => p.fst • ↑φ p.snd) (z, update f i m₁) + (fun p => p.fst • ↑φ p.snd) (z, update f i m₂) =
    (fun p => p.fst • ↑φ p.snd) (z, update f i (m₁ + m₂))
[PROOFSTEP]
simp_rw [← smul_add, φ.map_add]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
z₁ z₂ : R
f : (i : ι) → s i
⊢ (fun p => p.fst • ↑φ p.snd) (z₁, f) + (fun p => p.fst • ↑φ p.snd) (z₂, f) = (fun p => p.fst • ↑φ p.snd) (z₁ + z₂, f)
[PROOFSTEP]
rw [← add_smul]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R
⊢ (fun p => p.fst • ↑φ p.snd) (z, update f i (r • f i)) = (fun p => p.fst • ↑φ p.snd) (r * z, f)
[PROOFSTEP]
simp [φ.map_smul, smul_smul, mul_comm]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ ↑(liftAux φ) (↑(tprod R) f) = ↑φ f
[PROOFSTEP]
simp only [liftAux, liftAddHom, tprod_eq_tprodCoeff_one, tprodCoeff, AddCon.coe_mk']
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ ↑(AddCon.lift (addConGen (Eqv R fun i => s i)) (↑FreeAddMonoid.lift fun p => p.fst • ↑φ p.snd)
          (_ : addConGen (Eqv R fun i => s i) ≤ AddCon.ker (↑FreeAddMonoid.lift fun p => p.fst • ↑φ p.snd)))
      ↑(FreeAddMonoid.of (1, f)) =
    ↑φ f
[PROOFSTEP]
rw [FreeAddMonoid.of, FreeAddMonoid.ofList, Equiv.refl_apply, AddCon.lift_coe]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ ↑(↑FreeAddMonoid.lift fun p => p.fst • ↑φ p.snd) [(1, f)] = ↑φ f
[PROOFSTEP]
dsimp [FreeAddMonoid.lift, FreeAddMonoid.sumAux]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ (FreeAddMonoid.sumAux.match_1 (fun x => E) [1 • ↑φ f] (fun _ => 0) fun x xs =>
      List.foldl (fun x x_1 => x + x_1) x xs) =
    ↑φ f
[PROOFSTEP]
show _ • _ = _
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ 1 • ↑φ f = ↑φ f
[PROOFSTEP]
rw [one_smul]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x
[PROOFSTEP]
refine' PiTensorProduct.induction_on' x _ _
[GOAL]
case refine'_1
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ ∀ {r_1 : R} {f : (i : ι) → s i}, ↑(liftAux φ) (r • tprodCoeff R r_1 f) = r • ↑(liftAux φ) (tprodCoeff R r_1 f)
[PROOFSTEP]
intro z f
[GOAL]
case refine'_1
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
⊢ ↑(liftAux φ) (r • tprodCoeff R z f) = r • ↑(liftAux φ) (tprodCoeff R z f)
[PROOFSTEP]
rw [smul_tprodCoeff' r z f, liftAux_tprodCoeff, liftAux_tprodCoeff, smul_assoc]
[GOAL]
case refine'_2
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ ∀ {x y : ⨂[R] (i : ι), s i},
    ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x →
      ↑(liftAux φ) (r • y) = r • ↑(liftAux φ) y → ↑(liftAux φ) (r • (x + y)) = r • ↑(liftAux φ) (x + y)
[PROOFSTEP]
intro z y ihz ihy
[GOAL]
case refine'_2
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
x z y : ⨂[R] (i : ι), s i
ihz : ↑(liftAux φ) (r • z) = r • ↑(liftAux φ) z
ihy : ↑(liftAux φ) (r • y) = r • ↑(liftAux φ) y
⊢ ↑(liftAux φ) (r • (z + y)) = r • ↑(liftAux φ) (z + y)
[PROOFSTEP]
rw [smul_add, (liftAux φ).map_add, ihz, ihy, (liftAux φ).map_add, smul_add]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ₁ φ₂ : MultilinearMap R s E
⊢ (fun φ =>
        let src := liftAux φ;
        {
          toAddHom :=
            { toFun := src.toFun,
              map_add' :=
                (_ :
                  ∀ (x y : ⨂[R] (i : ι), s i),
                    ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
          map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
      (φ₁ + φ₂) =
    (fun φ =>
          let src := liftAux φ;
          {
            toAddHom :=
              { toFun := src.toFun,
                map_add' :=
                  (_ :
                    ∀ (x y : ⨂[R] (i : ι), s i),
                      ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
            map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
        φ₁ +
      (fun φ =>
          let src := liftAux φ;
          {
            toAddHom :=
              { toFun := src.toFun,
                map_add' :=
                  (_ :
                    ∀ (x y : ⨂[R] (i : ι), s i),
                      ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
            map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
        φ₂
[PROOFSTEP]
ext
[GOAL]
case H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ₁ φ₂ : MultilinearMap R s E
x✝ : (i : ι) → s i
⊢ ↑(LinearMap.compMultilinearMap
          ((fun φ =>
              let src := liftAux φ;
              {
                toAddHom :=
                  { toFun := src.toFun,
                    map_add' :=
                      (_ :
                        ∀ (x y : ⨂[R] (i : ι), s i),
                          ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
            (φ₁ + φ₂))
          (tprod R))
      x✝ =
    ↑(LinearMap.compMultilinearMap
          ((fun φ =>
                let src := liftAux φ;
                {
                  toAddHom :=
                    { toFun := src.toFun,
                      map_add' :=
                        (_ :
                          ∀ (x y : ⨂[R] (i : ι), s i),
                            ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                  map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
              φ₁ +
            (fun φ =>
                let src := liftAux φ;
                {
                  toAddHom :=
                    { toFun := src.toFun,
                      map_add' :=
                        (_ :
                          ∀ (x y : ⨂[R] (i : ι), s i),
                            ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                  map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
              φ₂)
          (tprod R))
      x✝
[PROOFSTEP]
simp [liftAux_tprod]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
r : R
φ₂ : MultilinearMap R s E
⊢ AddHom.toFun
      {
        toFun := fun φ =>
          let src := liftAux φ;
          {
            toAddHom :=
              { toFun := src.toFun,
                map_add' :=
                  (_ :
                    ∀ (x y : ⨂[R] (i : ι), s i),
                      ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
            map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
        map_add' :=
          (_ :
            ∀ (φ₁ φ₂ : MultilinearMap R s E),
              (fun φ =>
                    let src := liftAux φ;
                    {
                      toAddHom :=
                        { toFun := src.toFun,
                          map_add' :=
                            (_ :
                              ∀ (x y : ⨂[R] (i : ι), s i),
                                ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                      map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                  (φ₁ + φ₂) =
                (fun φ =>
                      let src := liftAux φ;
                      {
                        toAddHom :=
                          { toFun := src.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : ⨂[R] (i : ι), s i),
                                  ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                        map_smul' :=
                          (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                    φ₁ +
                  (fun φ =>
                      let src := liftAux φ;
                      {
                        toAddHom :=
                          { toFun := src.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : ⨂[R] (i : ι), s i),
                                  ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                        map_smul' :=
                          (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                    φ₂) }
      (r • φ₂) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        {
          toFun := fun φ =>
            let src := liftAux φ;
            {
              toAddHom :=
                { toFun := src.toFun,
                  map_add' :=
                    (_ :
                      ∀ (x y : ⨂[R] (i : ι), s i),
                        ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
              map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
          map_add' :=
            (_ :
              ∀ (φ₁ φ₂ : MultilinearMap R s E),
                (fun φ =>
                      let src := liftAux φ;
                      {
                        toAddHom :=
                          { toFun := src.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : ⨂[R] (i : ι), s i),
                                  ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                        map_smul' :=
                          (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                    (φ₁ + φ₂) =
                  (fun φ =>
                        let src := liftAux φ;
                        {
                          toAddHom :=
                            { toFun := src.toFun,
                              map_add' :=
                                (_ :
                                  ∀ (x y : ⨂[R] (i : ι), s i),
                                    ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                          map_smul' :=
                            (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                      φ₁ +
                    (fun φ =>
                        let src := liftAux φ;
                        {
                          toAddHom :=
                            { toFun := src.toFun,
                              map_add' :=
                                (_ :
                                  ∀ (x y : ⨂[R] (i : ι), s i),
                                    ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                          map_smul' :=
                            (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                      φ₂) }
        φ₂
[PROOFSTEP]
ext
[GOAL]
case H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
r : R
φ₂ : MultilinearMap R s E
x✝ : (i : ι) → s i
⊢ ↑(LinearMap.compMultilinearMap
          (AddHom.toFun
            {
              toFun := fun φ =>
                let src := liftAux φ;
                {
                  toAddHom :=
                    { toFun := src.toFun,
                      map_add' :=
                        (_ :
                          ∀ (x y : ⨂[R] (i : ι), s i),
                            ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                  map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
              map_add' :=
                (_ :
                  ∀ (φ₁ φ₂ : MultilinearMap R s E),
                    (fun φ =>
                          let src := liftAux φ;
                          {
                            toAddHom :=
                              { toFun := src.toFun,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ⨂[R] (i : ι), s i),
                                      ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                            map_smul' :=
                              (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                        (φ₁ + φ₂) =
                      (fun φ =>
                            let src := liftAux φ;
                            {
                              toAddHom :=
                                { toFun := src.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ⨂[R] (i : ι), s i),
                                        ZeroHom.toFun (↑src) (x + y) =
                                          ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                              map_smul' :=
                                (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                          φ₁ +
                        (fun φ =>
                            let src := liftAux φ;
                            {
                              toAddHom :=
                                { toFun := src.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ⨂[R] (i : ι), s i),
                                        ZeroHom.toFun (↑src) (x + y) =
                                          ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                              map_smul' :=
                                (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                          φ₂) }
            (r • φ₂))
          (tprod R))
      x✝ =
    ↑(LinearMap.compMultilinearMap
          (↑(RingHom.id R) r •
            AddHom.toFun
              {
                toFun := fun φ =>
                  let src := liftAux φ;
                  {
                    toAddHom :=
                      { toFun := src.toFun,
                        map_add' :=
                          (_ :
                            ∀ (x y : ⨂[R] (i : ι), s i),
                              ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                    map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                map_add' :=
                  (_ :
                    ∀ (φ₁ φ₂ : MultilinearMap R s E),
                      (fun φ =>
                            let src := liftAux φ;
                            {
                              toAddHom :=
                                { toFun := src.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ⨂[R] (i : ι), s i),
                                        ZeroHom.toFun (↑src) (x + y) =
                                          ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                              map_smul' :=
                                (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                          (φ₁ + φ₂) =
                        (fun φ =>
                              let src := liftAux φ;
                              {
                                toAddHom :=
                                  { toFun := src.toFun,
                                    map_add' :=
                                      (_ :
                                        ∀ (x y : ⨂[R] (i : ι), s i),
                                          ZeroHom.toFun (↑src) (x + y) =
                                            ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                map_smul' :=
                                  (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                            φ₁ +
                          (fun φ =>
                              let src := liftAux φ;
                              {
                                toAddHom :=
                                  { toFun := src.toFun,
                                    map_add' :=
                                      (_ :
                                        ∀ (x y : ⨂[R] (i : ι), s i),
                                          ZeroHom.toFun (↑src) (x + y) =
                                            ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                map_smul' :=
                                  (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                            φ₂) }
              φ₂)
          (tprod R))
      x✝
[PROOFSTEP]
simp [liftAux_tprod]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ (fun φ' => LinearMap.compMultilinearMap φ' (tprod R))
      (AddHom.toFun
        {
            toAddHom :=
              {
                toFun := fun φ =>
                  let src := liftAux φ;
                  {
                    toAddHom :=
                      { toFun := src.toFun,
                        map_add' :=
                          (_ :
                            ∀ (x y : ⨂[R] (i : ι), s i),
                              ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                    map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                map_add' :=
                  (_ :
                    ∀ (φ₁ φ₂ : MultilinearMap R s E),
                      (fun φ =>
                            let src := liftAux φ;
                            {
                              toAddHom :=
                                { toFun := src.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ⨂[R] (i : ι), s i),
                                        ZeroHom.toFun (↑src) (x + y) =
                                          ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                              map_smul' :=
                                (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                          (φ₁ + φ₂) =
                        (fun φ =>
                              let src := liftAux φ;
                              {
                                toAddHom :=
                                  { toFun := src.toFun,
                                    map_add' :=
                                      (_ :
                                        ∀ (x y : ⨂[R] (i : ι), s i),
                                          ZeroHom.toFun (↑src) (x + y) =
                                            ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                map_smul' :=
                                  (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                            φ₁ +
                          (fun φ =>
                              let src := liftAux φ;
                              {
                                toAddHom :=
                                  { toFun := src.toFun,
                                    map_add' :=
                                      (_ :
                                        ∀ (x y : ⨂[R] (i : ι), s i),
                                          ZeroHom.toFun (↑src) (x + y) =
                                            ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                map_smul' :=
                                  (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                            φ₂) },
            map_smul' :=
              (_ :
                ∀ (r : R) (φ₂ : MultilinearMap R s E),
                  AddHom.toFun
                      {
                        toFun := fun φ =>
                          let src := liftAux φ;
                          {
                            toAddHom :=
                              { toFun := src.toFun,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ⨂[R] (i : ι), s i),
                                      ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                            map_smul' :=
                              (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                        map_add' :=
                          (_ :
                            ∀ (φ₁ φ₂ : MultilinearMap R s E),
                              (fun φ =>
                                    let src := liftAux φ;
                                    {
                                      toAddHom :=
                                        { toFun := src.toFun,
                                          map_add' :=
                                            (_ :
                                              ∀ (x y : ⨂[R] (i : ι), s i),
                                                ZeroHom.toFun (↑src) (x + y) =
                                                  ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                      map_smul' :=
                                        (_ :
                                          ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                            ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                  (φ₁ + φ₂) =
                                (fun φ =>
                                      let src := liftAux φ;
                                      {
                                        toAddHom :=
                                          { toFun := src.toFun,
                                            map_add' :=
                                              (_ :
                                                ∀ (x y : ⨂[R] (i : ι), s i),
                                                  ZeroHom.toFun (↑src) (x + y) =
                                                    ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                        map_smul' :=
                                          (_ :
                                            ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                              ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                    φ₁ +
                                  (fun φ =>
                                      let src := liftAux φ;
                                      {
                                        toAddHom :=
                                          { toFun := src.toFun,
                                            map_add' :=
                                              (_ :
                                                ∀ (x y : ⨂[R] (i : ι), s i),
                                                  ZeroHom.toFun (↑src) (x + y) =
                                                    ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                        map_smul' :=
                                          (_ :
                                            ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                              ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                    φ₂) }
                      (r • φ₂) =
                    ↑(RingHom.id R) r •
                      AddHom.toFun
                        {
                          toFun := fun φ =>
                            let src := liftAux φ;
                            {
                              toAddHom :=
                                { toFun := src.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ⨂[R] (i : ι), s i),
                                        ZeroHom.toFun (↑src) (x + y) =
                                          ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                              map_smul' :=
                                (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                          map_add' :=
                            (_ :
                              ∀ (φ₁ φ₂ : MultilinearMap R s E),
                                (fun φ =>
                                      let src := liftAux φ;
                                      {
                                        toAddHom :=
                                          { toFun := src.toFun,
                                            map_add' :=
                                              (_ :
                                                ∀ (x y : ⨂[R] (i : ι), s i),
                                                  ZeroHom.toFun (↑src) (x + y) =
                                                    ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                        map_smul' :=
                                          (_ :
                                            ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                              ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                    (φ₁ + φ₂) =
                                  (fun φ =>
                                        let src := liftAux φ;
                                        {
                                          toAddHom :=
                                            { toFun := src.toFun,
                                              map_add' :=
                                                (_ :
                                                  ∀ (x y : ⨂[R] (i : ι), s i),
                                                    ZeroHom.toFun (↑src) (x + y) =
                                                      ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                          map_smul' :=
                                            (_ :
                                              ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                      φ₁ +
                                    (fun φ =>
                                        let src := liftAux φ;
                                        {
                                          toAddHom :=
                                            { toFun := src.toFun,
                                              map_add' :=
                                                (_ :
                                                  ∀ (x y : ⨂[R] (i : ι), s i),
                                                    ZeroHom.toFun (↑src) (x + y) =
                                                      ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                          map_smul' :=
                                            (_ :
                                              ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                      φ₂) }
                        φ₂) }.toAddHom
        φ) =
    φ
[PROOFSTEP]
ext
[GOAL]
case H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
x✝ : (i : ι) → s i
⊢ ↑((fun φ' => LinearMap.compMultilinearMap φ' (tprod R))
          (AddHom.toFun
            {
                toAddHom :=
                  {
                    toFun := fun φ =>
                      let src := liftAux φ;
                      {
                        toAddHom :=
                          { toFun := src.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : ⨂[R] (i : ι), s i),
                                  ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                        map_smul' :=
                          (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                    map_add' :=
                      (_ :
                        ∀ (φ₁ φ₂ : MultilinearMap R s E),
                          (fun φ =>
                                let src := liftAux φ;
                                {
                                  toAddHom :=
                                    { toFun := src.toFun,
                                      map_add' :=
                                        (_ :
                                          ∀ (x y : ⨂[R] (i : ι), s i),
                                            ZeroHom.toFun (↑src) (x + y) =
                                              ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                  map_smul' :=
                                    (_ :
                                      ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                              (φ₁ + φ₂) =
                            (fun φ =>
                                  let src := liftAux φ;
                                  {
                                    toAddHom :=
                                      { toFun := src.toFun,
                                        map_add' :=
                                          (_ :
                                            ∀ (x y : ⨂[R] (i : ι), s i),
                                              ZeroHom.toFun (↑src) (x + y) =
                                                ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                    map_smul' :=
                                      (_ :
                                        ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                φ₁ +
                              (fun φ =>
                                  let src := liftAux φ;
                                  {
                                    toAddHom :=
                                      { toFun := src.toFun,
                                        map_add' :=
                                          (_ :
                                            ∀ (x y : ⨂[R] (i : ι), s i),
                                              ZeroHom.toFun (↑src) (x + y) =
                                                ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                    map_smul' :=
                                      (_ :
                                        ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                φ₂) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (φ₂ : MultilinearMap R s E),
                      AddHom.toFun
                          {
                            toFun := fun φ =>
                              let src := liftAux φ;
                              {
                                toAddHom :=
                                  { toFun := src.toFun,
                                    map_add' :=
                                      (_ :
                                        ∀ (x y : ⨂[R] (i : ι), s i),
                                          ZeroHom.toFun (↑src) (x + y) =
                                            ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                map_smul' :=
                                  (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                            map_add' :=
                              (_ :
                                ∀ (φ₁ φ₂ : MultilinearMap R s E),
                                  (fun φ =>
                                        let src := liftAux φ;
                                        {
                                          toAddHom :=
                                            { toFun := src.toFun,
                                              map_add' :=
                                                (_ :
                                                  ∀ (x y : ⨂[R] (i : ι), s i),
                                                    ZeroHom.toFun (↑src) (x + y) =
                                                      ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                          map_smul' :=
                                            (_ :
                                              ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                      (φ₁ + φ₂) =
                                    (fun φ =>
                                          let src := liftAux φ;
                                          {
                                            toAddHom :=
                                              { toFun := src.toFun,
                                                map_add' :=
                                                  (_ :
                                                    ∀ (x y : ⨂[R] (i : ι), s i),
                                                      ZeroHom.toFun (↑src) (x + y) =
                                                        ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                            map_smul' :=
                                              (_ :
                                                ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                  ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                        φ₁ +
                                      (fun φ =>
                                          let src := liftAux φ;
                                          {
                                            toAddHom :=
                                              { toFun := src.toFun,
                                                map_add' :=
                                                  (_ :
                                                    ∀ (x y : ⨂[R] (i : ι), s i),
                                                      ZeroHom.toFun (↑src) (x + y) =
                                                        ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                            map_smul' :=
                                              (_ :
                                                ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                  ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                        φ₂) }
                          (r • φ₂) =
                        ↑(RingHom.id R) r •
                          AddHom.toFun
                            {
                              toFun := fun φ =>
                                let src := liftAux φ;
                                {
                                  toAddHom :=
                                    { toFun := src.toFun,
                                      map_add' :=
                                        (_ :
                                          ∀ (x y : ⨂[R] (i : ι), s i),
                                            ZeroHom.toFun (↑src) (x + y) =
                                              ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                  map_smul' :=
                                    (_ :
                                      ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                              map_add' :=
                                (_ :
                                  ∀ (φ₁ φ₂ : MultilinearMap R s E),
                                    (fun φ =>
                                          let src := liftAux φ;
                                          {
                                            toAddHom :=
                                              { toFun := src.toFun,
                                                map_add' :=
                                                  (_ :
                                                    ∀ (x y : ⨂[R] (i : ι), s i),
                                                      ZeroHom.toFun (↑src) (x + y) =
                                                        ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                            map_smul' :=
                                              (_ :
                                                ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                  ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                        (φ₁ + φ₂) =
                                      (fun φ =>
                                            let src := liftAux φ;
                                            {
                                              toAddHom :=
                                                { toFun := src.toFun,
                                                  map_add' :=
                                                    (_ :
                                                      ∀ (x y : ⨂[R] (i : ι), s i),
                                                        ZeroHom.toFun (↑src) (x + y) =
                                                          ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                              map_smul' :=
                                                (_ :
                                                  ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                    ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                          φ₁ +
                                        (fun φ =>
                                            let src := liftAux φ;
                                            {
                                              toAddHom :=
                                                { toFun := src.toFun,
                                                  map_add' :=
                                                    (_ :
                                                      ∀ (x y : ⨂[R] (i : ι), s i),
                                                        ZeroHom.toFun (↑src) (x + y) =
                                                          ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                              map_smul' :=
                                                (_ :
                                                  ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                    ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                          φ₂) }
                            φ₂) }.toAddHom
            φ))
      x✝ =
    ↑φ x✝
[PROOFSTEP]
simp [liftAux_tprod, LinearMap.compMultilinearMap]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : (⨂[R] (i : ι), s i) →ₗ[R] E
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun φ =>
                let src := liftAux φ;
                {
                  toAddHom :=
                    { toFun := src.toFun,
                      map_add' :=
                        (_ :
                          ∀ (x y : ⨂[R] (i : ι), s i),
                            ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                  map_smul' := (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
              map_add' :=
                (_ :
                  ∀ (φ₁ φ₂ : MultilinearMap R s E),
                    (fun φ =>
                          let src := liftAux φ;
                          {
                            toAddHom :=
                              { toFun := src.toFun,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ⨂[R] (i : ι), s i),
                                      ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                            map_smul' :=
                              (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                        (φ₁ + φ₂) =
                      (fun φ =>
                            let src := liftAux φ;
                            {
                              toAddHom :=
                                { toFun := src.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ⨂[R] (i : ι), s i),
                                        ZeroHom.toFun (↑src) (x + y) =
                                          ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                              map_smul' :=
                                (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                          φ₁ +
                        (fun φ =>
                            let src := liftAux φ;
                            {
                              toAddHom :=
                                { toFun := src.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ⨂[R] (i : ι), s i),
                                        ZeroHom.toFun (↑src) (x + y) =
                                          ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                              map_smul' :=
                                (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                          φ₂) },
          map_smul' :=
            (_ :
              ∀ (r : R) (φ₂ : MultilinearMap R s E),
                AddHom.toFun
                    {
                      toFun := fun φ =>
                        let src := liftAux φ;
                        {
                          toAddHom :=
                            { toFun := src.toFun,
                              map_add' :=
                                (_ :
                                  ∀ (x y : ⨂[R] (i : ι), s i),
                                    ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                          map_smul' :=
                            (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                      map_add' :=
                        (_ :
                          ∀ (φ₁ φ₂ : MultilinearMap R s E),
                            (fun φ =>
                                  let src := liftAux φ;
                                  {
                                    toAddHom :=
                                      { toFun := src.toFun,
                                        map_add' :=
                                          (_ :
                                            ∀ (x y : ⨂[R] (i : ι), s i),
                                              ZeroHom.toFun (↑src) (x + y) =
                                                ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                    map_smul' :=
                                      (_ :
                                        ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                (φ₁ + φ₂) =
                              (fun φ =>
                                    let src := liftAux φ;
                                    {
                                      toAddHom :=
                                        { toFun := src.toFun,
                                          map_add' :=
                                            (_ :
                                              ∀ (x y : ⨂[R] (i : ι), s i),
                                                ZeroHom.toFun (↑src) (x + y) =
                                                  ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                      map_smul' :=
                                        (_ :
                                          ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                            ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                  φ₁ +
                                (fun φ =>
                                    let src := liftAux φ;
                                    {
                                      toAddHom :=
                                        { toFun := src.toFun,
                                          map_add' :=
                                            (_ :
                                              ∀ (x y : ⨂[R] (i : ι), s i),
                                                ZeroHom.toFun (↑src) (x + y) =
                                                  ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                      map_smul' :=
                                        (_ :
                                          ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                            ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                  φ₂) }
                    (r • φ₂) =
                  ↑(RingHom.id R) r •
                    AddHom.toFun
                      {
                        toFun := fun φ =>
                          let src := liftAux φ;
                          {
                            toAddHom :=
                              { toFun := src.toFun,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ⨂[R] (i : ι), s i),
                                      ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                            map_smul' :=
                              (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                        map_add' :=
                          (_ :
                            ∀ (φ₁ φ₂ : MultilinearMap R s E),
                              (fun φ =>
                                    let src := liftAux φ;
                                    {
                                      toAddHom :=
                                        { toFun := src.toFun,
                                          map_add' :=
                                            (_ :
                                              ∀ (x y : ⨂[R] (i : ι), s i),
                                                ZeroHom.toFun (↑src) (x + y) =
                                                  ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                      map_smul' :=
                                        (_ :
                                          ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                            ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                  (φ₁ + φ₂) =
                                (fun φ =>
                                      let src := liftAux φ;
                                      {
                                        toAddHom :=
                                          { toFun := src.toFun,
                                            map_add' :=
                                              (_ :
                                                ∀ (x y : ⨂[R] (i : ι), s i),
                                                  ZeroHom.toFun (↑src) (x + y) =
                                                    ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                        map_smul' :=
                                          (_ :
                                            ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                              ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                    φ₁ +
                                  (fun φ =>
                                      let src := liftAux φ;
                                      {
                                        toAddHom :=
                                          { toFun := src.toFun,
                                            map_add' :=
                                              (_ :
                                                ∀ (x y : ⨂[R] (i : ι), s i),
                                                  ZeroHom.toFun (↑src) (x + y) =
                                                    ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                        map_smul' :=
                                          (_ :
                                            ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                              ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                    φ₂) }
                      φ₂) }.toAddHom
      ((fun φ' => LinearMap.compMultilinearMap φ' (tprod R)) φ) =
    φ
[PROOFSTEP]
ext
[GOAL]
case H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : (⨂[R] (i : ι), s i) →ₗ[R] E
x✝ : (i : ι) → s i
⊢ ↑(LinearMap.compMultilinearMap
          (AddHom.toFun
            {
                toAddHom :=
                  {
                    toFun := fun φ =>
                      let src := liftAux φ;
                      {
                        toAddHom :=
                          { toFun := src.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : ⨂[R] (i : ι), s i),
                                  ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                        map_smul' :=
                          (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                    map_add' :=
                      (_ :
                        ∀ (φ₁ φ₂ : MultilinearMap R s E),
                          (fun φ =>
                                let src := liftAux φ;
                                {
                                  toAddHom :=
                                    { toFun := src.toFun,
                                      map_add' :=
                                        (_ :
                                          ∀ (x y : ⨂[R] (i : ι), s i),
                                            ZeroHom.toFun (↑src) (x + y) =
                                              ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                  map_smul' :=
                                    (_ :
                                      ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                              (φ₁ + φ₂) =
                            (fun φ =>
                                  let src := liftAux φ;
                                  {
                                    toAddHom :=
                                      { toFun := src.toFun,
                                        map_add' :=
                                          (_ :
                                            ∀ (x y : ⨂[R] (i : ι), s i),
                                              ZeroHom.toFun (↑src) (x + y) =
                                                ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                    map_smul' :=
                                      (_ :
                                        ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                φ₁ +
                              (fun φ =>
                                  let src := liftAux φ;
                                  {
                                    toAddHom :=
                                      { toFun := src.toFun,
                                        map_add' :=
                                          (_ :
                                            ∀ (x y : ⨂[R] (i : ι), s i),
                                              ZeroHom.toFun (↑src) (x + y) =
                                                ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                    map_smul' :=
                                      (_ :
                                        ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                φ₂) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (φ₂ : MultilinearMap R s E),
                      AddHom.toFun
                          {
                            toFun := fun φ =>
                              let src := liftAux φ;
                              {
                                toAddHom :=
                                  { toFun := src.toFun,
                                    map_add' :=
                                      (_ :
                                        ∀ (x y : ⨂[R] (i : ι), s i),
                                          ZeroHom.toFun (↑src) (x + y) =
                                            ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                map_smul' :=
                                  (_ : ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                            map_add' :=
                              (_ :
                                ∀ (φ₁ φ₂ : MultilinearMap R s E),
                                  (fun φ =>
                                        let src := liftAux φ;
                                        {
                                          toAddHom :=
                                            { toFun := src.toFun,
                                              map_add' :=
                                                (_ :
                                                  ∀ (x y : ⨂[R] (i : ι), s i),
                                                    ZeroHom.toFun (↑src) (x + y) =
                                                      ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                          map_smul' :=
                                            (_ :
                                              ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                      (φ₁ + φ₂) =
                                    (fun φ =>
                                          let src := liftAux φ;
                                          {
                                            toAddHom :=
                                              { toFun := src.toFun,
                                                map_add' :=
                                                  (_ :
                                                    ∀ (x y : ⨂[R] (i : ι), s i),
                                                      ZeroHom.toFun (↑src) (x + y) =
                                                        ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                            map_smul' :=
                                              (_ :
                                                ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                  ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                        φ₁ +
                                      (fun φ =>
                                          let src := liftAux φ;
                                          {
                                            toAddHom :=
                                              { toFun := src.toFun,
                                                map_add' :=
                                                  (_ :
                                                    ∀ (x y : ⨂[R] (i : ι), s i),
                                                      ZeroHom.toFun (↑src) (x + y) =
                                                        ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                            map_smul' :=
                                              (_ :
                                                ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                  ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                        φ₂) }
                          (r • φ₂) =
                        ↑(RingHom.id R) r •
                          AddHom.toFun
                            {
                              toFun := fun φ =>
                                let src := liftAux φ;
                                {
                                  toAddHom :=
                                    { toFun := src.toFun,
                                      map_add' :=
                                        (_ :
                                          ∀ (x y : ⨂[R] (i : ι), s i),
                                            ZeroHom.toFun (↑src) (x + y) =
                                              ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                  map_smul' :=
                                    (_ :
                                      ∀ (r : R) (x : ⨂[R] (i : ι), s i), ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) },
                              map_add' :=
                                (_ :
                                  ∀ (φ₁ φ₂ : MultilinearMap R s E),
                                    (fun φ =>
                                          let src := liftAux φ;
                                          {
                                            toAddHom :=
                                              { toFun := src.toFun,
                                                map_add' :=
                                                  (_ :
                                                    ∀ (x y : ⨂[R] (i : ι), s i),
                                                      ZeroHom.toFun (↑src) (x + y) =
                                                        ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                            map_smul' :=
                                              (_ :
                                                ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                  ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                        (φ₁ + φ₂) =
                                      (fun φ =>
                                            let src := liftAux φ;
                                            {
                                              toAddHom :=
                                                { toFun := src.toFun,
                                                  map_add' :=
                                                    (_ :
                                                      ∀ (x y : ⨂[R] (i : ι), s i),
                                                        ZeroHom.toFun (↑src) (x + y) =
                                                          ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                              map_smul' :=
                                                (_ :
                                                  ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                    ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                          φ₁ +
                                        (fun φ =>
                                            let src := liftAux φ;
                                            {
                                              toAddHom :=
                                                { toFun := src.toFun,
                                                  map_add' :=
                                                    (_ :
                                                      ∀ (x y : ⨂[R] (i : ι), s i),
                                                        ZeroHom.toFun (↑src) (x + y) =
                                                          ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) },
                                              map_smul' :=
                                                (_ :
                                                  ∀ (r : R) (x : ⨂[R] (i : ι), s i),
                                                    ↑(liftAux φ) (r • x) = r • ↑(liftAux φ) x) })
                                          φ₂) }
                            φ₂) }.toAddHom
            ((fun φ' => LinearMap.compMultilinearMap φ' (tprod R)) φ))
          (tprod R))
      x✝ =
    ↑(LinearMap.compMultilinearMap φ (tprod R)) x✝
[PROOFSTEP]
simp [liftAux_tprod]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
⊢ LinearMap.comp (↑lift (domDomCongr e.symm (tprod R))) (↑lift (domDomCongr e (tprod R))) = LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
x✝ : ι₂ → M
⊢ ↑(LinearMap.compMultilinearMap
          (LinearMap.comp (↑lift (domDomCongr e.symm (tprod R))) (↑lift (domDomCongr e (tprod R)))) (tprod R))
      x✝ =
    ↑(LinearMap.compMultilinearMap LinearMap.id (tprod R)) x✝
[PROOFSTEP]
simp only [LinearMap.comp_apply, LinearMap.id_apply, lift_tprod, LinearMap.compMultilinearMap_apply, lift.tprod,
  domDomCongr_apply]
[GOAL]
case H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
x✝ : ι₂ → M
⊢ (⨂ₜ[R] (i : ι₂), x✝ (↑e (↑e.symm i))) = ↑(tprod R) x✝
[PROOFSTEP]
congr
[GOAL]
case H.H.h.e_6.h
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
x✝ : ι₂ → M
⊢ (fun i => x✝ (↑e (↑e.symm i))) = x✝
[PROOFSTEP]
ext
[GOAL]
case H.H.h.e_6.h.h
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
x✝¹ : ι₂ → M
x✝ : ι₂
⊢ x✝¹ (↑e (↑e.symm x✝)) = x✝¹ x✝
[PROOFSTEP]
rw [e.apply_symm_apply]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
⊢ LinearMap.comp (↑lift (domDomCongr e (tprod R))) (↑lift (domDomCongr e.symm (tprod R))) = LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
x✝ : ι → M
⊢ ↑(LinearMap.compMultilinearMap
          (LinearMap.comp (↑lift (domDomCongr e (tprod R))) (↑lift (domDomCongr e.symm (tprod R)))) (tprod R))
      x✝ =
    ↑(LinearMap.compMultilinearMap LinearMap.id (tprod R)) x✝
[PROOFSTEP]
simp only [LinearMap.comp_apply, LinearMap.id_apply, lift_tprod, LinearMap.compMultilinearMap_apply, lift.tprod,
  domDomCongr_apply]
[GOAL]
case H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
x✝ : ι → M
⊢ (⨂ₜ[R] (i : ι), x✝ (↑e.symm (↑e i))) = ↑(tprod R) x✝
[PROOFSTEP]
congr
[GOAL]
case H.H.h.e_6.h
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
x✝ : ι → M
⊢ (fun i => x✝ (↑e.symm (↑e i))) = x✝
[PROOFSTEP]
ext
[GOAL]
case H.H.h.e_6.h.h
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
x✝¹ : ι → M
x✝ : ι
⊢ x✝¹ (↑e.symm (↑e x✝)) = x✝¹ x✝
[PROOFSTEP]
rw [e.symm_apply_apply]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
f : ι → M
⊢ ↑(reindex R M e) (↑(tprod R) f) = ⨂ₜ[R] (i : ι₂), f (↑e.symm i)
[PROOFSTEP]
dsimp [reindex]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
f : ι → M
⊢ ↑(↑lift (domDomCongr e.symm (tprod R))) (↑(tprod R) f) = ⨂ₜ[R] (i : ι₂), f (↑e.symm i)
[PROOFSTEP]
exact liftAux_tprod _ f
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ✝ : MultilinearMap R s E
e : ι ≃ ι₂
φ : MultilinearMap R (fun x => M) E
⊢ LinearMap.comp (↑lift φ) ↑(reindex R M e) = ↑lift (domDomCongr e.symm φ)
[PROOFSTEP]
ext
[GOAL]
case H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ✝ : MultilinearMap R s E
e : ι ≃ ι₂
φ : MultilinearMap R (fun x => M) E
x✝ : ι → M
⊢ ↑(LinearMap.compMultilinearMap (LinearMap.comp (↑lift φ) ↑(reindex R M e)) (tprod R)) x✝ =
    ↑(LinearMap.compMultilinearMap (↑lift (domDomCongr e.symm φ)) (tprod R)) x✝
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
⊢ LinearEquiv.trans (reindex R M e) (reindex R M e') = reindex R M (e.trans e')
[PROOFSTEP]
apply LinearEquiv.toLinearMap_injective
[GOAL]
case a
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
⊢ ↑(LinearEquiv.trans (reindex R M e) (reindex R M e')) = ↑(reindex R M (e.trans e'))
[PROOFSTEP]
ext f
[GOAL]
case a.H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
f : ι → M
⊢ ↑(LinearMap.compMultilinearMap (↑(LinearEquiv.trans (reindex R M e) (reindex R M e'))) (tprod R)) f =
    ↑(LinearMap.compMultilinearMap (↑(reindex R M (e.trans e'))) (tprod R)) f
[PROOFSTEP]
simp only [LinearEquiv.trans_apply, LinearEquiv.coe_coe, reindex_tprod, LinearMap.coe_compMultilinearMap,
  Function.comp_apply, MultilinearMap.domDomCongr_apply, reindex_comp_tprod]
[GOAL]
case a.H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
e : ι ≃ ι₂
e' : ι₂ ≃ ι₃
f : ι → M
⊢ (⨂ₜ[R] (i : ι₃), f (↑e.symm (↑e'.symm i))) = ⨂ₜ[R] (i : ι₃), f (↑(e.trans e').symm i)
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ reindex R M (Equiv.refl ι) = LinearEquiv.refl R (⨂[R] (x : ι), M)
[PROOFSTEP]
apply LinearEquiv.toLinearMap_injective
[GOAL]
case a
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ ↑(reindex R M (Equiv.refl ι)) = ↑(LinearEquiv.refl R (⨂[R] (x : ι), M))
[PROOFSTEP]
ext
[GOAL]
case a.H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
x✝ : ι → M
⊢ ↑(LinearMap.compMultilinearMap (↑(reindex R M (Equiv.refl ι))) (tprod R)) x✝ =
    ↑(LinearMap.compMultilinearMap (↑(LinearEquiv.refl R (⨂[R] (x : ι), M))) (tprod R)) x✝
[PROOFSTEP]
rw [reindex_comp_tprod, LinearEquiv.refl_toLinearMap, Equiv.refl_symm]
[GOAL]
case a.H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
x✝ : ι → M
⊢ ↑(domDomCongr (Equiv.refl ι) (tprod R)) x✝ = ↑(LinearMap.compMultilinearMap LinearMap.id (tprod R)) x✝
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : IsEmpty ι
r : R
x : ⨂[R] (x : ι), M
⊢ AddHom.toFun
      { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
        map_add' :=
          (_ :
            ∀ (x y : ⨂[R] (x : ι), M),
              ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x + ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
          map_add' :=
            (_ :
              ∀ (x y : ⨂[R] (x : ι), M),
                ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                  ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x + ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
        x
[PROOFSTEP]
simp only
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : IsEmpty ι
r : R
x : ⨂[R] (x : ι), M
⊢ ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (r • x) = ↑(RingHom.id R) r • ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x
[PROOFSTEP]
exact LinearMap.map_smul _ r x
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : IsEmpty ι
x : ⨂[R] (x : ι), M
⊢ (fun r => r • ↑(tprod R) isEmptyElim)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                map_add' :=
                  (_ :
                    ∀ (x y : ⨂[R] (x : ι), M),
                      ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                        ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x + ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨂[R] (x : ι), M),
                  AddHom.toFun
                      { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                        map_add' :=
                          (_ :
                            ∀ (x y : ⨂[R] (x : ι), M),
                              ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                  ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                      (r • x) =
                    ↑(RingHom.id R) r •
                      AddHom.toFun
                        { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                          map_add' :=
                            (_ :
                              ∀ (x y : ⨂[R] (x : ι), M),
                                ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                  ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                    ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                        x) }.toAddHom
        x) =
    x
[PROOFSTEP]
refine x.induction_on ?_ ?_
[GOAL]
case refine_1
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : IsEmpty ι
x : ⨂[R] (x : ι), M
⊢ ∀ {r : R} {f : ι → M},
    (fun r => r • ↑(tprod R) isEmptyElim)
        (AddHom.toFun
          {
              toAddHom :=
                { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                  map_add' :=
                    (_ :
                      ∀ (x y : ⨂[R] (x : ι), M),
                        ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                          ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                            ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) },
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : ⨂[R] (x : ι), M),
                    AddHom.toFun
                        { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                          map_add' :=
                            (_ :
                              ∀ (x y : ⨂[R] (x : ι), M),
                                ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                  ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                    ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                        (r • x) =
                      ↑(RingHom.id R) r •
                        AddHom.toFun
                          { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                            map_add' :=
                              (_ :
                                ∀ (x y : ⨂[R] (x : ι), M),
                                  ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                    ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                      ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                          x) }.toAddHom
          (r • ↑(tprod R) f)) =
      r • ↑(tprod R) f
[PROOFSTEP]
intro x y
[GOAL]
case refine_1
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : IsEmpty ι
x✝ : ⨂[R] (x : ι), M
x : R
y : ι → M
⊢ (fun r => r • ↑(tprod R) isEmptyElim)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                map_add' :=
                  (_ :
                    ∀ (x y : ⨂[R] (x : ι), M),
                      ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                        ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x + ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨂[R] (x : ι), M),
                  AddHom.toFun
                      { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                        map_add' :=
                          (_ :
                            ∀ (x y : ⨂[R] (x : ι), M),
                              ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                  ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                      (r • x) =
                    ↑(RingHom.id R) r •
                      AddHom.toFun
                        { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                          map_add' :=
                            (_ :
                              ∀ (x y : ⨂[R] (x : ι), M),
                                ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                  ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                    ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                        x) }.toAddHom
        (x • ↑(tprod R) y)) =
    x • ↑(tprod R) y
[PROOFSTEP]
simp only [map_smulₛₗ, RingHom.id_apply, lift.tprod, constOfIsEmpty_apply, const_apply, smul_eq_mul, mul_one]
[GOAL]
case refine_1
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : IsEmpty ι
x✝ : ⨂[R] (x : ι), M
x : R
y : ι → M
⊢ x • ↑(tprod R) isEmptyElim = x • ↑(tprod R) y
[PROOFSTEP]
congr
[GOAL]
case refine_1.e_a.h.e_6.h
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : IsEmpty ι
x✝ : ⨂[R] (x : ι), M
x : R
y : ι → M
⊢ isEmptyElim = y
[PROOFSTEP]
aesop
[GOAL]
case refine_2
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : IsEmpty ι
x : ⨂[R] (x : ι), M
⊢ ∀ {x y : ⨂[R] (i : ι), M},
    (fun r => r • ↑(tprod R) isEmptyElim)
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                    map_add' :=
                      (_ :
                        ∀ (x y : ⨂[R] (x : ι), M),
                          ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                            ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                              ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : ⨂[R] (x : ι), M),
                      AddHom.toFun
                          { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                            map_add' :=
                              (_ :
                                ∀ (x y : ⨂[R] (x : ι), M),
                                  ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                    ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                      ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                          (r • x) =
                        ↑(RingHom.id R) r •
                          AddHom.toFun
                            { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                              map_add' :=
                                (_ :
                                  ∀ (x y : ⨂[R] (x : ι), M),
                                    ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                      ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                        ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                            x) }.toAddHom
            x) =
        x →
      (fun r => r • ↑(tprod R) isEmptyElim)
            (AddHom.toFun
              {
                  toAddHom :=
                    { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                      map_add' :=
                        (_ :
                          ∀ (x y : ⨂[R] (x : ι), M),
                            ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                              ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) },
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : ⨂[R] (x : ι), M),
                        AddHom.toFun
                            { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                              map_add' :=
                                (_ :
                                  ∀ (x y : ⨂[R] (x : ι), M),
                                    ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                      ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                        ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                            (r • x) =
                          ↑(RingHom.id R) r •
                            AddHom.toFun
                              { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ⨂[R] (x : ι), M),
                                      ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                        ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                          ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                              x) }.toAddHom
              y) =
          y →
        (fun r => r • ↑(tprod R) isEmptyElim)
            (AddHom.toFun
              {
                  toAddHom :=
                    { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                      map_add' :=
                        (_ :
                          ∀ (x y : ⨂[R] (x : ι), M),
                            ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                              ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) },
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : ⨂[R] (x : ι), M),
                        AddHom.toFun
                            { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                              map_add' :=
                                (_ :
                                  ∀ (x y : ⨂[R] (x : ι), M),
                                    ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                      ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                        ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                            (r • x) =
                          ↑(RingHom.id R) r •
                            AddHom.toFun
                              { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ⨂[R] (x : ι), M),
                                      ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                        ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                          ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                              x) }.toAddHom
              (x + y)) =
          x + y
[PROOFSTEP]
simp only
[GOAL]
case refine_2
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : IsEmpty ι
x : ⨂[R] (x : ι), M
⊢ ∀ {x y : ⨂[R] (i : ι), M},
    ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x • ↑(tprod R) isEmptyElim = x →
      ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y • ↑(tprod R) isEmptyElim = y →
        ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) • ↑(tprod R) isEmptyElim = x + y
[PROOFSTEP]
intro x y hx hy
[GOAL]
case refine_2
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : IsEmpty ι
x✝ x y : ⨂[R] (i : ι), M
hx : ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x • ↑(tprod R) isEmptyElim = x
hy : ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y • ↑(tprod R) isEmptyElim = y
⊢ ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) • ↑(tprod R) isEmptyElim = x + y
[PROOFSTEP]
rw [map_add, add_smul, hx, hy]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : IsEmpty ι
t : R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
              map_add' :=
                (_ :
                  ∀ (x y : ⨂[R] (x : ι), M),
                    ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                      ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x + ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : ⨂[R] (x : ι), M),
                AddHom.toFun
                    { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                      map_add' :=
                        (_ :
                          ∀ (x y : ⨂[R] (x : ι), M),
                            ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                              ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                    (r • x) =
                  ↑(RingHom.id R) r •
                    AddHom.toFun
                      { toFun := ↑(↑lift (constOfIsEmpty R (fun i => M) 1)),
                        map_add' :=
                          (_ :
                            ∀ (x y : ⨂[R] (x : ι), M),
                              ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) (x + y) =
                                ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) x +
                                  ↑(↑lift (constOfIsEmpty R (fun i => M) 1)) y) }
                      x) }.toAddHom
      ((fun r => r • ↑(tprod R) isEmptyElim) t) =
    t
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
r : R
x : ⨂[R] (x : ι), M
⊢ AddHom.toFun
      { toFun := ↑(↑lift (ofSubsingleton R M i₀)),
        map_add' :=
          (_ :
            ∀ (x y : ⨂[R] (x : ι), M),
              ↑(↑lift (ofSubsingleton R M i₀)) (x + y) =
                ↑(↑lift (ofSubsingleton R M i₀)) x + ↑(↑lift (ofSubsingleton R M i₀)) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := ↑(↑lift (ofSubsingleton R M i₀)),
          map_add' :=
            (_ :
              ∀ (x y : ⨂[R] (x : ι), M),
                ↑(↑lift (ofSubsingleton R M i₀)) (x + y) =
                  ↑(↑lift (ofSubsingleton R M i₀)) x + ↑(↑lift (ofSubsingleton R M i₀)) y) }
        x
[PROOFSTEP]
simp only
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
r : R
x : ⨂[R] (x : ι), M
⊢ ↑(↑lift (ofSubsingleton R M i₀)) (r • x) = ↑(RingHom.id R) r • ↑(↑lift (ofSubsingleton R M i₀)) x
[PROOFSTEP]
exact LinearMap.map_smul _ r x
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
x : ⨂[R] (x : ι), M
⊢ (fun m => ⨂ₜ[R] (x : ι), m)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(↑lift (ofSubsingleton R M i₀)),
                map_add' :=
                  (_ :
                    ∀ (x y : ⨂[R] (x : ι), M),
                      ↑(↑lift (ofSubsingleton R M i₀)) (x + y) =
                        ↑(↑lift (ofSubsingleton R M i₀)) x + ↑(↑lift (ofSubsingleton R M i₀)) y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : ⨂[R] (x : ι), M),
                  AddHom.toFun
                      { toFun := ↑(↑lift (ofSubsingleton R M i₀)),
                        map_add' :=
                          (_ :
                            ∀ (x y : ⨂[R] (x : ι), M),
                              ↑(↑lift (ofSubsingleton R M i₀)) (x + y) =
                                ↑(↑lift (ofSubsingleton R M i₀)) x + ↑(↑lift (ofSubsingleton R M i₀)) y) }
                      (r • x) =
                    ↑(RingHom.id R) r •
                      AddHom.toFun
                        { toFun := ↑(↑lift (ofSubsingleton R M i₀)),
                          map_add' :=
                            (_ :
                              ∀ (x y : ⨂[R] (x : ι), M),
                                ↑(↑lift (ofSubsingleton R M i₀)) (x + y) =
                                  ↑(↑lift (ofSubsingleton R M i₀)) x + ↑(↑lift (ofSubsingleton R M i₀)) y) }
                        x) }.toAddHom
        x) =
    x
[PROOFSTEP]
dsimp only
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
x : ⨂[R] (x : ι), M
⊢ (⨂ₜ[R] (x_1 : ι), ↑(↑lift (ofSubsingleton R M i₀)) x) = x
[PROOFSTEP]
have : ∀ (f : ι → M) (z : M), (fun _ : ι ↦ z) = update f i₀ z :=
  by
  intro f z
  ext i
  rw [Subsingleton.elim i i₀, Function.update_same]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
x : ⨂[R] (x : ι), M
⊢ ∀ (f : ι → M) (z : M), (fun x => z) = update f i₀ z
[PROOFSTEP]
intro f z
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
x : ⨂[R] (x : ι), M
f : ι → M
z : M
⊢ (fun x => z) = update f i₀ z
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
x : ⨂[R] (x : ι), M
f : ι → M
z : M
i : ι
⊢ z = update f i₀ z i
[PROOFSTEP]
rw [Subsingleton.elim i i₀, Function.update_same]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
x : ⨂[R] (x : ι), M
this : ∀ (f : ι → M) (z : M), (fun x => z) = update f i₀ z
⊢ (⨂ₜ[R] (x_1 : ι), ↑(↑lift (ofSubsingleton R M i₀)) x) = x
[PROOFSTEP]
refine x.induction_on ?_ ?_
[GOAL]
case refine_1
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
x : ⨂[R] (x : ι), M
this : ∀ (f : ι → M) (z : M), (fun x => z) = update f i₀ z
⊢ ∀ {r : R} {f : ι → M}, (⨂ₜ[R] (x : ι), ↑(↑lift (ofSubsingleton R M i₀)) (r • ↑(tprod R) f)) = r • ↑(tprod R) f
[PROOFSTEP]
intro r f
[GOAL]
case refine_1
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
x : ⨂[R] (x : ι), M
this : ∀ (f : ι → M) (z : M), (fun x => z) = update f i₀ z
r : R
f : ι → M
⊢ (⨂ₜ[R] (x : ι), ↑(↑lift (ofSubsingleton R M i₀)) (r • ↑(tprod R) f)) = r • ↑(tprod R) f
[PROOFSTEP]
simp only [LinearMap.map_smul, lift.tprod, ofSubsingleton_apply, Function.eval, this f, MultilinearMap.map_smul,
  update_eq_self]
[GOAL]
case refine_2
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
x : ⨂[R] (x : ι), M
this : ∀ (f : ι → M) (z : M), (fun x => z) = update f i₀ z
⊢ ∀ {x y : ⨂[R] (i : ι), M},
    (⨂ₜ[R] (x_1 : ι), ↑(↑lift (ofSubsingleton R M i₀)) x) = x →
      (⨂ₜ[R] (x : ι), ↑(↑lift (ofSubsingleton R M i₀)) y) = y →
        (⨂ₜ[R] (x_1 : ι), ↑(↑lift (ofSubsingleton R M i₀)) (x + y)) = x + y
[PROOFSTEP]
intro x y hx hy
[GOAL]
case refine_2
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
x✝ : ⨂[R] (x : ι), M
this : ∀ (f : ι → M) (z : M), (fun x => z) = update f i₀ z
x y : ⨂[R] (i : ι), M
hx : (⨂ₜ[R] (x_1 : ι), ↑(↑lift (ofSubsingleton R M i₀)) x) = x
hy : (⨂ₜ[R] (x : ι), ↑(↑lift (ofSubsingleton R M i₀)) y) = y
⊢ (⨂ₜ[R] (x_1 : ι), ↑(↑lift (ofSubsingleton R M i₀)) (x + y)) = x + y
[PROOFSTEP]
rw [LinearMap.map_add, this 0 (_ + _), MultilinearMap.map_add, ← this 0 (lift _ _), hx, ← this 0 (lift _ _), hy]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁸ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁷ : (i : ι) → AddCommMonoid (s i)
inst✝⁶ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
E : Type u_9
inst✝³ : AddCommMonoid E
inst✝² : Module R E
F : Type u_10
inst✝¹ : AddCommMonoid F
φ : MultilinearMap R s E
inst✝ : Subsingleton ι
i₀ : ι
t : M
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(↑lift (ofSubsingleton R M i₀)),
              map_add' :=
                (_ :
                  ∀ (x y : ⨂[R] (x : ι), M),
                    ↑(↑lift (ofSubsingleton R M i₀)) (x + y) =
                      ↑(↑lift (ofSubsingleton R M i₀)) x + ↑(↑lift (ofSubsingleton R M i₀)) y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : ⨂[R] (x : ι), M),
                AddHom.toFun
                    { toFun := ↑(↑lift (ofSubsingleton R M i₀)),
                      map_add' :=
                        (_ :
                          ∀ (x y : ⨂[R] (x : ι), M),
                            ↑(↑lift (ofSubsingleton R M i₀)) (x + y) =
                              ↑(↑lift (ofSubsingleton R M i₀)) x + ↑(↑lift (ofSubsingleton R M i₀)) y) }
                    (r • x) =
                  ↑(RingHom.id R) r •
                    AddHom.toFun
                      { toFun := ↑(↑lift (ofSubsingleton R M i₀)),
                        map_add' :=
                          (_ :
                            ∀ (x y : ⨂[R] (x : ι), M),
                              ↑(↑lift (ofSubsingleton R M i₀)) (x + y) =
                                ↑(↑lift (ofSubsingleton R M i₀)) x + ↑(↑lift (ofSubsingleton R M i₀)) y) }
                      x) }.toAddHom
      ((fun m => ⨂ₜ[R] (x : ι), m) t) =
    t
[PROOFSTEP]
simp only [ofSubsingleton_apply, lift.tprod, Function.eval_apply]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
a b : ⨂[R] (x : ι), M
⊢ (fun a => ↑lift (↑(↑lift (↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R))) a)) (a + b) =
    (fun a => ↑lift (↑(↑lift (↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R))) a)) a +
      (fun a => ↑lift (↑(↑lift (↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R))) a)) b
[PROOFSTEP]
simp only [LinearEquiv.map_add, LinearMap.map_add]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
r : R
a : ⨂[R] (x : ι), M
⊢ AddHom.toFun
      { toFun := fun a => ↑lift (↑(↑lift (↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R))) a),
        map_add' :=
          (_ :
            ∀ (a b : ⨂[R] (x : ι), M),
              ↑lift (↑(↑lift (↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R))) (a + b)) =
                ↑lift (↑(↑lift (↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R))) a) +
                  ↑lift (↑(↑lift (↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R))) b)) }
      (r • a) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun a => ↑lift (↑(↑lift (↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R))) a),
          map_add' :=
            (_ :
              ∀ (a b : ⨂[R] (x : ι), M),
                ↑lift (↑(↑lift (↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R))) (a + b)) =
                  ↑lift (↑(↑lift (↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R))) a) +
                    ↑lift (↑(↑lift (↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R))) b)) }
        a
[PROOFSTEP]
simp only [LinearEquiv.map_smul, LinearMap.map_smul, RingHom.id_apply]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
a : ι → M
b : ι₂ → M
⊢ ↑PiTensorProduct.tmul ((⨂ₜ[R] (i : ι), a i) ⊗ₜ[R] ⨂ₜ[R] (i : ι₂), b i) = ⨂ₜ[R] (i : ι ⊕ ι₂), Sum.elim a b i
[PROOFSTEP]
erw [TensorProduct.lift.tmul, PiTensorProduct.lift.tprod, PiTensorProduct.lift.tprod]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
a : ι → M
b : ι₂ → M
⊢ (↑(↑(↑(currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R)) fun i => a i) fun i => b i) =
    ⨂ₜ[R] (i : ι ⊕ ι₂), Sum.elim a b i
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ LinearMap.comp PiTensorProduct.tmul PiTensorProduct.tmulSymm = LinearMap.id
[PROOFSTEP]
ext x
[GOAL]
case H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
x : ι ⊕ ι₂ → M
⊢ ↑(LinearMap.compMultilinearMap (LinearMap.comp PiTensorProduct.tmul PiTensorProduct.tmulSymm) (tprod R)) x =
    ↑(LinearMap.compMultilinearMap LinearMap.id (tprod R)) x
[PROOFSTEP]
show tmul (tmulSymm (tprod R x)) = tprod R x
[GOAL]
case H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
x : ι ⊕ ι₂ → M
⊢ ↑PiTensorProduct.tmul (↑PiTensorProduct.tmulSymm (↑(tprod R) x)) = ↑(tprod R) x
[PROOFSTEP]
simp only [tmulSymm_apply, tmul_apply]
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/5026):
        -- was part of `simp only` above
[GOAL]
case H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
x : ι ⊕ ι₂ → M
⊢ (⨂ₜ[R] (i : ι ⊕ ι₂), Sum.elim (fun i => x (Sum.inl i)) (fun i => x (Sum.inr i)) i) = ↑(tprod R) x
[PROOFSTEP]
erw [Sum.elim_comp_inl_inr]
[GOAL]
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
⊢ LinearMap.comp PiTensorProduct.tmulSymm PiTensorProduct.tmul = LinearMap.id
[PROOFSTEP]
ext x y
[GOAL]
case H.H.H.H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
x : ι → M
y : ι₂ → M
⊢ ↑(LinearMap.compMultilinearMap
          (↑(LinearMap.compMultilinearMap
                (LinearMap.compr₂ (TensorProduct.mk R (⨂[R] (x : ι), M) (⨂[R] (x : ι₂), M))
                  (LinearMap.comp PiTensorProduct.tmulSymm PiTensorProduct.tmul))
                (tprod R))
            x)
          (tprod R))
      y =
    ↑(LinearMap.compMultilinearMap
          (↑(LinearMap.compMultilinearMap
                (LinearMap.compr₂ (TensorProduct.mk R (⨂[R] (x : ι), M) (⨂[R] (x : ι₂), M)) LinearMap.id) (tprod R))
            x)
          (tprod R))
      y
[PROOFSTEP]
show tmulSymm (tmul (tprod R x ⊗ₜ[R] tprod R y)) = tprod R x ⊗ₜ[R] tprod R y
[GOAL]
case H.H.H.H.H
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
x : ι → M
y : ι₂ → M
⊢ ↑PiTensorProduct.tmulSymm (↑PiTensorProduct.tmul (↑(tprod R) x ⊗ₜ[R] ↑(tprod R) y)) = ↑(tprod R) x ⊗ₜ[R] ↑(tprod R) y
[PROOFSTEP]
simp only [tmul_apply, tmulSymm_apply, Sum.elim_inl, Sum.elim_inr]
