awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
i j : ι
⊢ 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:
b.toDual_apply i j

Premises used: Module.Basis.toDual_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 ι
i j : ι
h : j = i ↔ 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)

Tactic:
convert! b.toDual_apply i j using 2

Premises used: Module.Basis.toDual_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 ι
i j : ι
h h₁ : i = j ↔ i = j
⊢ j = i ↔ i = j

Tactic:
rw [@eq_comm _ j i]

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
inst_4 : Finite ι
f : ι →₀ R
i : ι
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)
⊢ 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 ι

Premises used: nonempty_fintype
-- 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 : ι →₀ 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)
intro₁ : ∀ (i : ι), HSMul.hSMul (α := R) (β := Dual R M) 0 ((b.dualBasis : (a : ι) → Dual R M) i : Dual R M) = 0
⊢ 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:
rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype, LinearMap.sum_apply]

Premises used: Finsupp.sum_fintype, Finsupp.linearCombination_apply, 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
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)
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)
⊢ 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:
simp_rw [LinearMap.smul_apply, smul_eq_mul, dualBasis_apply_self, mul_boole,
      Finset.sum_ite_eq, if_pos (Finset.mem_univ i)]

Premises used: Finset.mem_univ, LinearMap.smul_apply, mul_boole, Module.Basis.dualBasis_apply_self, if_pos, smul_eq_mul, Finset.sum_ite_eq
-- 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 : ι →₀ R
i : ι
val : Fintype ι
i_1 : ι
intro intro₁ : Eq (α := Dual R M) 0 0
⊢ HSMul.hSMul (α := R) (β := Dual R M) 0 ((b.dualBasis : (a : ι) → Dual R M) i_1 : Dual R M) = 0

Tactic:
rw [zero_smul]

Premises used: zero_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
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [← linearCombination_dualBasis b, Basis.linearCombination_repr b.dualBasis l]

Premises used: Module.Basis.linearCombination_dualBasis, Module.Basis.dualBasis, 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
inst_4 : Finite ι
i : ι
m : M
⊢ Eq.{uR + 1} (α := R) ((((b.dualBasis : (a : ι) → Dual R M) i : Dual R M) : (a : M) → R) m : R)
    ((((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
b.toDual_apply_right i m

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
inst_4 : Finite ι
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)
⊢ (⇑b.dualBasis : (a : ι) → Dual R M) = b.coord

Tactic:
ext i x
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
i : ι
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:
apply dualBasis_apply

Premises used: Module.Basis.dualBasis_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 ι
⊢ b.dualBasis.toDual ∘ₗ b.toDual = Dual.eval R M

Tactic:
b.ext fun i => b.dualBasis.ext fun j => ?_

Premises used: Module.Basis.dualBasis, Module.Basis.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
inst_4 : Finite ι
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)
⊢ b.dualBasis.toDual ∘ₗ b.toDual = Dual.eval R M

Tactic:
refine b.ext fun i => b.dualBasis.ext fun j => ?_

Premises used: Module.Basis.dualBasis, Module.Basis.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
inst_4 : Finite ι
l : Dual R M
i : ι
rw :
  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)
rw₁ 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)
⊢ Eq.{uR + 1} (α := R) ((b.dualBasis.equivFun : (a : Dual R M) → ι → R) l i : R)
    ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R)

Tactic:
rw [Basis.equivFun_apply, dualBasis_repr]

Premises used: Module.Basis.dualBasis_repr, Module.Basis.equivFun_apply
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
m m' : M
eq :
  Eq (α := Dual R (Dual R M)) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m : Dual R (Dual R M))
    ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m' : Dual R (Dual R M))
⊢ ∀ (x : Dual R M), Eq.{uR + 1} (α := R) ((x : (a : M) → R) m : R) ((x : (a : M) → R) m' : R)

Tactic:
simp_rw [LinearMap.ext_iff, Dual.eval_apply] at eq

Premises used: Module.Dual.eval_apply, LinearMap.ext_iff
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
m m' : M
eq : ∀ (x : Dual R M), Eq.{uR + 1} (α := R) ((x : (a : M) → R) m : R) ((x : (a : M) → R) m' : R)
⊢ m = m'

Tactic:
b.ext_elem fun i ↦ eq (b.coord i)

Premises used: Module.Basis.coord, Module.Basis.ext_elem
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
m m' : M
eq : ∀ (x : Dual R M), Eq.{uR + 1} (α := R) ((x : (a : M) → R) m : R) ((x : (a : M) → R) m' : R)
⊢ m = m'

Tactic:
exact b.ext_elem fun i ↦ eq (b.coord i)

Premises used: Module.Basis.coord, Module.Basis.ext_elem
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
⊢ Eq (α := Submodule R M) (ker (Dual.eval R M)) ⊥

Tactic:
ker_eq_bot_of_injective (eval_injective b)

Premises used: Module.Basis.eval_injective, LinearMap.ker_eq_bot_of_injective
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : Finite ι
b : Basis ι R M
intro : ∀ (val : Fintype ι), Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤
⊢ Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
intro : (b.dualBasis.toDual ∘ₗ b.toDual).range = ⊤
intro₁ : map b.dualBasis.toDual b.toDual.range = ⊤
intro₂ : map b.dualBasis.toDual ⊤ = ⊤
intro₃ : b.dualBasis.toDual.range = ⊤
intro₄ intro₅ : Eq (α := Submodule R (Dual R (Dual R M))) ⊤ ⊤
⊢ Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤

Tactic:
rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]

Premises used: Submodule.map_top, LinearMap.range_comp, Module.Basis.toDual_range, Module.Basis.toDual_toDual
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : Finite ι
b : Basis ι R M
intro : ∀ (val : Fintype ι), Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤
⊢ Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤

Tactic:
classical
    cases nonempty_fintype ι
    rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]

Premises used: Submodule.map_top, LinearMap.range_comp, Module.Basis.toDual_range, nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
i : ι
f : M
⊢ Eq.{uR + 1} (α := R)
    ((b.dualBasis.coord i : (a : Dual R M) → R) ((b.toDualEquiv : (a : M) → Dual R M) f : Dual R M) : R)
    ((b.coord i : (a : M) → R) f : R)

Tactic:
simp [-toDualEquiv_apply, Basis.dualBasis]

Premises used: Module.Basis.toDualEquiv_apply, Module.Basis.dualBasis
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
i : ι
f : Dual R M
⊢ Eq.{uR + 1} (α := R) ((b.coord i : (a : M) → R) ((b.toDualEquiv.symm : (a : Dual R M) → M) f : M) : R)
    ((b.dualBasis.coord i : (a : Dual R M) → R) f : R)

Tactic:
simp [Basis.dualBasis]

Premises used: Module.Basis.dualBasis
-- 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 : Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
haveI :
  ∀ (this : DecidableEq ι),
    Eq.{uR + 1} (α := R)
      ((((Finsupp.linearCombination R b.coord : (a : ι →₀ R) → M →ₗ[R] R) f : M →ₗ[R] R) : (a : M) → R)
          ((b : (a : ι) → M) i : M) :
        R)
      ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R b.coord : (a : ι →₀ R) → M →ₗ[R] R) f : M →ₗ[R] R) : (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)

Tactic:
haveI := Classical.decEq ι
-- 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 : Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
this : DecidableEq ι
rw :
  Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R (⇑b.dualBasis : (a : ι) → Dual R M) : (a : ι →₀ R) → M →ₗ[R] R) f : M →ₗ[R] R) :
          (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
rw₁ rw₂ : Eq.{uR + 1} (α := R) ((f : (a : ι) → R) i : R) ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R b.coord : (a : ι →₀ R) → M →ₗ[R] R) f : M →ₗ[R] R) : (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)

Tactic:
rw [← coe_dualBasis, linearCombination_dualBasis]

Premises used: Module.Basis.coe_dualBasis, Module.Basis.linearCombination_dualBasis
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
i : ι
rw :
  Membership.mem (γ := Set ι) {i : ι | Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)} i ↔
    Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)
rw₁ rw₂ :
  Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R) ↔ Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)
⊢ i ∈ ⋯.toFinset (s := {i : ι | Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)}) ↔
    Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)

Tactic:
rw [Set.Finite.mem_toFinset, Set.mem_setOf_eq]

Premises used: Set.Finite.mem_toFinset, Set.mem_setOf_eq
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((h.coeffs m : (a : ι) → R) i : R) ((ε i : (a : M) → R) m : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
l : ι →₀ R
⊢ lc e l = (Finsupp.linearCombination R e : (a : ι →₀ R) → M) l

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, rfl, Module.DualBases.lc
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
rw :
  Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : ι) → R) i : R) (e i)) : R)
    ((l : (a : ι) → R) i : R)
h₀ :
  ∀ (b : ι),
    Ne.{u_1 + 1} (α := R) ((l : (a : ι) → R) b : R) (0 : R) →
      b ≠ i →
        Eq.{u_1 + 1} (α := R)
          ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : ι) → R) b : R) (e b)) : R) (0 : R)
h₁ :
  Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R) →
    Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (e i)) : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (lc e l) : R) ((l : (a : ι) → R) i : R)

Tactic:
rw [lc, map_finsuppSum, Finsupp.sum_eq_single i (g := fun a b ↦ (ε i) (b • e a))]

Premises used: Finsupp.sum_eq_single, map_finsuppSum, Module.DualBases.lc
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : ι) → R) i : R) (e i)) : R)
    ((l : (a : ι) → R) i : R)

Tactic:
simp [h.eval_same, smul_eq_mul]

Premises used: Module.DualBases.eval_same, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i q : ι
h₀ :
  Ne.{u_1 + 1} (α := R) ((l : (a : ι) → R) q : R) (0 : R) →
    q ≠ i →
      Eq.{u_1 + 1} (α := R)
        ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : ι) → R) q : R) (e q)) : R) (0 : R)
⊢ Ne.{u_1 + 1} (α := R) ((l : (a : ι) → R) q : R) (0 : R) →
    q ≠ i →
      Eq.{u_1 + 1} (α := R)
        ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : ι) → R) q : R) (e q)) : R) (0 : R)

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i q : ι
h_1 : Ne.{u_1 + 1} (α := R) ((l : (a : ι) → R) q : R) (0 : R)
q_ne : q ≠ i
⊢ Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : ι) → R) q : R) (e q)) : R)
    (0 : R)

Tactic:
simp [h.eval_of_ne q_ne.symm, smul_eq_mul]

Premises used: Module.DualBases.eval_of_ne, Ne.symm, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R) →
    Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (e i)) : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((h.coeffs (lc e l) : (a : ι) → R) i : R) ((l : (a : ι) → R) i : R)
⊢ h.coeffs (lc e l) = l

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
h₁ : Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (lc e l) : R) ((l : (a : ι) → R) i : R)
h₂ h₃ : Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) ((l : (a : ι) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R) ((h.coeffs (lc e l) : (a : ι) → R) i : R) ((l : (a : ι) → R) i : R)

Tactic:
rw [h.coeffs_apply, h.dual_lc]

Premises used: Module.DualBases.dual_lc, Module.DualBases.coeffs_apply
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
⊢ ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (lc e (h.coeffs m)) : R) ((ε i : (a : M) → R) m : R)

Tactic:
simp [h.dual_lc]

Premises used: Module.DualBases.dual_lc
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
v w : M
h₁ :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R) ((h.coeffs (v + w) : (a : ι) → R) i : R) ((h.coeffs v + h.coeffs w : (a : ι) → R) i : R)
⊢ h.coeffs (v + w) = h.coeffs v + h.coeffs w

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
v w : M
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((h.coeffs (v + w) : (a : ι) → R) i : R) ((h.coeffs v + h.coeffs w : (a : ι) → R) i : R)

Tactic:
(ε i).map_add v w

Premises used: LinearMap.map_add
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
v w : M
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((h.coeffs (v + w) : (a : ι) → R) i : R) ((h.coeffs v + h.coeffs w : (a : ι) → R) i : R)

Tactic:
exact (ε i).map_add v w

Premises used: LinearMap.map_add
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
c : R
v : M
h₁ :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R) ((h.coeffs (c • v) : (a : ι) → R) i : R)
      ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.coeffs v) : (a : ι) → R) i : R)
⊢ h.coeffs (c • v) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.coeffs v)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
c : R
v : M
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((h.coeffs (c • v) : (a : ι) → R) i : R)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.coeffs v) : (a : ι) → R) i : R)

Tactic:
(ε i).map_smul c v

Premises used: LinearMap.map_smul
-- Module: Mathlib.LinearAlgebra.Dual.Basis
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
c : R
v : M
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((h.coeffs (c • v) : (a : ι) → R) i : R)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.coeffs v) : (a : ι) → R) i : R)

Tactic:
exact (ε i).map_smul c v

Premises used: LinearMap.map_smul