-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
i j : ι
rw :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual : (a : Dual R M) → Dual R (Dual R M))
              ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) :
            Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₁ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) : ι →₀ R) :
          (a : ι) → R)
        j :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₂ :
  Eq.{uR + 1} (α := R) ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) (b.coord i) : ι →₀ R) : (a : ι) → R) j : R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₃ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.dualBasis : (a : ι) → Dual R M) i) : ι →₀ R) : (a : ι) → R) j :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₄ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.dualBasis : (a : ι) → Dual R M) i) : ι →₀ R) : (a : ι) → R) j :
      R)
    ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
rw₅ :
  Eq.{uR + 1} (α := R) ((Finsupp.single i 1 : (a : ι) → R) j : R)
    ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
rw₆ :
  Eq.{uR + 1} (α := R) (if i = j then 1 else 0 : R)
    ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
rw₇ rw₈ : Eq.{uR + 1} (α := R) (if i = j then 1 else 0) (if i = j then 1 else 0)
⊢ Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual ∘ₗ b.toDual : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)

Tactic:
rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis,
    Dual.eval_apply, Basis.repr_self, Finsupp.single_apply, dualBasis_apply_self]

Premises used: Module.Basis.coe_dualBasis, Module.Dual.eval_apply, LinearMap.comp_apply, Module.Basis.dualBasis_apply_self, Module.Basis.coe_toDual_self, Finsupp.single_apply, Module.Basis.toDual_apply_left, Module.Basis.repr_self