[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
m : M
⊢ ↑Dual.transpose (↑(dualTensorHom R M M) (f ⊗ₜ[R] m)) =
    ↑(dualTensorHom R (Dual R M) (Dual R M)) (↑(Dual.eval R M) m ⊗ₜ[R] f)
[PROOFSTEP]
ext f' m'
[GOAL]
case h.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
m : M
f' : Dual R M
m' : M
⊢ ↑(↑(↑Dual.transpose (↑(dualTensorHom R M M) (f ⊗ₜ[R] m))) f') m' =
    ↑(↑(↑(dualTensorHom R (Dual R M) (Dual R M)) (↑(Dual.eval R M) m ⊗ₜ[R] f)) f') m'
[PROOFSTEP]
simp only [Dual.transpose_apply, coe_comp, Function.comp_apply, dualTensorHom_apply, LinearMap.map_smulₛₗ,
  RingHom.id_apply, Algebra.id.smul_eq_mul, Dual.eval_apply, LinearMap.smul_apply]
[GOAL]
case h.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
m : M
f' : Dual R M
m' : M
⊢ ↑f m' * ↑f' m = ↑f' m * ↑f m'
[PROOFSTEP]
exact mul_comm _ _
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
p : P
⊢ prodMap (↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) 0 =
    ↑(dualTensorHom R (M × N) (P × Q)) (comp f (fst R M N) ⊗ₜ[R] ↑(inl R P Q) p)
[PROOFSTEP]
ext
[GOAL]
case hl.h.h₁
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
p : P
x✝ : M
⊢ (↑(comp (prodMap (↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) 0) (inl R M N)) x✝).fst =
    (↑(comp (↑(dualTensorHom R (M × N) (P × Q)) (comp f (fst R M N) ⊗ₜ[R] ↑(inl R P Q) p)) (inl R M N)) x✝).fst
[PROOFSTEP]
simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply, fst_apply, Prod.smul_mk,
  LinearMap.zero_apply, smul_zero]
[GOAL]
case hl.h.h₂
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
p : P
x✝ : M
⊢ (↑(comp (prodMap (↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) 0) (inl R M N)) x✝).snd =
    (↑(comp (↑(dualTensorHom R (M × N) (P × Q)) (comp f (fst R M N) ⊗ₜ[R] ↑(inl R P Q) p)) (inl R M N)) x✝).snd
[PROOFSTEP]
simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply, fst_apply, Prod.smul_mk,
  LinearMap.zero_apply, smul_zero]
[GOAL]
case hr.h.h₁
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
p : P
x✝ : N
⊢ (↑(comp (prodMap (↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) 0) (inr R M N)) x✝).fst =
    (↑(comp (↑(dualTensorHom R (M × N) (P × Q)) (comp f (fst R M N) ⊗ₜ[R] ↑(inl R P Q) p)) (inr R M N)) x✝).fst
[PROOFSTEP]
simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply, fst_apply, Prod.smul_mk,
  LinearMap.zero_apply, smul_zero]
[GOAL]
case hr.h.h₂
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
p : P
x✝ : N
⊢ (↑(comp (prodMap (↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) 0) (inr R M N)) x✝).snd =
    (↑(comp (↑(dualTensorHom R (M × N) (P × Q)) (comp f (fst R M N) ⊗ₜ[R] ↑(inl R P Q) p)) (inr R M N)) x✝).snd
[PROOFSTEP]
simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply, fst_apply, Prod.smul_mk,
  LinearMap.zero_apply, smul_zero]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
g : Dual R N
q : Q
⊢ prodMap 0 (↑(dualTensorHom R N Q) (g ⊗ₜ[R] q)) =
    ↑(dualTensorHom R (M × N) (P × Q)) (comp g (snd R M N) ⊗ₜ[R] ↑(inr R P Q) q)
[PROOFSTEP]
ext
[GOAL]
case hl.h.h₁
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
g : Dual R N
q : Q
x✝ : M
⊢ (↑(comp (prodMap 0 (↑(dualTensorHom R N Q) (g ⊗ₜ[R] q))) (inl R M N)) x✝).fst =
    (↑(comp (↑(dualTensorHom R (M × N) (P × Q)) (comp g (snd R M N) ⊗ₜ[R] ↑(inr R P Q) q)) (inl R M N)) x✝).fst
[PROOFSTEP]
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply, snd_apply, Prod.smul_mk,
  LinearMap.zero_apply, smul_zero]
[GOAL]
case hl.h.h₂
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
g : Dual R N
q : Q
x✝ : M
⊢ (↑(comp (prodMap 0 (↑(dualTensorHom R N Q) (g ⊗ₜ[R] q))) (inl R M N)) x✝).snd =
    (↑(comp (↑(dualTensorHom R (M × N) (P × Q)) (comp g (snd R M N) ⊗ₜ[R] ↑(inr R P Q) q)) (inl R M N)) x✝).snd
[PROOFSTEP]
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply, snd_apply, Prod.smul_mk,
  LinearMap.zero_apply, smul_zero]
[GOAL]
case hr.h.h₁
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
g : Dual R N
q : Q
x✝ : N
⊢ (↑(comp (prodMap 0 (↑(dualTensorHom R N Q) (g ⊗ₜ[R] q))) (inr R M N)) x✝).fst =
    (↑(comp (↑(dualTensorHom R (M × N) (P × Q)) (comp g (snd R M N) ⊗ₜ[R] ↑(inr R P Q) q)) (inr R M N)) x✝).fst
[PROOFSTEP]
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply, snd_apply, Prod.smul_mk,
  LinearMap.zero_apply, smul_zero]
[GOAL]
case hr.h.h₂
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
g : Dual R N
q : Q
x✝ : N
⊢ (↑(comp (prodMap 0 (↑(dualTensorHom R N Q) (g ⊗ₜ[R] q))) (inr R M N)) x✝).snd =
    (↑(comp (↑(dualTensorHom R (M × N) (P × Q)) (comp g (snd R M N) ⊗ₜ[R] ↑(inr R P Q) q)) (inr R M N)) x✝).snd
[PROOFSTEP]
simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply, snd_apply, Prod.smul_mk,
  LinearMap.zero_apply, smul_zero]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
p : P
g : Dual R N
q : Q
⊢ TensorProduct.map (↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) (↑(dualTensorHom R N Q) (g ⊗ₜ[R] q)) =
    ↑(dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q)) (↑(dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] p ⊗ₜ[R] q)
[PROOFSTEP]
ext m n
[GOAL]
case H.h.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
p : P
g : Dual R N
q : Q
m : M
n : N
⊢ ↑(↑(compr₂ (TensorProduct.mk R M N)
              (TensorProduct.map (↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) (↑(dualTensorHom R N Q) (g ⊗ₜ[R] q))))
          m)
      n =
    ↑(↑(compr₂ (TensorProduct.mk R M N)
              (↑(dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q)) (↑(dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] p ⊗ₜ[R] q)))
          m)
      n
[PROOFSTEP]
simp only [compr₂_apply, mk_apply, map_tmul, dualTensorHom_apply, dualDistrib_apply, ← smul_tmul_smul]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
n : N
g : Dual R N
p : P
⊢ comp (↑(dualTensorHom R N P) (g ⊗ₜ[R] p)) (↑(dualTensorHom R M N) (f ⊗ₜ[R] n)) =
    ↑g n • ↑(dualTensorHom R M P) (f ⊗ₜ[R] p)
[PROOFSTEP]
ext m
[GOAL]
case h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ ↑(comp (↑(dualTensorHom R N P) (g ⊗ₜ[R] p)) (↑(dualTensorHom R M N) (f ⊗ₜ[R] n))) m =
    ↑(↑g n • ↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) m
[PROOFSTEP]
simp only [coe_comp, Function.comp_apply, dualTensorHom_apply, LinearMap.map_smul, RingHom.id_apply,
  LinearMap.smul_apply]
[GOAL]
case h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ ↑f m • ↑g n • p = ↑g n • ↑f m • p
[PROOFSTEP]
rw [smul_comm]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i : n
⊢ ↑(toMatrix bM bN) (↑(dualTensorHom R M N) (Basis.coord bM j ⊗ₜ[R] ↑bN i)) = stdBasisMatrix i j 1
[PROOFSTEP]
ext i' j'
[GOAL]
case a.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
⊢ ↑(toMatrix bM bN) (↑(dualTensorHom R M N) (Basis.coord bM j ⊗ₜ[R] ↑bN i)) i' j' = stdBasisMatrix i j 1 i' j'
[PROOFSTEP]
by_cases hij : i = i' ∧ j = j'
[GOAL]
case pos
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : i = i' ∧ j = j'
⊢ ↑(toMatrix bM bN) (↑(dualTensorHom R M N) (Basis.coord bM j ⊗ₜ[R] ↑bN i)) i' j' = stdBasisMatrix i j 1 i' j'
[PROOFSTEP]
simp [LinearMap.toMatrix_apply, Finsupp.single_eq_pi_single, hij]
[GOAL]
case neg
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬(i = i' ∧ j = j')
⊢ ↑(toMatrix bM bN) (↑(dualTensorHom R M N) (Basis.coord bM j ⊗ₜ[R] ↑bN i)) i' j' = stdBasisMatrix i j 1 i' j'
[PROOFSTEP]
simp [LinearMap.toMatrix_apply, Finsupp.single_eq_pi_single, hij]
[GOAL]
case neg
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬(i = i' ∧ j = j')
⊢ Pi.single i (Pi.single j' 1 j) i' = 0
[PROOFSTEP]
rw [and_iff_not_or_not, Classical.not_not] at hij 
[GOAL]
case neg
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i' ∨ ¬j = j'
⊢ Pi.single i (Pi.single j' 1 j) i' = 0
[PROOFSTEP]
cases' hij with hij hij
[GOAL]
case neg.inl
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i'
⊢ Pi.single i (Pi.single j' 1 j) i' = 0
[PROOFSTEP]
simp [hij]
[GOAL]
case neg.inr
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬j = j'
⊢ Pi.single i (Pi.single j' 1 j) i' = 0
[PROOFSTEP]
simp [hij]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
⊢ comp (dualTensorHom R M N)
      (∑ i : ι, comp (↑(TensorProduct.mk R ((fun x => Dual R M) i) N) (↑(Basis.dualBasis b) i)) (↑applyₗ (↑b i))) =
    LinearMap.id
[PROOFSTEP]
ext f m
[GOAL]
case h.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M →ₗ[R] N
m : M
⊢ ↑(↑(comp (dualTensorHom R M N)
              (∑ i : ι,
                comp (↑(TensorProduct.mk R ((fun x => Dual R M) i) N) (↑(Basis.dualBasis b) i)) (↑applyₗ (↑b i))))
          f)
      m =
    ↑(↑LinearMap.id f) m
[PROOFSTEP]
simp only [applyₗ_apply_apply, coeFn_sum, dualTensorHom_apply, mk_apply, id_coe, id.def, Fintype.sum_apply,
  Function.comp_apply, Basis.coe_dualBasis, coe_comp, Basis.coord_apply, ← f.map_smul, (dualTensorHom R M N).map_sum, ←
  f.map_sum, b.sum_repr]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
⊢ comp (∑ i : ι, comp (↑(TensorProduct.mk R ((fun x => Dual R M) i) N) (↑(Basis.dualBasis b) i)) (↑applyₗ (↑b i)))
      (dualTensorHom R M N) =
    LinearMap.id
[PROOFSTEP]
ext f m
[GOAL]
case H.h.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
m : N
⊢ ↑(↑(compr₂ (TensorProduct.mk R (Dual R M) N)
              (comp
                (∑ i : ι,
                  comp (↑(TensorProduct.mk R ((fun x => Dual R M) i) N) (↑(Basis.dualBasis b) i)) (↑applyₗ (↑b i)))
                (dualTensorHom R M N)))
          f)
      m =
    ↑(↑(compr₂ (TensorProduct.mk R (Dual R M) N) LinearMap.id) f) m
[PROOFSTEP]
simp only [applyₗ_apply_apply, coeFn_sum, dualTensorHom_apply, mk_apply, id_coe, id.def, Fintype.sum_apply,
  Function.comp_apply, Basis.coe_dualBasis, coe_comp, compr₂_apply, tmul_smul, smul_tmul', ← sum_tmul,
  Basis.sum_dual_apply_smul_coord]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
⊢ ↑(dualTensorHomEquivOfBasis b) x = ↑(dualTensorHom R M N) x
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
x✝ : M
⊢ ↑(↑(dualTensorHomEquivOfBasis b) x) x✝ = ↑(↑(dualTensorHom R M N) x) x✝
[PROOFSTEP]
rfl
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
⊢ ↑(LinearEquiv.symm (dualTensorHomEquivOfBasis b)) (↑(dualTensorHom R M N) x) = x
[PROOFSTEP]
rw [← dualTensorHomEquivOfBasis_apply b, LinearEquiv.symm_apply_apply <| dualTensorHomEquivOfBasis (N := N) b]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
x : M →ₗ[R] N
⊢ ↑(dualTensorHom R M N) (↑(LinearEquiv.symm (dualTensorHomEquivOfBasis b)) x) = x
[PROOFSTEP]
rw [← dualTensorHomEquivOfBasis_apply b, LinearEquiv.apply_symm_apply]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor R M P Q
[PROOFSTEP]
classical
  -- Porting note: missing decidable for choosing basis
let e := congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
have h : Function.Surjective e.toLinearMap := e.surjective
refine' (cancel_right h).1 _
ext f q m
dsimp [lTensorHomEquivHomLTensor]
simp only [lTensorHomEquivHomLTensor, dualTensorHomEquiv, compr₂_apply, mk_apply, coe_comp, LinearEquiv.coe_toLinearMap,
  Function.comp_apply, map_tmul, LinearEquiv.coe_coe, dualTensorHomEquivOfBasis_apply, LinearEquiv.trans_apply,
  congr_tmul, LinearEquiv.refl_apply, dualTensorHomEquivOfBasis_symm_cancel_left, leftComm_tmul, dualTensorHom_apply,
  tmul_smul]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor R M P Q
[PROOFSTEP]
let e := congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : P ⊗[R] Dual R M ⊗[R] Q ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor R M P Q
[PROOFSTEP]
have h : Function.Surjective e.toLinearMap := e.surjective
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : P ⊗[R] Dual R M ⊗[R] Q ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
h : Function.Surjective ↑↑e
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor R M P Q
[PROOFSTEP]
refine' (cancel_right h).1 _
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : P ⊗[R] Dual R M ⊗[R] Q ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
h : Function.Surjective ↑↑e
⊢ comp ↑(lTensorHomEquivHomLTensor R M P Q) ↑e = comp (lTensorHomToHomLTensor R M P Q) ↑e
[PROOFSTEP]
ext f q m
[GOAL]
case H.h.H.h.h.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : P ⊗[R] Dual R M ⊗[R] Q ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
h : Function.Surjective ↑↑e
f : P
q : Dual R M
m : Q
x✝ : M
⊢ ↑(↑(↑(compr₂ (TensorProduct.mk R (Dual R M) Q)
                  (↑(compr₂ (TensorProduct.mk R P (Dual R M ⊗[R] Q)) (comp ↑(lTensorHomEquivHomLTensor R M P Q) ↑e)) f))
              q)
          m)
      x✝ =
    ↑(↑(↑(compr₂ (TensorProduct.mk R (Dual R M) Q)
                  (↑(compr₂ (TensorProduct.mk R P (Dual R M ⊗[R] Q)) (comp (lTensorHomToHomLTensor R M P Q) ↑e)) f))
              q)
          m)
      x✝
[PROOFSTEP]
dsimp [lTensorHomEquivHomLTensor]
[GOAL]
case H.h.H.h.h.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : P ⊗[R] Dual R M ⊗[R] Q ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
h : Function.Surjective ↑↑e
f : P
q : Dual R M
m : Q
x✝ : M
⊢ ↑(↑(dualTensorHomEquivOfBasis (Free.chooseBasis R M))
          (↑(leftComm R P (Dual R M) Q)
            (f ⊗ₜ[R]
              ↑(LinearEquiv.symm (dualTensorHomEquivOfBasis (Free.chooseBasis R M)))
                (↑(dualTensorHomEquivOfBasis (Free.chooseBasis R M)) (q ⊗ₜ[R] m)))))
      x✝ =
    f ⊗ₜ[R] ↑(↑(dualTensorHomEquivOfBasis (Free.chooseBasis R M)) (q ⊗ₜ[R] m)) x✝
[PROOFSTEP]
simp only [lTensorHomEquivHomLTensor, dualTensorHomEquiv, compr₂_apply, mk_apply, coe_comp, LinearEquiv.coe_toLinearMap,
  Function.comp_apply, map_tmul, LinearEquiv.coe_coe, dualTensorHomEquivOfBasis_apply, LinearEquiv.trans_apply,
  congr_tmul, LinearEquiv.refl_apply, dualTensorHomEquivOfBasis_symm_cancel_left, leftComm_tmul, dualTensorHom_apply,
  tmul_smul]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor R M P Q
[PROOFSTEP]
classical
  -- Porting note: missing decidable for choosing basis
let e := congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
have h : Function.Surjective e.toLinearMap := e.surjective
refine' (cancel_right h).1 _
ext f p q m
simp only [rTensorHomEquivHomRTensor, dualTensorHomEquiv, compr₂_apply, mk_apply, coe_comp, LinearEquiv.coe_toLinearMap,
  Function.comp_apply, map_tmul, LinearEquiv.coe_coe, dualTensorHomEquivOfBasis_apply, LinearEquiv.trans_apply,
  congr_tmul, dualTensorHomEquivOfBasis_symm_cancel_left, LinearEquiv.refl_apply, assoc_tmul, dualTensorHom_apply,
  rTensorHomToHomRTensor_apply, smul_tmul']
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor R M P Q
[PROOFSTEP]
let e := congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : (Dual R M ⊗[R] P) ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor R M P Q
[PROOFSTEP]
have h : Function.Surjective e.toLinearMap := e.surjective
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : (Dual R M ⊗[R] P) ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
h : Function.Surjective ↑↑e
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor R M P Q
[PROOFSTEP]
refine' (cancel_right h).1 _
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : (Dual R M ⊗[R] P) ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
h : Function.Surjective ↑↑e
⊢ comp ↑(rTensorHomEquivHomRTensor R M P Q) ↑e = comp (rTensorHomToHomRTensor R M P Q) ↑e
[PROOFSTEP]
ext f p q m
[GOAL]
case H.H.h.h.h.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : (Dual R M ⊗[R] P) ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
h : Function.Surjective ↑↑e
f : Dual R M
p : P
q : Q
m : M
⊢ ↑(↑(↑(↑(compr₂ (TensorProduct.mk R (Dual R M) P)
                      (compr₂ (TensorProduct.mk R (Dual R M ⊗[R] P) Q) (comp ↑(rTensorHomEquivHomRTensor R M P Q) ↑e)))
                  f)
              p)
          q)
      m =
    ↑(↑(↑(↑(compr₂ (TensorProduct.mk R (Dual R M) P)
                      (compr₂ (TensorProduct.mk R (Dual R M ⊗[R] P) Q) (comp (rTensorHomToHomRTensor R M P Q) ↑e)))
                  f)
              p)
          q)
      m
[PROOFSTEP]
simp only [rTensorHomEquivHomRTensor, dualTensorHomEquiv, compr₂_apply, mk_apply, coe_comp, LinearEquiv.coe_toLinearMap,
  Function.comp_apply, map_tmul, LinearEquiv.coe_coe, dualTensorHomEquivOfBasis_apply, LinearEquiv.trans_apply,
  congr_tmul, dualTensorHomEquivOfBasis_symm_cancel_left, LinearEquiv.refl_apply, assoc_tmul, dualTensorHom_apply,
  rTensorHomToHomRTensor_apply, smul_tmul']
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
x : P ⊗[R] (M →ₗ[R] Q)
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) x = ↑(lTensorHomToHomLTensor R M P Q) x
[PROOFSTEP]
rw [← LinearEquiv.coe_toLinearMap, lTensorHomEquivHomLTensor_toLinearMap]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
x : (M →ₗ[R] P) ⊗[R] Q
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) x = ↑(rTensorHomToHomRTensor R M P Q) x
[PROOFSTEP]
rw [← LinearEquiv.coe_toLinearMap, rTensorHomEquivHomRTensor_toLinearMap]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
⊢ ↑(homTensorHomEquiv R M N P Q) = homTensorHomMap R M N P Q
[PROOFSTEP]
ext m n
[GOAL]
case H.h.h.H.h.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
m : M →ₗ[R] P
n : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ↑(↑(compr₂ (TensorProduct.mk R M N)
              (↑(↑(compr₂ (TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)) ↑(homTensorHomEquiv R M N P Q)) m) n))
          x✝¹)
      x✝ =
    ↑(↑(compr₂ (TensorProduct.mk R M N)
              (↑(↑(compr₂ (TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)) (homTensorHomMap R M N P Q)) m) n))
          x✝¹)
      x✝
[PROOFSTEP]
simp only [homTensorHomEquiv, compr₂_apply, mk_apply, LinearEquiv.coe_toLinearMap, LinearEquiv.trans_apply,
  lift.equiv_apply, LinearEquiv.arrowCongr_apply, LinearEquiv.refl_symm, LinearEquiv.refl_apply,
  rTensorHomEquivHomRTensor_apply, lTensorHomEquivHomLTensor_apply, lTensorHomToHomLTensor_apply,
  rTensorHomToHomRTensor_apply, homTensorHomMap_apply, map_tmul]
[GOAL]
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : AddCommGroup P
inst✝⁹ : AddCommGroup Q
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)
⊢ ↑(homTensorHomEquiv R M N P Q) x = ↑(homTensorHomMap R M N P Q) x
[PROOFSTEP]
rw [← LinearEquiv.coe_toLinearMap, homTensorHomEquiv_toLinearMap]
