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
x : M
i_1 : ι
h_1 : Nontrivial R
i : ι
h :
  ∀ (j : ι),
    Eq.{u_11 + 1} (α := 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))
          ((b : (a : ι) → M) i) j :
        R)
      ((single i 1 : (a : ι) → R) j : R)
⊢ Eq (α := ι → 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))
      ((b : (a : ι) → M) i))
    (⇑(single i 1) : (a : ι) → R)

Tactic:
ext j
-- 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_1 : ι
h_1 : Nontrivial R
i j : ι
h :
  Eq.{u_11 + 1} (α := 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) :
          (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) j)
            ⋯ :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      R)
    ((single i 1 : (a : ι) → R) j : R)
⊢ Eq.{u_11 + 1} (α := 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))
        ((b : (a : ι) → M) i) j :
      R)
    ((single i 1 : (a : ι) → R) j : R)

Tactic:
simp only [reindexRange_repr_self]

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

Tactic:
apply Finsupp.single_apply_left (f := fun i => (⟨b i, _⟩ : Set.range b))

Premises used: Finsupp.single_apply_left
-- 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_1 : ι
h : Nontrivial R
i j : ι
⊢ Injective.{u_10 + 1, u_12 + 1} (β :=
    { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
      ((b : (a : ι) → M) i) ⋯

Tactic:
fun i j h => b.injective (Subtype.mk.inj h)

Premises used: Module.Basis.injective, Subtype.mk.inj, Function.Injective
-- 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_1 : ι
h : Nontrivial R
i j : ι
⊢ Injective.{u_10 + 1, u_12 + 1} (β :=
    { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
      ((b : (a : ι) → M) i) ⋯

Tactic:
exact fun i j h => b.injective (Subtype.mk.inj h)

Premises used: Module.Basis.injective, Subtype.mk.inj
-- 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 : ι
h :
  Membership.mem.{u_12, u_12} (α := M) (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M))
    ((b : (a : ι) → M) i : M)
⊢ 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)
            h :
          { 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)

Tactic:
b.reindexRange_repr' _ rfl

Premises used: Module.Basis.reindexRange_repr', rfl
-- 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
inst_8 : Fintype ι
inst_9 : DecidableEq M
⊢ ∀ (a : M),
    Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) a ↔
      Membership.mem (α := M) (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)
        ((Equiv.refl M : (a : M) → M) a : M)

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
inst_3 : Fintype ι
inst_4 : DecidableEq M
i : ι
h :
  Membership.mem.{u_12, u_12} (α := M) (γ := Finset M)
    (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) ((b : (a : ι) → M) i : M)
rw :
  Eq.{u_12 + 1} (α := M)
    ((↑((Equiv.symm
                ((Equiv.refl M).subtypeEquiv (p :=
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M))) (q :=
                  Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ))
                  ⋯) :
              (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → (↑(range (⇑b : (a : ι) → M)) : Type u_12))
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
              ((b : (a : ι) → M) i) h)) :
        M) :
      M)
    ((b : (a : ι) → M) i : M)
⊢ Eq.{u_12 + 1} (α := M)
    ((b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
            ((b : (a : ι) → M) i) h :
          ↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) :
      M)
    ((b : (a : ι) → M) i : M)

Tactic:
rw [reindexFinsetRange, reindex_apply, reindexRange_apply]

Premises used: Module.Basis.reindexFinsetRange, Module.Basis.reindexRange_apply, 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
inst_3 : Fintype ι
inst_4 : DecidableEq M
i : ι
h :
  Membership.mem.{u_12, u_12} (α := M) (γ := Finset M)
    (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) ((b : (a : ι) → M) i : M)
⊢ Eq.{u_12 + 1} (α := M)
    ((↑((Equiv.symm
                ((Equiv.refl M).subtypeEquiv (p :=
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M))) (q :=
                  Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ))
                  ⋯) :
              (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → (↑(range (⇑b : (a : ι) → M)) : Type u_12))
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
              ((b : (a : ι) → M) i) h)) :
        M) :
      M)
    ((b : (a : ι) → M) i : M)

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
inst_3 : Fintype ι
inst_4 : DecidableEq M
x : ↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)
rcases :
  ∀ (bi : M)
    (hbi : Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) bi),
    (b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
          hbi) =
      (↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
            hbi) :
        M)
⊢ (b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M) x = (↑x : M)

Tactic:
rcases x with ⟨bi, hbi⟩
-- 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
inst_3 : Fintype ι
inst_4 : DecidableEq M
bi : M
hbi : Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) bi
rcases :
  ∀ (i : ι)
    (hbi :
      Membership.mem.{u_12, u_12} (α := M) (γ := Finset M)
        (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) ((b : (a : ι) → M) i : M)),
    Eq.{u_12 + 1} (α := M)
      ((b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M)
          (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
              ((b : (a : ι) → M) i) hbi :
            ↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) :
        M)
      ((↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
              ((b : (a : ι) → M) i) hbi) :
          M) :
        M)
⊢ (b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi hbi) =
    (↑(Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
          hbi) :
      M)

Tactic:
rcases Finset.mem_image.mp hbi with ⟨i, -, rfl⟩

Premises used: Finset.mem_image, Iff.mp, 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
inst_3 : Fintype ι
inst_4 : DecidableEq M
i : ι
hbi :
  Membership.mem.{u_12, u_12} (α := M) (γ := Finset M)
    (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) ((b : (a : ι) → M) i : M)
⊢ Eq.{u_12 + 1} (α := M)
    ((b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
            ((b : (a : ι) → M) i) hbi :
          ↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) :
      M)
    ((↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
            ((b : (a : ι) → M) i) hbi) :
        M) :
      M)

Tactic:
b.reindexFinsetRange_self i

Premises used: Finset.mem_univ, Finset.mem_image_of_mem, DFunLike.coe, Module.Basis.reindexFinsetRange_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
inst_3 : Fintype ι
inst_4 : DecidableEq M
i : ι
hbi :
  Membership.mem.{u_12, u_12} (α := M) (γ := Finset M)
    (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) ((b : (a : ι) → M) i : M)
⊢ Eq.{u_12 + 1} (α := M)
    ((b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
            ((b : (a : ι) → M) i) hbi :
          ↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) :
      M)
    ((↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
            ((b : (a : ι) → M) i) hbi) :
        M) :
      M)

Tactic:
exact b.reindexFinsetRange_self i

Premises used: Finset.mem_univ, Finset.mem_image_of_mem, DFunLike.coe, Module.Basis.reindexFinsetRange_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
inst_3 : Fintype ι
inst_4 : DecidableEq M
i : ι
h :
  ∀ (bi : M)
    (hbi : Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) bi),
    Eq.{u_11 + 1} (α := R)
      ((((repr b.reindexFinsetRange : (a : M) → ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ) →₀ R)
                ((b : (a : ι) → M) i) :
              Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R) :
            (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → R)
          (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
            hbi) :
        R)
      (((single
                (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
                  ((b : (a : ι) → M) i) ⋯)
                1 :
              Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R) :
            (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → R)
          (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
            hbi) :
        R)
⊢ Eq (α := Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R)
    ((repr b.reindexFinsetRange : (a : M) → ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ) →₀ R) ((b : (a : ι) → M) i) :
      Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R)
    (single
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
          ((b : (a : ι) → M) i) ⋯)
        1 :
      Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R)

Tactic:
ext ⟨bi, hbi⟩
-- 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
inst_3 : Fintype ι
inst_4 : DecidableEq M
i : ι
bi : M
hbi : Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) bi
⊢ Eq.{u_11 + 1} (α := 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) :
          (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
        ((Equiv.symm
                ((Equiv.refl M).subtypeEquiv (p :=
                  Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M))) (q :=
                  Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ))
                  ⋯) :
              (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → (↑(range (⇑b : (a : ι) → M)) : Type u_12))
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
              hbi) :
          (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12)) :
      R)
    (((single
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
                ((b : (a : ι) → M) i) ⋯)
              1 :
            Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R) :
          (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → R)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
          hbi) :
      R)

Tactic:
simp [Finsupp.single_apply]

Premises used: Finsupp.single_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
inst_3 : Fintype ι
inst_4 : DecidableEq M
x : M
i : ι
h :
  Membership.mem.{u_12, u_12} (α := M) (γ := Finset M)
    (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) ((b : (a : ι) → M) i : M)
⊢ Eq.{u_11 + 1} (α := R)
    ((((repr b.reindexFinsetRange : (a : M) → ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ) →₀ R) x :
            Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R) :
          (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → R)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
            ((b : (a : ι) → M) i) h :
          ↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) :
      R)
    ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
simp [reindexFinsetRange]

Premises used: Module.Basis.reindexFinsetRange
-- 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
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
f g : ι → M'
⊢ linearCombination R id ∘ₗ lmapDomain R R (f + g) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) =
    HAdd.hAdd (α := M →ₗ[R] M') (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))
      (linearCombination R id ∘ₗ lmapDomain R R g ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))

Tactic:
b.ext fun i => ?_

Premises used: Module.Basis.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
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
f g : ι → M'
refine :
  ∀ (i : ι),
    Eq.{u_7 + 1} (α := M')
      ((linearCombination R id ∘ₗ lmapDomain R R (f + g) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → M')
          ((b : (a : ι) → M) i : M) :
        M')
      ((HAdd.hAdd (α := M →ₗ[R] M') (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))
              (linearCombination R id ∘ₗ lmapDomain R R g ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)) :
            (a : M) → M')
          ((b : (a : ι) → M) i : M) :
        M')
⊢ linearCombination R id ∘ₗ lmapDomain R R (f + g) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) =
    HAdd.hAdd (α := M →ₗ[R] M') (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))
      (linearCombination R id ∘ₗ lmapDomain R R g ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))

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

Premises used: Module.Basis.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
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
f g : ι → M'
i : ι
⊢ Eq.{u_7 + 1} (α := M')
    ((linearCombination R id ∘ₗ lmapDomain R R (f + g) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → M')
        ((b : (a : ι) → M) i : M) :
      M')
    ((HAdd.hAdd (α := M →ₗ[R] M') (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))
            (linearCombination R id ∘ₗ lmapDomain R R g ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)) :
          (a : M) → M')
        ((b : (a : ι) → M) i : M) :
      M')

Tactic:
simp