awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (f_i : (a : M) → R) x = f x i

Tactic:
rfl

Premises used: 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
x₁ : Eq.{u_11 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) ((f_i : (a : M) → R) x : R)
⊢ (((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i = f x i

Tactic:
calc
    b.repr x i = f_i x := by
      { rw [← this]
        rfl }
    _ = f x i := rfl

Premises used: Module.Basis.repr, DFunLike.coe, 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₁ b₂ : Basis ι R M
h :
  ∀ (x : M) (i : ι),
    Eq.{u_11 + 1} (α := R) ((((b₁.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
      ((((b₂.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
h₁ :
  ∀ (x : M) (a : ι),
    Eq.{u_11 + 1} (α := R) ((((b₁.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)
      ((((b₂.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)
⊢ b₁.repr = b₂.repr

Tactic:
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₁ b₂ : Basis ι R M
h :
  ∀ (x : M) (i : ι),
    Eq.{u_11 + 1} (α := R) ((((b₁.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
      ((((b₂.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
x : M
a : ι
⊢ Eq.{u_11 + 1} (α := R) ((((b₁.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)
    ((((b₂.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)

Tactic:
apply h
-- 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₁ b₂ : Basis ι R M
⊢ (∀ (i : ι), Eq.{u_12 + 1} (α := M) ((b₁ : (a : ι) → M) i : M) ((b₂ : (a : ι) → M) i : M)) → b₁ = b₂

Tactic:
DFunLike.ext _ _

Premises used: DFunLike.ext
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
R' : Type u_13
inst_8 : Semiring R'
inst_9 : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') c : R') x = c • x
this : Module R' R := compHom R (↑f.symm : R' →+* R)
x : R'
y : R
z : M
change : HMul.hMul (α := R) ((f.symm : (a : R') → R) x : R) y • z = x • y • z
⊢ (x • y) • z = x • y • z

Tactic:
change (f.symm x * y) • z = x • (y • z)

Premises used: HMul.hMul, HSMul.hSMul, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
R' : Type u_13
inst_8 : Semiring R'
inst_9 : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') c : R') x = c • x
this : Module R' R := compHom R (↑f.symm : R' →+* R)
x : R'
y : R
z : M
rw : HSMul.hSMul.{u_11, u_12, u_12} (α := R) ((f.symm : (a : R') → R) x : R) (y • z) = x • y • z
rw₁ :
  HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') ((f.symm : (a : R') → R) x : R) : R') (y • z) = x • y • z
rw₂ rw₃ : x • y • z = x • y • z
⊢ HMul.hMul (α := R) ((f.symm : (a : R') → R) x : R) y • z = x • y • z

Tactic:
rw [mul_smul, ← h, f.apply_symm_apply]

Premises used: RingEquiv.apply_symm_apply, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
R' : Type u_13
inst_8 : Semiring R'
inst_9 : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') c : R') x = c • x
this : Module R' R := compHom R (↑f.symm : R' →+* R)
⊢ IsScalarTower R' R M

Tactic:
haveI : IsScalarTower R' R M :=
    { smul_assoc := fun x y z => by
        change (f.symm x * y) • z = x • (y • z)
        rw [mul_smul, ← h, f.apply_symm_apply] }
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
R' : Type u_13
inst_8 : Semiring R'
inst_9 : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') c : R') x = c • x
this_1 : Module R' R := compHom R (↑f.symm : R' →+* R)
this : IsScalarTower R' R M
⊢ Basis ι R' M

Tactic:
exact ofRepr <| (b.repr.restrictScalars R').trans <|
    Finsupp.mapRange.linearEquiv (Module.compHom.toLinearEquiv f.symm).symm

Premises used: Module.Basis.ofRepr, LinearEquiv.symm, LinearEquiv.restrictScalars, Finsupp.mapRange.linearEquiv, Module.Basis.repr, Module.compHom.toLinearEquiv, LinearEquiv.trans, RingEquiv.symm
-- 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'
inst_4 : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') c : R') x = c • x
i : ι
⊢ Eq (α := ι →₀ R') (((b.mapCoeffs f h).repr : (a : M) → ι →₀ R') ((b : (a : ι) → M) i) : ι →₀ R')
    (single i 1 : ι →₀ R')

Tactic:
simp
-- 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'
inst_4 : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') c : R') x = c • x
⊢ Eq (α := (a : ι) → M) (⇑(b.mapCoeffs f h) : (a : ι) → M) (⇑b : (a : ι) → M)

Tactic:
funext <| b.mapCoeffs_apply f h

Premises used: funext, Module.Basis.mapCoeffs_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
i : ι
h :
  Membership.mem.{u_12, u_12} (α := M) (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M))
    ((b : (a : ι) → M) i : M)
inl :
  Subsingleton R →
    Eq.{u_12 + 1} (α := M)
      ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
          (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
              h :
            { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
        M)
      ((b : (a : ι) → M) i : M)
inr :
  Nontrivial R →
    Eq.{u_12 + 1} (α := M)
      ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
          (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
              h :
            { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
        M)
      ((b : (a : ι) → M) i : M)
⊢ Eq.{u_12 + 1} (α := M)
    ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            h :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      M)
    ((b : (a : ι) → M) i : M)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- 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
i : ι
h :
  Membership.mem.{u_12, u_12} (α := M) (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M))
    ((b : (a : ι) → M) i : M)
h_1 : Subsingleton R
this : Subsingleton M := ⋯
⊢ Eq.{u_12 + 1} (α := M)
    ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            h :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      M)
    ((b : (a : ι) → M) i : M)

Tactic:
simp [reindexRange, eq_iff_true_of_subsingleton]

Premises used: Module.Basis.reindexRange, eq_iff_true_of_subsingleton
-- 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
i : ι
h :
  Membership.mem.{u_12, u_12} (α := M) (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M))
    ((b : (a : ι) → M) i : M)
h_1 : Nontrivial R
⊢ Eq.{u_12 + 1} (α := M)
    ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            h :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      M)
    ((b : (a : ι) → M) i : M)

Tactic:
simp [*, reindexRange, reindex_apply]

Premises used: Module.Basis.reindexRange, Module.Basis.reindex_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
i : ι
⊢ Eq (α := Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R)
    ((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) ((b : (a : ι) → M) i) :
      Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R)
    (single
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i) ⋯)
        1 :
      Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R)

Tactic:
calc
    b.reindexRange.repr (b i) = b.reindexRange.repr (b.reindexRange ⟨b i, mem_range_self i⟩) :=
      congr_arg _ (b.reindexRange_self _ _).symm
    _ = Finsupp.single ⟨b i, mem_range_self i⟩ 1 := b.reindexRange.repr_self _

Premises used: Module.Basis.reindexRange_self, Trans.trans, Module.Basis.reindexRange, congr_arg, Eq.symm, 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
x : (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12)
rcases :
  ∀ (i : ι),
    Eq.{u_12 + 1} (α := M)
      ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
          (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
              ⋯ :
            { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
        M)
      ((↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
              ⋯) :
          M) :
        M)
⊢ (b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M) x = (↑x : M)

Tactic:
rcases x with ⟨bi, ⟨i, rfl⟩⟩

Premises used: 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
i : ι
⊢ Eq.{u_12 + 1} (α := M)
    ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            ⋯ :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      M)
    ((↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            ⋯) :
        M) :
      M)

Tactic:
b.reindexRange_self i

Premises used: Set.mem_range_self, Module.Basis.reindexRange_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
i : ι
⊢ Eq.{u_12 + 1} (α := M)
    ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            ⋯ :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      M)
    ((↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            ⋯) :
        M) :
      M)

Tactic:
exact b.reindexRange_self i

Premises used: Set.mem_range_self, Module.Basis.reindexRange_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
x bi : M
i : ι
h : (b : (a : ι) → M) i = bi
⊢ Nontrivial R

Tactic:
nontriviality
-- 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 bi : M
i : ι
h : (b : (a : ι) → M) i = bi
h_1 : Nontrivial R
subst :
  Eq.{u_11 + 1} (α := R)
    ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
            Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
          (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            ⋯ :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      R)
    ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
⊢ Eq.{u_11 + 1} (α := R)
    ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
            Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
          (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) bi ⋯) :
      R)
    ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
subst h
-- 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_1 : M
i_1 : ι
h : Nontrivial R
x y : M
i : ι
⊢ (fun (x : M) (i : ι) ↦
        ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
              (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
            (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                ((b : (a : ι) → M) i) ⋯ :
              { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
          R))
      (x + y) i =
    HAdd.hAdd (α := ι → R) (β := ι → R)
      ((fun (x : M) (i : ι) ↦
          ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                  Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
                (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
              (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                  ((b : (a : ι) → M) i) ⋯ :
                { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
            R))
        x)
      ((fun (x : M) (i : ι) ↦
          ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                  Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
                (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
              (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                  ((b : (a : ι) → M) i) ⋯ :
                { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
            R))
        y)
      i

Tactic:
simp only [Pi.add_apply, map_add, Finsupp.coe_add]

Premises used: map_add, Pi.add_apply, Finsupp.coe_add
-- 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_1 : M
i : ι
h_1 : Nontrivial R
c : R
x : M
h :
  ∀ (i : ι),
    (fun (x : M) (i : ι) ↦
          ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                  Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
                (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
              (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                  ((b : (a : ι) → M) i) ⋯ :
                { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
            R))
        (c • x) i =
      HSMul.hSMul (β := ι → R) c
        ((fun (x : M) (i : ι) ↦
            ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                    Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
                  (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
                (Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                    ((b : (a : ι) → M) i) ⋯ :
                  { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
              R))
          x)
        i
⊢ (fun (x : M) (i : ι) ↦
        ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
              (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
            (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                ((b : (a : ι) → M) i) ⋯ :
              { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
          R))
      (c • x) =
    HSMul.hSMul (β := ι → R) c
      ((fun (x : M) (i : ι) ↦
          ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                  Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
                (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
              (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                  ((b : (a : ι) → M) i) ⋯ :
                { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
            R))
        x)

Tactic:
ext i
-- 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_1 : M
i_1 : ι
h : Nontrivial R
c : R
x : M
i : ι
⊢ (fun (x : M) (i : ι) ↦
        ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
              (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
            (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                ((b : (a : ι) → M) i) ⋯ :
              { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
          R))
      (c • x) i =
    HSMul.hSMul (β := ι → R) c
      ((fun (x : M) (i : ι) ↦
          ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
                  Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
                (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
              (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                  ((b : (a : ι) → M) i) ⋯ :
                { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
            R))
        x)
      i

Tactic:
simp