-- Mathlib/LinearAlgebra/Contraction.lean
theorem toMatrix_dualTensorHom {m : Type*} {n : Type*} [Fintype m] [Finite n] [DecidableEq m]
    [DecidableEq n] (bM : Basis m R M) (bN : Basis n R N) (j : m) (i : n) :
    toMatrix bM bN (dualTensorHom R M N (bM.coord j ⊗ₜ bN i)) = stdBasisMatrix i j 1

Proof state:
R : Type u
M : Type v₁
N : Type v₂
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Finite 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) (bM.coord j ⊗ₜ[R] bN i)) = stdBasisMatrix i j 1

Tactic:
ext i' j'

Result:
case a
R : Type u
M : Type v₁
N : Type v₂
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Finite 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) (bM.coord j ⊗ₜ[R] bN i)) i' j' = stdBasisMatrix i j 1 i' j'

Proof state:
case a
R : Type u
M : Type v₁
N : Type v₂
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Finite 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) (bM.coord j ⊗ₜ[R] bN i)) i' j' = stdBasisMatrix i j 1 i' j'

Tactic:
by_cases hij : i = i' ∧ j = j' <;>
  simp [LinearMap.toMatrix_apply, Finsupp.single_eq_pi_single, hij]

Result:
case neg
R : Type u
M : Type v₁
N : Type v₂
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Finite 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

Proof state:
case neg
R : Type u
M : Type v₁
N : Type v₂
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Finite 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

Tactic:
rw [and_iff_not_or_not, Classical.not_not] at hij

Result:
case neg
R : Type u
M : Type v₁
N : Type v₂
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Finite 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

Proof state:
case neg
R : Type u
M : Type v₁
N : Type v₂
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Finite 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

Tactic:
rcases hij with hij | hij <;> simp [hij]

Result:
no goals