awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
e : ι ≃ ι'
⊢ Eq (α := (a : ι') → M) (⇑(b.reindex e) : (a : ι') → M)
    (comp.{u_2 + 1, u_1 + 1, u_6 + 1} (β := ι) (⇑b : (a : ι) → M) (⇑e.symm : (a : ι') → ι))

Tactic:
funext (b.reindex_apply e)

Premises used: funext, Module.Basis.reindex_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x : M
e : ι ≃ ι'
i' : ι'
⊢ Eq.{u_3 + 1} (α := R)
    ((((Finsupp.domLCongr e : (a : ι →₀ R) → ι' →₀ R) ((b.repr : (a : M) → ι →₀ R) x) : ι' →₀ R) : (a : ι') → R) i' : R)
    ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) ((e.symm : (a : ι') → ι) i' : ι) : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x : M
e : ι ≃ ι'
⊢ ∀ (x_1 : ι'),
    Eq.{u_3 + 1} (α := R) (((((b.reindex e).repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) x_1 : R)
      ((mapDomain.{u_1, u_2, u_3} (α := ι) (⇑e : (a : ι) → ι') ((b.repr : (a : M) → ι →₀ R) x) : (a : ι') → R) x_1 : R)

Tactic:
simp [repr_reindex_apply]

Premises used: Module.Basis.repr_reindex_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
⊢ b.reindex (Equiv.refl ι) = b

Tactic:
simp [reindex]

Premises used: Module.Basis.reindex
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
e : ι ≃ ι'
⊢ Eq.{u_6 + 1} (α := Set M) (range.{u_6, u_2 + 1} (ι := ι') (⇑(b.reindex e) : (a : ι') → M))
    (range.{u_6, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))

Tactic:
simp [coe_reindex, range_comp]

Premises used: Set.range_comp, Module.Basis.coe_reindex
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
b : Basis ι R M
x : ι → R
⊢ Eq.{u_6 + 1} (α := M) ((b.equivFun.symm : (a : ι → R) → M) x : M)
    (∑ i : ι, HSMul.hSMul (β := M) (x i) ((b : (a : ι) → M) i : M) : M)

Tactic:
simp [Basis.equivFun, Finsupp.linearCombination_apply, sum_fintype, equivFunOnFinite]

Premises used: Finsupp.sum_fintype, Finsupp.equivFunOnFinite, Finsupp.linearCombination_apply, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
u : M
⊢ Eq (α := ι → R) ((b.equivFun : (a : M) → ι → R) u : ι → R)
    ((⇑((b.repr : (a : M) → ι →₀ R) u : ι →₀ R) : (a : ι) → R) : (a : ι) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
M' : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : Finite ι
b : Basis ι R M
f : M ≃ₗ[R] M'
⊢ (b.map f).equivFun = f.symm ≪≫ₗ b.equivFun

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.toEquiv, LinearEquiv.trans, rfl, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
b : Basis ι R M
u : M
rw : (b.equivFun.symm : (a : ι → R) → M) ((b.equivFun : (a : M) → ι → R) u : ι → R) = u
rw₁ rw₂ : u = u
⊢ ∑ i : ι,
      HSMul.hSMul.{u_3, u_6, u_6} (α := R) (β := M) ((b.equivFun : (a : M) → ι → R) u i : R) ((b : (a : ι) → M) i : M) =
    u

Tactic:
rw [← b.equivFun_symm_apply, b.equivFun.symm_apply_apply]

Premises used: Module.Basis.equivFun_symm_apply, LinearEquiv.symm_apply_apply, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
b : Basis ι R M
u : M
⊢ ∑ i : ι,
      HSMul.hSMul.{u_3, u_6, u_6} (α := R) (β := M) ((((b.repr : (a : M) → ι →₀ R) u : ι →₀ R) : (a : ι) → R) i : R)
        ((b : (a : ι) → M) i : M) =
    u

Tactic:
b.sum_equivFun u

Premises used: Module.Basis.sum_equivFun
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
inst_4 : DecidableEq ι
b : Basis ι R M
i j : ι
rw :
  Eq.{u_3 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) : (a : ι) → R) j : R)
    (if i = j then 1 else 0 : R)
rw₁ rw₂ : Eq.{u_3 + 1} (α := R) (if i = j then 1 else 0) (if i = j then 1 else 0)
⊢ Eq.{u_3 + 1} (α := R) ((b.equivFun : (a : M) → ι → R) ((b : (a : ι) → M) i : M) j : R) (if i = j then 1 else 0 : R)

Tactic:
rw [b.equivFun_apply, b.repr_self_apply]

Premises used: Module.Basis.repr_self_apply, Module.Basis.equivFun_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
b : Basis ι R M
c : ι → R
simp_rw : (⇑((b.repr : (a : M) → ι →₀ R) ((b.equivFun.symm : (a : ι → R) → M) c) : ι →₀ R) : (a : ι) → R) = c
simp_rw₁ : (b.equivFun : (a : M) → ι → R) ((b.equivFun.symm : (a : ι → R) → M) c : M) = c
⊢ (⇑((b.repr : (a : M) → ι →₀ R) (∑ i : ι, HSMul.hSMul (β := M) (c i) ((b : (a : ι) → M) i : M))) : (a : ι) → R) = c

Tactic:
simp_rw [← b.equivFun_symm_apply, ← b.equivFun_apply, b.equivFun.apply_symm_apply]

Premises used: Module.Basis.equivFun_symm_apply, Module.Basis.equivFun_apply, LinearEquiv.apply_symm_apply, Module.Basis.equivFun
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
e : M ≃ₗ[R] ι → R
x : M
i : ι
⊢ Eq.{u_3 + 1} (α := R) (((((ofEquivFun e).repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
    ((e : (a : M) → ι → R) x i : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
inst_4 : DecidableEq ι
e : M ≃ₗ[R] ι → R
i j : ι
⊢ Eq.{u_3 + 1} (α := R) ((e : (a : M) → ι → R) ((ofEquivFun e : (a : ι) → M) i : M) j : R)
    ((e : (a : M) → ι → R) ((e.symm : (a : ι → R) → M) (Pi.single (M := fun (a : ι) ↦ R) i 1) : M) j : R)

Tactic:
simp [Basis.ofEquivFun, ← Finsupp.single_eq_pi_single]

Premises used: Module.Basis.ofEquivFun, Finsupp.single_eq_pi_single
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
v : Basis ι R M
h :
  ∀ (x : M) (a : ι),
    Eq.{u_3 + 1} (α := R) (((((ofEquivFun v.equivFun).repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)
      ((((v.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)
⊢ (ofEquivFun v.equivFun).repr = v.repr

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
v : Basis ι R M
x : M
a : ι
⊢ Eq.{u_3 + 1} (α := R) (((((ofEquivFun v.equivFun).repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)
    ((((v.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
e : M ≃ₗ[R] ι → R
h :
  ∀ (j : M) (x : ι),
    Eq.{u_3 + 1} (α := R) (((ofEquivFun e).equivFun : (a : M) → ι → R) j x : R) ((e : (a : M) → ι → R) j x : R)
⊢ (ofEquivFun e).equivFun = e

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
e : M ≃ₗ[R] ι → R
j : M
x : ι
h :
  Eq.{u_3 + 1} (α := R) (((((ofEquivFun e).repr : (a : M) → ι →₀ R) j : ι →₀ R) : (a : ι) → R) x : R)
    ((e : (a : M) → ι → R) j x : R)
⊢ Eq.{u_3 + 1} (α := R) (((ofEquivFun e).equivFun : (a : M) → ι → R) j x : R) ((e : (a : M) → ι → R) j x : R)

Tactic:
simp_rw [Basis.equivFun_apply, Basis.ofEquivFun_repr_apply]

Premises used: Module.Basis.ofEquivFun_repr_apply, Module.Basis.equivFun_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
R₁ : Type u_13
inst_3 : Semiring R₁
σ : R →+* R₁
M₁ : Type u_14
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h :
  ∀ (i : ι),
    Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
      ((f₂ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
h₁ : ∀ (x : M), Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) x : M₁) ((f₂ : (a : M) → M₁) x : M₁)
⊢ f₁ = f₂

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
R₁ : Type u_13
inst_3 : Semiring R₁
σ : R →+* R₁
M₁ : Type u_14
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h :
  ∀ (i : ι),
    Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
      ((f₂ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
x : M
h₁ :
  Eq.{u_14 + 1} (α := M₁)
    ((f₁ : (a : M) → M₁)
        (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
          HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
            ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
      M₁)
    ((f₂ : (a : M) → M₁)
        (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
          HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
            ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
      M₁)
⊢ Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) x : M₁) ((f₂ : (a : M) → M₁) x : M₁)

Tactic:
rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, Module.Basis.linearCombination_repr
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
R₁ : Type u_13
inst_3 : Semiring R₁
σ : R →+* R₁
M₁ : Type u_14
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h :
  ∀ (i : ι),
    Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
      ((f₂ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
x : M
⊢ Eq.{u_14 + 1} (α := M₁)
    ((f₁ : (a : M) → M₁)
        (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
          HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
            ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
      M₁)
    ((f₂ : (a : M) → M₁)
        (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
          HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
            ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
      M₁)

Tactic:
simp only [map_sum, map_smulₛₗ, h]

Premises used: MulActionSemiHomClass.map_smulₛₗ, map_sum
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
R₁ : Type u_13
inst_3 : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
M₁ : Type u_14
inst_6 : AddCommMonoid M₁
inst_7 : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h :
  ∀ (i : ι),
    Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
      ((f₂ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
h₁ : ∀ (x : M), Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) x : M₁) ((f₂ : (a : M) → M₁) x : M₁)
⊢ f₁ = f₂

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
R₁ : Type u_13
inst_3 : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
M₁ : Type u_14
inst_6 : AddCommMonoid M₁
inst_7 : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h :
  ∀ (i : ι),
    Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
      ((f₂ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
x : M
h₁ :
  Eq.{u_14 + 1} (α := M₁)
    ((f₁ : (a : M) → M₁)
        (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
          HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
            ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
      M₁)
    ((f₂ : (a : M) → M₁)
        (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
          HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
            ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
      M₁)
⊢ Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) x : M₁) ((f₂ : (a : M) → M₁) x : M₁)

Tactic:
rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, Module.Basis.linearCombination_repr
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
R₁ : Type u_13
inst_3 : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
M₁ : Type u_14
inst_6 : AddCommMonoid M₁
inst_7 : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h :
  ∀ (i : ι),
    Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
      ((f₂ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
x : M
⊢ Eq.{u_14 + 1} (α := M₁)
    ((f₁ : (a : M) → M₁)
        (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
          HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
            ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
      M₁)
    ((f₂ : (a : M) → M₁)
        (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
          HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
            ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
      M₁)

Tactic:
simp only [map_sum, map_smulₛₗ, h]

Premises used: MulActionSemiHomClass.map_smulₛₗ, map_sum
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x y : M
⊢ x = y ↔
    ∀ (i : ι),
      Eq.{u_11 + 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 only [← DFunLike.ext_iff, EmbeddingLike.apply_eq_iff_eq]

Premises used: DFunLike.ext_iff, EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M →ₗ[R] ι →₀ R
⊢ (↑b.repr : M →ₗ[R] ι →₀ R) = f ↔
    ∀ (i : ι), Eq (α := ι →₀ R) ((f : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) (single i 1 : ι →₀ R)

Tactic:
⟨fun h i => h ▸ b.repr_self i, fun h => b.ext fun i => (b.repr_self i).trans (h i).symm⟩

Premises used: Eq.rec, Iff.intro, Eq.symm, Module.Basis.ext, Module.Basis.repr_self, Eq.trans
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M ≃ₗ[R] ι →₀ R
⊢ b.repr = f ↔ ∀ (i : ι), Eq (α := ι →₀ R) ((f : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) (single i 1 : ι →₀ R)

Tactic:
⟨fun h i => h ▸ b.repr_self i, fun h => b.ext' fun i => (b.repr_self i).trans (h i).symm⟩

Premises used: Eq.rec, Iff.intro, Eq.symm, Module.Basis.ext', Module.Basis.repr_self, Eq.trans
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x : M
i : ι
⊢ (b : (a : ι) → M) i = x ↔ Eq (α := ι →₀ R) ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) (single i 1 : ι →₀ R)

Tactic:
⟨fun h => h ▸ b.repr_self i, fun h => b.repr.injective ((b.repr_self i).trans h.symm)⟩

Premises used: Eq.rec, Module.Basis.repr, Iff.intro, LinearEquiv.injective, Eq.symm, Module.Basis.repr_self, Eq.trans
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
x_1 x_2 : M
rw : (f x_1 + f x_2) i = f x_1 i + f x_2 i
rw₁ rw₂ : f x_1 i + f x_2 i = f x_1 i + f x_2 i
⊢ f (x_1 + x_2) i = f x_1 i + f x_2 i

Tactic:
rw [hadd, Pi.add_apply]

Premises used: Pi.add_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
x_1 : R
x_2 : M
⊢ f (x_1 • x_2) i = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x_1 : R) (f x_2 i)

Tactic:
simp [hsmul, Pi.smul_apply]

Premises used: Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
⊢ lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) = f_i

Tactic:
b.ext fun j => ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
refine :
  ∀ (j : ι),
    Eq.{u_11 + 1} (α := R) ((lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → R) ((b : (a : ι) → M) j : M) : R)
      ((f_i : (a : M) → R) ((b : (a : ι) → M) j : M) : R)
⊢ lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) = f_i

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

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
j : ι
change : (((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i = f ((b : (a : ι) → M) j) i
⊢ Eq.{u_11 + 1} (α := R) ((lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → R) ((b : (a : ι) → M) j : M) : R)
    ((f_i : (a : M) → R) ((b : (a : ι) → M) j : M) : R)

Tactic:
change b.repr (b j) i = f (b j) i

Premises used: Module.Basis.repr, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
j : ι
rw : (single j 1 : (a : ι) → R) i = f ((b : (a : ι) → M) j) i
rw₁ rw₂ : Eq.{u_11 + 1} (α := R) ((single j 1 : (a : ι) → R) i : R) ((single j 1 : (a : ι) → R) i : R)
⊢ (((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i = f ((b : (a : ι) → M) j) i

Tactic:
rw [b.repr_self, f_eq]

Premises used: Module.Basis.repr_self
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
⊢ lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) = f_i

Tactic:
have : Finsupp.lapply i ∘ₗ ↑b.repr = f_i := by
    refine b.ext fun j => ?_
    change b.repr (b j) i = f (b j) i
    rw [b.repr_self, f_eq]
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) = f_i
rw :
  Eq.{u_11 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
    ((lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → R) x : R)
⊢ Eq.{u_11 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) ((f_i : (a : M) → R) x : R)

Tactic:
rw [← this]
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) = f_i
⊢ Eq.{u_11 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
    ((lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → R) x : R)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) = f_i
rw rw₁ rw₂ :
  Eq.{u_11 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
    ((lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → R) x : R)
⊢ Eq.{u_11 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) ((f_i : (a : M) → R) x : R)

Tactic:
{ rw [← this]
        rfl }