awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
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
a : A
w : W
h :
  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)
⊢ 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) (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)
        (a • w) :
      A)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
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
x y : W
hx :
  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) x : 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)
        x :
      A)
hy :
  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) y : 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)
        y :
      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) (x + y) : 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)
        (x + y) :
      A)

Tactic:
simp [map_add, hx, hy]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
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 : A
f : Dual R V
v : V
⊢ (((ibc.toDualBaseChange : (a : A ⊗[R] Dual R V) → Dual A W) (a ⊗ₜ[R] f) : Dual A W) : (a : W) → A)
      ((j : (a : V) → W) v : W) =
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) ((f : (a : V) → R) v : R) : A)

Tactic:
toDualBaseChangeAux_tmul ibc a f v

Premises used: _private.0.IsBaseChange.toDualBaseChangeAux_tmul
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
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
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)
⊢ IsBaseChange A ibc.toDual

Tactic:
apply of_equiv (toDualBaseChange ibc)

Premises used: IsBaseChange.of_equiv, IsBaseChange.toDualBaseChange
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
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
f : Dual R V
⊢ Eq (α := Dual A W) ((ibc.toDualBaseChange : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W)
    ((ibc.toDual : (a : Dual R V) → Dual A W) f : Dual A W)

Tactic:
simp [toDualBaseChange, toDualBaseChangeAux]

Premises used: IsBaseChange.toDualBaseChange, _private.0.IsBaseChange.toDualBaseChangeAux
-- 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
i j : ι
rw : Eq.{uR + 1} (α := R) (if j = i then 1 else 0) (if i = j then 1 else 0)
⊢ 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)

Tactic:
rw [toDual, constr_basis b, constr_basis b]

Premises used: Module.Basis.toDual, Module.Basis.constr_basis
-- 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
i j : ι
⊢ Eq.{uR + 1} (α := R) (if j = i then 1 else 0) (if i = j then 1 else 0)

Tactic:
simp only [eq_comm]

Premises used: eq_comm
-- 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
f : ι →₀ R
i : ι
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)
⊢ 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)

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, LinearMap.sum_apply]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, map_sum, LinearMap.sum_apply
-- 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
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)
simp_rw₅ : Eq.{uR + 1} (α := R) (if i ∈ f.support then (f : (a : ι) → R) i 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)

Tactic:
simp_rw [map_smul, LinearMap.smul_apply, toDual_apply, smul_eq_mul, mul_boole,
    Finset.sum_ite_eq', Finsupp.if_mem_support]

Premises used: Finsupp.if_mem_support, Finset.sum_ite_eq', LinearMap.smul_apply, mul_boole, Module.Basis.toDual_apply, smul_eq_mul, map_smul
-- 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
f : ι →₀ R
i : ι
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)
⊢ 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)

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, map_sum
-- 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
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)
simp_rw₄ : Eq.{uR + 1} (α := R) (if i ∈ f.support then (f : (a : ι) → R) i 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)

Tactic:
simp_rw [map_smul, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq,
    Finsupp.if_mem_support]

Premises used: Finsupp.if_mem_support, mul_boole, Module.Basis.toDual_apply, smul_eq_mul, Finset.sum_ite_eq, map_smul
-- 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
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)
rw₁ 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)
⊢ 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.toDual_linearCombination_left, b.linearCombination_repr]

Premises used: Module.Basis.toDual_linearCombination_left, Module.Basis.linearCombination_repr
-- 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
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [← b.toDual_linearCombination_right, b.linearCombination_repr]

Premises used: Module.Basis.linearCombination_repr, Module.Basis.toDual_linearCombination_right
-- 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
i : ι
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)
⊢ (b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i) = b.coord i

Tactic:
ext
-- 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
i : ι
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:
apply toDual_apply_right

Premises used: Module.Basis.toDual_apply_right
-- 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
m₁ m₂ : M
⊢ Eq.{uR + 1} (α := R) ((b.toDualFlip m₁ : (a : M) → R) m₂ : R)
    ((((b.toDual : (a : M) → Dual R M) m₂ : Dual R M) : (a : M) → R) m₁ : R)

Tactic:
rfl

Premises used: rfl
-- 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
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)

Tactic:
b.toDual_apply_left m i

Premises used: Module.Basis.toDual_apply_left
-- 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 ι
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [b.equivFun_apply, toDual_eq_repr]

Premises used: Module.Basis.toDual_eq_repr, Module.Basis.equivFun_apply
-- 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
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 : ι
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)
⊢ 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)

Tactic:
simp_rw [← toDual_eq_repr]

Premises used: Module.Basis.toDual_eq_repr
-- 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
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.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:
DFunLike.congr_fun h _

Premises used: DFunLike.congr_fun
-- 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
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.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:
exact DFunLike.congr_fun h _

Premises used: DFunLike.congr_fun
-- 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
m : M
a rwa rwa₁ rwa₂ rwa₃ : Eq (α := Dual R M) ((b.toDual : (a : M) → Dual R M) m : Dual R M) (0 : Dual R M)
⊢ Eq (α := Dual R M) ((b.toDual : (a : M) → Dual R M) m : Dual R M) ((b.toDual : (a : M) → Dual R M) 0 : Dual R M)

Tactic:
rwa [map_zero]

Premises used: map_zero
-- 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
⊢ b.toDual.ker = ⊥

Tactic:
ker_eq_bot'.mpr b.toDual_inj

Premises used: Iff.mpr, Module.Basis.toDual_inj, LinearMap.ker_eq_bot'
-- 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 ι
f : Dual R M
i : ι
⊢ Eq.{uR + 1} (α := R)
    (((b.toDual : (a : M) → Dual R M)
            ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M)
              ((Equiv.symm Finsupp.equivFunOnFinite : (a : ι → R) → ι →₀ R) fun (i : ι) ↦
                (f : (a : M) → R) ((b : (a : ι) → M) i : M))) :
          (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : M) → R) ((b : (a : ι) → M) i : M) : R)

Tactic:
simp
-- 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
b : Basis ι R M
inst_3 : Fintype ι
f : Dual R M
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)
⊢ ∑ x : ι, HSMul.hSMul (α := R) ((f : (a : M) → R) ((b : (a : ι) → M) x : M) : R) (b.coord x) = f

Tactic:
ext m
-- 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
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)
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)
⊢ 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:
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]

Premises used: LinearMap.smul_apply, map_sum, LinearMap.map_smul, mul_comm, LinearMap.sum_apply, smul_eq_mul, DFunLike.coe, Module.Basis.sum_repr, Module.Basis.coord_apply
-- 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 ι
m : M
⊢ Eq (α := Dual R M) ((b.toDualEquiv : (a : M) → Dual R M) m : Dual R M) ((b.toDual : (a : M) → Dual R M) m : Dual R M)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl