awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
inst_3 : Fintype ι
f : Dual R M
m : M
h :
  Eq.{uR + 1} (α := R)
    (∑ d : ι, (HSMul.hSMul (α := R) ((f : (a : M) → R) ((b : (a : ι) → M) d : M) : R) (b.coord d) : (a : M) → R) m : R)
    ((f : (a : M) → R) m : R)
h₁ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HSMul.hSMul (α := R) (β := R) ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R)
          ((b.coord x : (a : M) → R) m : R) :
      R)
    ((f : (a : M) → R) m : R)
h₂ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HMul.hMul (α := R) (β := R) ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R)
          ((b.coord x : (a : M) → R) m : R) :
      R)
    ((f : (a : M) → R) m : R)
h₃ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HMul.hMul (α := R) (β := R) ((b.coord x : (a : M) → R) m : R)
          ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R) :
      R)
    ((f : (a : M) → R) m : R)
h₄ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HSMul.hSMul (α := R) (β := R) ((b.coord x : (a : M) → R) m : R)
          ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R) :
      R)
    ((f : (a : M) → R) m : R)
h₅ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        (f : (a : M) → R)
          (HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((b.coord x : (a : M) → R) m : R) ((b : (a : ι) → M) x : M)) :
      R)
    ((f : (a : M) → R) m : R)
⊢ Eq.{uR + 1} (α := R)
    ((∑ x : ι, HSMul.hSMul (α := R) ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R) (b.coord x) : (a : M) → R) m : R)
    ((f : (a : M) → R) m : R)
have h₆ : Eq.{uR + 1} (α := R)
  ((f : (a : M) → R)
      (∑ x : ι,
        HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((b.coord x : (a : M) → R) m : R) ((b : (a : ι) → M) x : M)) :
    R)
  ((f : (a : M) → R) m : R)
Tactic: simp_rw [LinearMap.sum_apply, LinearMap.smul_apply, smul_eq_mul, mul_comm (f _), ← smul_eq_mul,
    ← f.map_smul, ← map_sum, Basis.coord_apply, Basis.sum_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
inst_3 : Fintype ι
f : Dual R M
m : M
h :
  Eq.{uR + 1} (α := R)
    (∑ d : ι, (HSMul.hSMul (α := R) ((f : (a : M) → R) ((b : (a : ι) → M) d : M) : R) (b.coord d) : (a : M) → R) m : R)
    ((f : (a : M) → R) m : R)
h₁ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HSMul.hSMul (α := R) (β := R) ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R)
          ((b.coord x : (a : M) → R) m : R) :
      R)
    ((f : (a : M) → R) m : R)
h₂ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HMul.hMul (α := R) (β := R) ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R)
          ((b.coord x : (a : M) → R) m : R) :
      R)
    ((f : (a : M) → R) m : R)
h₃ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HMul.hMul (α := R) (β := R) ((b.coord x : (a : M) → R) m : R)
          ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R) :
      R)
    ((f : (a : M) → R) m : R)
h₄ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HSMul.hSMul (α := R) (β := R) ((b.coord x : (a : M) → R) m : R)
          ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R) :
      R)
    ((f : (a : M) → R) m : R)
h₅ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        (f : (a : M) → R)
          (HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((b.coord x : (a : M) → R) m : R) ((b : (a : ι) → M) x : M)) :
      R)
    ((f : (a : M) → R) m : R)
h₆ :
  Eq.{uR + 1} (α := R)
    ((f : (a : M) → R)
        (∑ x : ι,
          HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((b.coord x : (a : M) → R) m : R) ((b : (a : ι) → M) x : M)) :
      R)
    ((f : (a : M) → R) m : R)
⊢ Eq.{uR + 1} (α := R)
    ((∑ x : ι, HSMul.hSMul (α := R) ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R) (b.coord x) : (a : M) → R) m : R)
    ((f : (a : M) → R) m : R)
have h₇ : Eq.{uR + 1} (α := R)
  ((f : (a : M) → R)
      (∑ x : ι,
        HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) x : R)
          ((b : (a : ι) → M) x : M)) :
    R)
  ((f : (a : M) → R) m : R)
Tactic: simp_rw [LinearMap.sum_apply, LinearMap.smul_apply, smul_eq_mul, mul_comm (f _), ← smul_eq_mul,
    ← f.map_smul, ← map_sum, Basis.coord_apply, Basis.sum_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 : ι
⊢ Eq.{uR + 1} (α := R) ((((b.dualBasis : (a : ι) → Dual R M) i : Dual R M) : (a : M) → R) ((b : (a : ι) → M) j : M) : R)
    (if j = i then 1 else 0 : R)
have h : j = i ↔ i = j
Tactic: convert! b.toDual_apply i j using 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 : ι
⊢ j = i ↔ i = j
have h : i = j ↔ i = j
Tactic: rw [@eq_comm _ j i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
f : ι →₀ R
i : ι
⊢ Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R (⇑b.dualBasis : (a : ι) → Dual R M) : (a : ι →₀ R) → Dual R M) f : Dual R M) :
          (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have intro : ∀ (val : Fintype ι),
  Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R (⇑b.dualBasis : (a : ι) → Dual R M) : (a : ι →₀ R) → Dual R M) f : Dual R M) :
          (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
f : ι →₀ R
i : ι
val : Fintype ι
⊢ Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R (⇑b.dualBasis : (a : ι) → Dual R M) : (a : ι →₀ R) → Dual R M) f : Dual R M) :
          (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have intro : Eq.{uR + 1} (α := R)
  (∑ d : ι,
      (HSMul.hSMul (α := R) (β := Dual R M) ((f : (a : ι) → R) d : R)
            ((b.dualBasis : (a : ι) → Dual R M) d : Dual R M) :
          (a : M) → R)
        ((b : (a : ι) → M) i : M) :
    R)
  ((f : (a : ι) → R) i : R)
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype, LinearMap.sum_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
f : ι →₀ R
i : ι
val : Fintype ι
intro :
  Eq.{uR + 1} (α := R)
    (∑ d : ι,
        (HSMul.hSMul (α := R) (β := Dual R M) ((f : (a : ι) → R) d : R)
              ((b.dualBasis : (a : ι) → Dual R M) d : Dual R M) :
            (a : M) → R)
          ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R (⇑b.dualBasis : (a : ι) → Dual R M) : (a : ι →₀ R) → Dual R M) f : Dual R M) :
          (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have intro₁ : ∀ (i : ι), HSMul.hSMul (α := R) (β := Dual R M) 0 ((b.dualBasis : (a : ι) → Dual R M) i : Dual R M) = 0
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype, LinearMap.sum_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
f : ι →₀ R
i : ι
val : Fintype ι
⊢ Eq.{uR + 1} (α := R)
    (∑ d : ι,
        (HSMul.hSMul (α := R) (β := Dual R M) ((f : (a : ι) → R) d : R)
              ((b.dualBasis : (a : ι) → Dual R M) d : Dual R M) :
            (a : M) → R)
          ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have intro : Eq.{uR + 1} (α := R)
  (∑ x : ι,
      HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
        ((((b.dualBasis : (a : ι) → Dual R M) x : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) :
    R)
  ((f : (a : ι) → R) i : R)
Tactic: simp_rw [LinearMap.smul_apply, smul_eq_mul, dualBasis_apply_self, mul_boole,
      Finset.sum_ite_eq, if_pos (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
f : ι →₀ R
i : ι
val : Fintype ι
intro :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.dualBasis : (a : ι) → Dual R M) x : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) :
      R)
    ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    (∑ d : ι,
        (HSMul.hSMul (α := R) (β := Dual R M) ((f : (a : ι) → R) d : R)
              ((b.dualBasis : (a : ι) → Dual R M) d : Dual R M) :
            (a : M) → R)
          ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have intro₁ : Eq.{uR + 1} (α := R)
  (∑ x : ι,
      HMul.hMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
        ((((b.dualBasis : (a : ι) → Dual R M) x : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) :
    R)
  ((f : (a : ι) → R) i : R)
Tactic: simp_rw [LinearMap.smul_apply, smul_eq_mul, dualBasis_apply_self, mul_boole,
      Finset.sum_ite_eq, if_pos (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
f : ι →₀ R
i : ι
val : Fintype ι
intro :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.dualBasis : (a : ι) → Dual R M) x : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) :
      R)
    ((f : (a : ι) → R) i : R)
intro₁ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HMul.hMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.dualBasis : (a : ι) → Dual R M) x : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) :
      R)
    ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    (∑ d : ι,
        (HSMul.hSMul (α := R) (β := Dual R M) ((f : (a : ι) → R) d : R)
              ((b.dualBasis : (a : ι) → Dual R M) d : Dual R M) :
            (a : M) → R)
          ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have intro₂ : Eq.{uR + 1} (α := R) (∑ x : ι, HMul.hMul (α := R) (β := R) ((f : (a : ι) → R) x : R) (if i = x then 1 else 0 : R) : R)
  ((f : (a : ι) → R) i : R)
Tactic: simp_rw [LinearMap.smul_apply, smul_eq_mul, dualBasis_apply_self, mul_boole,
      Finset.sum_ite_eq, if_pos (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
f : ι →₀ R
i : ι
val : Fintype ι
intro :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.dualBasis : (a : ι) → Dual R M) x : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) :
      R)
    ((f : (a : ι) → R) i : R)
intro₁ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HMul.hMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.dualBasis : (a : ι) → Dual R M) x : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) :
      R)
    ((f : (a : ι) → R) i : R)
intro₂ :
  Eq.{uR + 1} (α := R) (∑ x : ι, HMul.hMul (α := R) (β := R) ((f : (a : ι) → R) x : R) (if i = x then 1 else 0 : R) : R)
    ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    (∑ d : ι,
        (HSMul.hSMul (α := R) (β := Dual R M) ((f : (a : ι) → R) d : R)
              ((b.dualBasis : (a : ι) → Dual R M) d : Dual R M) :
            (a : M) → R)
          ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have intro₃ : Eq.{uR + 1} (α := R) (∑ x : ι, if i = x then (f : (a : ι) → R) x else 0 : R) ((f : (a : ι) → R) i : R)
Tactic: simp_rw [LinearMap.smul_apply, smul_eq_mul, dualBasis_apply_self, mul_boole,
      Finset.sum_ite_eq, if_pos (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
f : ι →₀ R
i : ι
val : Fintype ι
intro :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.dualBasis : (a : ι) → Dual R M) x : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) :
      R)
    ((f : (a : ι) → R) i : R)
intro₁ :
  Eq.{uR + 1} (α := R)
    (∑ x : ι,
        HMul.hMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.dualBasis : (a : ι) → Dual R M) x : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) :
      R)
    ((f : (a : ι) → R) i : R)
intro₂ :
  Eq.{uR + 1} (α := R) (∑ x : ι, HMul.hMul (α := R) (β := R) ((f : (a : ι) → R) x : R) (if i = x then 1 else 0 : R) : R)
    ((f : (a : ι) → R) i : R)
intro₃ : Eq.{uR + 1} (α := R) (∑ x : ι, if i = x then (f : (a : ι) → R) x else 0 : R) ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    (∑ d : ι,
        (HSMul.hSMul (α := R) (β := Dual R M) ((f : (a : ι) → R) d : R)
              ((b.dualBasis : (a : ι) → Dual R M) d : Dual R M) :
            (a : M) → R)
          ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have intro₄ : Eq.{uR + 1} (α := R) (if Membership.mem (γ := Finset ι) Finset.univ i then (f : (a : ι) → R) i else 0 : R)
  ((f : (a : ι) → R) i : R)
Tactic: simp_rw [LinearMap.smul_apply, smul_eq_mul, dualBasis_apply_self, mul_boole,
      Finset.sum_ite_eq, if_pos (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
f : ι →₀ R
i : ι
val : Fintype ι
i_1 : ι
⊢ HSMul.hSMul (α := R) (β := Dual R M) 0 ((b.dualBasis : (a : ι) → Dual R M) i_1 : Dual R M) = 0
have intro : Eq (α := Dual R M) 0 0
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
l : Dual R M
i : ι
⊢ Eq.{uR + 1} (α := R) ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) l : ι →₀ R) : (a : ι) → R) i : R)
    ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
have rw : Eq.{uR + 1} (α := R)
  ((((Finsupp.linearCombination R (⇑b.dualBasis : (a : ι) → Dual R M) : (a : ι →₀ R) → Dual R M)
            ((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) l) :
          Dual R M) :
        (a : M) → R)
      ((b : (a : ι) → M) i : M) :
    R)
  ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: rw [← linearCombination_dualBasis b, Basis.linearCombination_repr b.dualBasis l]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
l : Dual R M
i : ι
rw :
  Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R (⇑b.dualBasis : (a : ι) → Dual R M) : (a : ι →₀ R) → Dual R M)
              ((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) l) :
            Dual R M) :
          (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
⊢ Eq.{uR + 1} (α := R) ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) l : ι →₀ R) : (a : ι) → R) i : R)
    ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
have rw₁ : Eq.{uR + 1} (α := R) ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R) ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: rw [← linearCombination_dualBasis b, Basis.linearCombination_repr b.dualBasis l]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
⊢ (⇑b.dualBasis : (a : ι) → Dual R M) = b.coord
have h : ∀ (i : ι) (x : M),
  Eq.{uR + 1} (α := R) ((((b.dualBasis : (a : ι) → Dual R M) i : Dual R M) : (a : M) → R) x : R)
    ((b.coord i : (a : M) → R) x : R)
Tactic: ext i x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 ι
⊢ b.dualBasis.toDual ∘ₗ b.toDual = Dual.eval R M
have refine : ∀ (i j : ι),
  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: refine b.ext fun i => b.dualBasis.ext fun j => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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 : ι
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
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)
⊢ 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)
have 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)
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]