-- 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
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_1 : ι × κ),
    ((dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis (i, j)))
        ((b.tensorProduct c) i_1) =
      (LinearMap.id ((b.tensorProduct c).dualBasis (i, j))) ((b.tensorProduct c) i_1)

Tactic:
rintro ⟨i', 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' : κ
⊢ ((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'))

Proof state:
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
⊢ dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = LinearMap.id

Tactic:
apply (b.tensorProduct c).dualBasis.ext

Result:
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 : ι × κ),
    (dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis i) =
      LinearMap.id ((b.tensorProduct c).dualBasis i)

Proof state:
case 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 : κ
⊢ (dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis (i, j)) =
    LinearMap.id ((b.tensorProduct c).dualBasis (i, j))

Tactic:
apply (b.tensorProduct c).ext

Result:
case 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_1 : ι × κ),
    ((dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis (i, j)))
        ((b.tensorProduct c) i_1) =
      (LinearMap.id ((b.tensorProduct c).dualBasis (i, j))) ((b.tensorProduct c) i_1)

Proof state:
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

Tactic:
all_goals { intros; simp [*] at * }

Result:
no goals

Proof state:
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' : κ
a✝ : 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

Tactic:
simp [*] at *

Result:
no goals

Proof state:
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 : ι × κ),
    (dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis i) =
      LinearMap.id ((b.tensorProduct c).dualBasis i)

Tactic:
rintro ⟨i, j⟩

Result:
case 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 : κ
⊢ (dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis (i, j)) =
    LinearMap.id ((b.tensorProduct c).dualBasis (i, j))

Proof state:
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

Tactic:
intros

Result:
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' : κ
a✝ : 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