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
inst_3 : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
simp_rw :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support,
        (HSMul.hSMul (α := R) (β := Dual R M) ((f : (a : ι) → R) x : R)
              ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) x) : Dual R M) :
            (a : M) → R)
          ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
simp_rw₁ :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support,
        HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) x) : Dual R M) : (a : M) → R)
              ((b : (a : ι) → M) i : M) :
            R) :
      R)
    ((f : (a : ι) → R) i : R)
simp_rw₂ :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support, HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R) (if x = i then 1 else 0) : R)
    ((f : (a : ι) → R) i : R)
simp_rw₃ :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support, HMul.hMul (α := R) (β := R) ((f : (a : ι) → R) x : R) (if x = i then 1 else 0 : R) : R)
    ((f : (a : ι) → R) i : R)
simp_rw₄ :
  Eq.{uR + 1} (α := R) (∑ x ∈ f.support, if x = i then (f : (a : ι) → R) x else 0 : R) ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    (∑ d ∈ f.support,
        (((b.toDual : (a : M) → Dual R M)
                (HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((f : (a : ι) → R) d : R) ((b : (a : ι) → M) d : M)) :
              Dual R M) :
            (a : M) → R)
          ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have simp_rw₅ : Eq.{uR + 1} (α := R) (if i ∈ f.support then (f : (a : ι) → R) i else 0 : R) ((f : (a : ι) → R) i : R)
Tactic: simp_rw [map_smul, LinearMap.smul_apply, toDual_apply, smul_eq_mul, mul_boole,
    Finset.sum_ite_eq', Finsupp.if_mem_support]
-- 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
f : ι →₀ R
i : ι
⊢ Eq.{uR + 1} (α := R)
    ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
        ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) f : M) :
      R)
    ((f : (a : ι) → R) i : R)
have rw : Eq.{uR + 1} (α := R)
  (∑ x ∈ f.support,
      (((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
        (HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((f : (a : ι) → R) x : R) ((b : (a : ι) → M) x : M)) :
    R)
  ((f : (a : ι) → R) i : R)
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum]
-- 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
f : ι →₀ R
i : ι
⊢ Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support,
        (((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
          (HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((f : (a : ι) → R) x : R) ((b : (a : ι) → M) x : M)) :
      R)
    ((f : (a : ι) → R) i : R)
have simp_rw : Eq.{uR + 1} (α := R)
  (∑ x ∈ f.support,
      HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
        ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R) ((b : (a : ι) → M) x : M) :
          R) :
    R)
  ((f : (a : ι) → R) i : R)
Tactic: simp_rw [map_smul, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq,
    Finsupp.if_mem_support]
-- 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
f : ι →₀ R
i : ι
simp_rw :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support,
        HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
              ((b : (a : ι) → M) x : M) :
            R) :
      R)
    ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support,
        (((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
          (HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((f : (a : ι) → R) x : R) ((b : (a : ι) → M) x : M)) :
      R)
    ((f : (a : ι) → R) i : R)
have simp_rw₁ : Eq.{uR + 1} (α := R)
  (∑ x ∈ f.support, HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R) (if i = x then 1 else 0) : R)
  ((f : (a : ι) → R) i : R)
Tactic: simp_rw [map_smul, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq,
    Finsupp.if_mem_support]
-- 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
f : ι →₀ R
i : ι
simp_rw :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support,
        HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
              ((b : (a : ι) → M) x : M) :
            R) :
      R)
    ((f : (a : ι) → R) i : R)
simp_rw₁ :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support, HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R) (if i = x then 1 else 0) : R)
    ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support,
        (((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
          (HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((f : (a : ι) → R) x : R) ((b : (a : ι) → M) x : M)) :
      R)
    ((f : (a : ι) → R) i : R)
have simp_rw₂ : Eq.{uR + 1} (α := R)
  (∑ x ∈ f.support, 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 [map_smul, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq,
    Finsupp.if_mem_support]
-- 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
f : ι →₀ R
i : ι
simp_rw :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support,
        HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
              ((b : (a : ι) → M) x : M) :
            R) :
      R)
    ((f : (a : ι) → R) i : R)
simp_rw₁ :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support, HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R) (if i = x then 1 else 0) : R)
    ((f : (a : ι) → R) i : R)
simp_rw₂ :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support, 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)
    (∑ x ∈ f.support,
        (((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
          (HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((f : (a : ι) → R) x : R) ((b : (a : ι) → M) x : M)) :
      R)
    ((f : (a : ι) → R) i : R)
have simp_rw₃ : Eq.{uR + 1} (α := R) (∑ x ∈ f.support, if i = x then (f : (a : ι) → R) x else 0 : R) ((f : (a : ι) → R) i : R)
Tactic: simp_rw [map_smul, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq,
    Finsupp.if_mem_support]
-- 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
f : ι →₀ R
i : ι
simp_rw :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support,
        HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R)
          ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
              ((b : (a : ι) → M) x : M) :
            R) :
      R)
    ((f : (a : ι) → R) i : R)
simp_rw₁ :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support, HSMul.hSMul (α := R) (β := R) ((f : (a : ι) → R) x : R) (if i = x then 1 else 0) : R)
    ((f : (a : ι) → R) i : R)
simp_rw₂ :
  Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support, HMul.hMul (α := R) (β := R) ((f : (a : ι) → R) x : R) (if i = x then 1 else 0 : R) : R)
    ((f : (a : ι) → R) i : R)
simp_rw₃ :
  Eq.{uR + 1} (α := R) (∑ x ∈ f.support, if i = x then (f : (a : ι) → R) x else 0 : R) ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    (∑ x ∈ f.support,
        (((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
          (HSMul.hSMul.{uR, uM, uM} (α := R) (β := M) ((f : (a : ι) → R) x : R) ((b : (a : ι) → M) x : M)) :
      R)
    ((f : (a : ι) → R) i : R)
have simp_rw₄ : Eq.{uR + 1} (α := R) (if i ∈ f.support then (f : (a : ι) → R) i else 0 : R) ((f : (a : ι) → R) i : R)
Tactic: simp_rw [map_smul, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq,
    Finsupp.if_mem_support]
-- 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
m : M
i : ι
⊢ Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) m : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
    ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R)
have rw : Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) m : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
  ((((b.toDual : (a : M) → Dual R M)
            ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M)
              ((b.repr : (a : M) → ι →₀ R) m : ι →₀ R)) :
          Dual R M) :
        (a : M) → R)
      ((b : (a : ι) → M) i : M) :
    R)
Tactic: rw [← b.toDual_linearCombination_left, b.linearCombination_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
m : M
i : ι
rw :
  Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) m : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
    ((((b.toDual : (a : M) → Dual R M)
              ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M)
                ((b.repr : (a : M) → ι →₀ R) m : ι →₀ R)) :
            Dual R M) :
          (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
⊢ Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) m : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
    ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R)
have rw₁ : Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) m : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
  ((((b.toDual : (a : M) → Dual R M) m : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: rw [← b.toDual_linearCombination_left, b.linearCombination_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
i : ι
m : M
⊢ Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R) m : R)
    ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R)
have rw : Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R) m : R)
  ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
      ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) :
        M) :
    R)
Tactic: rw [← b.toDual_linearCombination_right, b.linearCombination_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
i : ι
m : M
rw :
  Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R) m : R)
    ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R)
        ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) :
          M) :
      R)
⊢ Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R) m : R)
    ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R)
have rw₁ : Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R) m : R)
  ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R) m : R)
Tactic: rw [← b.toDual_linearCombination_right, b.linearCombination_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
i : ι
⊢ (b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) = b.coord i
have h : ∀ (x : M),
  Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R) x : R)
    ((b.coord i : (a : M) → R) x : R)
Tactic: ext
-- 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 ι
m : M
i : ι
⊢ Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) m : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
    ((b.equivFun : (a : M) → ι → R) m i : R)
have rw : Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) m : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
  ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [b.equivFun_apply, toDual_eq_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 ι
m : M
i : ι
rw :
  Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) m : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
    ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) m : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
    ((b.equivFun : (a : M) → ι → R) m i : R)
have rw₁ : Eq.{uR + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R)
  ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [b.equivFun_apply, toDual_eq_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
x y : M
h : Eq (α := Dual R M) ((b.toDual : (a : M) → Dual R M) x : Dual R M) ((b.toDual : (a : M) → Dual R M) y : Dual R M)
i : ι
⊢ Eq.{uR + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
    ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R)
have simp_rw : Eq.{uR + 1} (α := R) ((((b.toDual : (a : M) → Dual R M) x : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
  ((((b.toDual : (a : M) → Dual R M) y : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: simp_rw [← toDual_eq_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
⊢ ∑ x : ι, HSMul.hSMul (α := R) ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R) (b.coord x) = f
have h : ∀ (m : M),
  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)
Tactic: ext m
-- 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
⊢ 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)
  (∑ 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)
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)
⊢ 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)
  (∑ 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)
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)
⊢ 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)
  (∑ 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)
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)
⊢ 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)
  (∑ 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)
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)
⊢ 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)
  (∑ 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)
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)
⊢ 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)
  (∑ 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)
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]