awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
a : A
g : A ⊗[R] Dual R V
⊢ AddHom.toFun
      (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
        (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
      (a • g) =
    HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
      (AddHom.toFun
        (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
          (TensorProduct.lift
            { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
        g)
have zero : AddHom.toFun
    (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
      (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := sorry, map_smul' := sorry }))
    (HSMul.hSMul (β := A ⊗[R] Dual R V) a 0) =
  HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
    (AddHom.toFun (M := A ⊗[R] Dual R V)
      (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
        (TensorProduct.lift
          { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := sorry, map_smul' := sorry : A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
      0)
Tactic: induction g using TensorProduct.induction_on with
    | zero => simp
    | add x y hx hy => aesop
    | tmul b f => simp [TensorProduct.smul_tmul', mul_smul]
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
⊢ A ⊗[R] Dual R V ≃ₗ[A] Dual A W
have apply : Function.Bijective (α := A ⊗[R] Dual R V) (β := Dual A W) (⇑ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W)
Tactic: apply LinearEquiv.ofBijective ibc.toDualBaseChangeAux
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
b : Basis (Free.ChooseBasisIndex R V) R V := Free.chooseBasis R V
⊢ Function.Bijective (α := A ⊗[R] Dual R V) (β := Dual A W)
    (⇑ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W)
have set : let ι := Free.ChooseBasisIndex R V;
∀ (b : Basis ι R V),
  Function.Bijective (α := A ⊗[R] Dual R V) (β := Dual A W)
    (⇑ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W)
Tactic: set ι := Free.ChooseBasisIndex R V
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
⊢ Function.Bijective (α := A ⊗[R] Dual R V) (β := Dual A W)
    (⇑ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W)
have ibc_pow : IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)
Tactic: have ibc_pow : IsBaseChange A ((Algebra.linearMap R A).compLeft ι) := (linearMap R A).finitePow ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)
⊢ Function.Bijective (α := A ⊗[R] Dual R V) (β := Dual A W)
    (⇑ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W)
have suffices : ibc.toDualBaseChangeAux =
  (↑(LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) ≪≫ₗ ibc_pow.equiv ≪≫ₗ
        (basis b ibc).constr A) :
    A ⊗[R] (V →ₗ[R] R) →ₗ[A] W →ₗ[A] A)
Tactic: suffices ibc.toDualBaseChangeAux =
      (((b.constr R).symm.baseChange ..).trans ibc_pow.equiv).trans ((ibc.basis b).constr A) from
    this ▸ LinearEquiv.bijective _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)
⊢ ibc.toDualBaseChangeAux =
    (↑(LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) ≪≫ₗ ibc_pow.equiv ≪≫ₗ
          (basis b ibc).constr A) :
      A ⊗[R] (V →ₗ[R] R) →ₗ[A] W →ₗ[A] A)
have a : ∀ (f : Dual R V) (w : W),
  Eq.{u_4 + 1} (α := A)
    ((((((AlgebraTensorModule.curry ibc.toDualBaseChangeAux : A →ₗ[A] Dual R V →ₗ[R] Dual A W) :
                    (a : A) → Dual R V →ₗ[R] Dual A W)
                  1 :
                (a : Dual R V) → Dual A W)
              f :
            Dual A W) :
          (a : W) → A)
        w :
      A)
    ((((((AlgebraTensorModule.curry
                        (↑(LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) ≪≫ₗ
                                ibc_pow.equiv ≪≫ₗ
                              (basis b ibc).constr A) :
                          A ⊗[R] (V →ₗ[R] R) →ₗ[A] W →ₗ[A] A) :
                      A →ₗ[A] Dual R V →ₗ[R] Dual A W) :
                    (a : A) → Dual R V →ₗ[R] Dual A W)
                  1 :
                (a : Dual R V) → Dual A W)
              f :
            Dual A W) :
          (a : W) → A)
        w :
      A)
Tactic: ext f w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)
f : Dual R V
w : W
⊢ Eq.{u_4 + 1} (α := A)
    ((((((AlgebraTensorModule.curry ibc.toDualBaseChangeAux : A →ₗ[A] Dual R V →ₗ[R] Dual A W) :
                    (a : A) → Dual R V →ₗ[R] Dual A W)
                  1 :
                (a : Dual R V) → Dual A W)
              f :
            Dual A W) :
          (a : W) → A)
        w :
      A)
    ((((((AlgebraTensorModule.curry
                        (↑(LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) ≪≫ₗ
                                ibc_pow.equiv ≪≫ₗ
                              (basis b ibc).constr A) :
                          A ⊗[R] (V →ₗ[R] R) →ₗ[A] W →ₗ[A] A) :
                      A →ₗ[A] Dual R V →ₗ[R] Dual A W) :
                    (a : A) → Dual R V →ₗ[R] Dual A W)
                  1 :
                (a : Dual R V) → Dual A W)
              f :
            Dual A W) :
          (a : W) → A)
        w :
      A)
have a : Eq.{u_4 + 1} (α := A)
  ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A) w : A)
  (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
            ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
              ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                    (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                  (1 ⊗ₜ[R] f) :
                A ⊗[R] (ι → R))) :
          W →ₗ[A] A) :
        (a : W) → A)
      w :
    A)
Tactic: simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars,
    LinearEquiv.coe_coe, LinearEquiv.trans_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)
f : Dual R V
w : W
⊢ Eq.{u_4 + 1} (α := A)
    ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A) w : A)
    (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
              ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
                ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                      (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                    (1 ⊗ₜ[R] f) :
                  A ⊗[R] (ι → R))) :
            W →ₗ[A] A) :
          (a : W) → A)
        w :
      A)
have a : Eq.{u_4 + 1} (α := A)
  ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A) 0 : A)
  (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
            ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
              ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                    (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                  (1 ⊗ₜ[R] f) :
                A ⊗[R] (ι → R))) :
          W →ₗ[A] A) :
        (a : W) → A)
      0 :
    A)
Tactic: induction w using ibc.inductionOn with
  | zero => simp
  | tmul v =>
    simp only [toDualBaseChangeAux_tmul, one_mul]
    conv_lhs => rw [← Basis.sum_equivFun b v, map_sum]
    simp [LinearEquiv.baseChange, basis_repr_comp_apply]
  | smul a w h => simp [h]
  | add x y hx hy => simp [map_add, hx, hy]
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)
f : Dual R V
w : W
a :
  Eq.{u_4 + 1} (α := A)
    ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A) 0 : A)
    (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
              ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
                ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                      (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                    (1 ⊗ₜ[R] f) :
                  A ⊗[R] (ι → R))) :
            W →ₗ[A] A) :
          (a : W) → A)
        0 :
      A)
⊢ Eq.{u_4 + 1} (α := A)
    ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A) w : A)
    (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
              ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
                ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                      (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                    (1 ⊗ₜ[R] f) :
                  A ⊗[R] (ι → R))) :
            W →ₗ[A] A) :
          (a : W) → A)
        w :
      A)
have a₁ : ∀ (v : V),
  Eq.{u_4 + 1} (α := A)
    ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A)
        ((j : (a : V) → W) v : W) :
      A)
    (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
              ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
                ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                      (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                    (1 ⊗ₜ[R] f) :
                  A ⊗[R] (ι → R))) :
            W →ₗ[A] A) :
          (a : W) → A)
        ((j : (a : V) → W) v : W) :
      A)
Tactic: induction w using ibc.inductionOn with
  | zero => simp
  | tmul v =>
    simp only [toDualBaseChangeAux_tmul, one_mul]
    conv_lhs => rw [← Basis.sum_equivFun b v, map_sum]
    simp [LinearEquiv.baseChange, basis_repr_comp_apply]
  | smul a w h => simp [h]
  | add x y hx hy => simp [map_add, hx, hy]
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.BaseChange (goal)
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
⊢ IsBaseChange A ibc.toDual
have apply : ∀ (x : Dual R V),
  Eq (α := Dual A W) ((ibc.toDualBaseChange : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] x) : Dual A W)
    ((ibc.toDual : (a : Dual R V) → Dual A W) x : Dual A W)
Tactic: apply of_equiv (toDualBaseChange ibc)
-- 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 j : ι
⊢ Eq.{uR + 1} (α := R)
    ((((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) : Dual R M) : (a : M) → R) ((b : (a : ι) → M) j : M) : R)
    (if i = j then 1 else 0 : R)
have rw : Eq.{uR + 1} (α := R) (if j = i then 1 else 0) (if i = j then 1 else 0)
Tactic: rw [toDual, constr_basis b, constr_basis b]
-- 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) ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) f) :
            Dual R M) :
          (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have rw : 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)
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, 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
f : ι →₀ R
i : ι
⊢ 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)
  (∑ 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)
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 : ι
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)
⊢ 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)
  (∑ 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)
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 : ι
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)
⊢ 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)
  (∑ 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)
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 : ι
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)
⊢ 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)
  (∑ 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)
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 : ι
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)
⊢ 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) (∑ x ∈ f.support, if x = i then (f : (a : ι) → R) x 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]