-- Mathlib/LinearAlgebra/Dual.lean
theorem dualDistrib_dualDistribInvOfBasis_left_inverse (b : Basis ι R M) (c : Basis κ R N) :
    comp (dualDistrib R M N) (dualDistribInvOfBasis b c) = LinearMap.id

Proof state:
case mk.mk
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ((dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis (i, j)))
      ((b.tensorProduct c) (i', j')) =
    (LinearMap.id ((b.tensorProduct c).dualBasis (i, j))) ((b.tensorProduct c) (i', j'))

Tactic:
simp only [dualDistrib, Basis.coe_dualBasis, coe_comp, Function.comp_apply,
  dualDistribInvOfBasis_apply, Basis.coord_apply, Basis.tensorProduct_repr_tmul_apply,
  Basis.repr_self, ne_eq, _root_.map_sum, map_smul, homTensorHomMap_apply, compRight_apply,
  Basis.tensorProduct_apply, coeFn_sum, Finset.sum_apply, smul_apply, LinearEquiv.coe_coe,
  map_tmul, lid_tmul, smul_eq_mul, id_coe, id_eq]

Result:
case mk.mk
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∑ x : ι,
      ∑ x_1 : κ,
        (Finsupp.single x_1 1) j * (Finsupp.single x 1) i * ((Finsupp.single i' 1) x * (Finsupp.single j' 1) x_1) =
    (Finsupp.single j' 1) j * (Finsupp.single i' 1) i

Proof state:
case mk.mk
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∑ x : ι,
      ∑ x_1 : κ,
        (Finsupp.single x_1 1) j * (Finsupp.single x 1) i * ((Finsupp.single i' 1) x * (Finsupp.single j' 1) x_1) =
    (Finsupp.single j' 1) j * (Finsupp.single i' 1) i

Tactic:
rw [Finset.sum_eq_single i, Finset.sum_eq_single j]

Result:
case mk.mk
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ (Finsupp.single j 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) j) =
    (Finsupp.single j' 1) j * (Finsupp.single i' 1) i

case mk.mk.h₀
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ b ∈ Finset.univ,
    b ≠ j → (Finsupp.single b 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) b) = 0

case mk.mk.h₁
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ j ∉ Finset.univ →
    (Finsupp.single j 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) j) = 0

case mk.mk.h₀
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ b ∈ Finset.univ,
    b ≠ i →
      ∑ x : κ, (Finsupp.single x 1) j * (Finsupp.single b 1) i * ((Finsupp.single i' 1) b * (Finsupp.single j' 1) x) = 0

case mk.mk.h₁
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ i ∉ Finset.univ →
    ∑ x : κ, (Finsupp.single x 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) x) = 0

Proof state:
case mk.mk
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ (Finsupp.single j 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) j) =
    (Finsupp.single j' 1) j * (Finsupp.single i' 1) i

Tactic:
simpa using mul_comm _ _

Result:
no goals