awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
simp :
  ∀ (x : M),
    (∃ (l : ι →₀ R),
        Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l ∧
          (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = x) →
      (∃ (l : ι →₀ R),
          Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R t) l ∧
            (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = x) →
        x = 0
⊢ Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))

Tactic:
simp only [disjoint_def, Finsupp.mem_span_image_iff_linearCombination]

Premises used: Submodule.disjoint_def, Finsupp.mem_span_image_iff_linearCombination
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l₁
l₂ : ι →₀ R
hl₂ : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R t) l₂
H :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₂ : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M)
⊢ l₂ = l₁

Tactic:
rw [hv.finsuppLinearCombination_injective.eq_iff] at H

Premises used: Function.Injective.eq_iff, LinearIndependent.finsuppLinearCombination_injective
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l₁
l₂ : ι →₀ R
hl₂ : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R t) l₂
H : l₂ = l₁
⊢ Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R t) l₁

Tactic:
subst l₂
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l₁
hl₂ : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R t) l₁
⊢ l₁ = 0

Tactic:
have : l₁ = 0 := Submodule.disjoint_def.mp (Finsupp.disjoint_supported_supported hs) _ hl₁ hl₂
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l₁
hl₂ : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R t) l₁
this : l₁ = 0
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M) (0 : M)

Tactic:
simp [this]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
rw : Membership.mem (γ := Submodule R M) (R ∙ v x) (v x)
⊢ Membership.mem (γ := Submodule R M) (span R (v '' {x})) (v x)

Tactic:
rw [Set.image_singleton]

Premises used: Set.image_singleton
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ Membership.mem (γ := Submodule R M) (R ∙ v x) (v x)

Tactic:
mem_span_singleton_self (v x)

Premises used: Submodule.mem_span_singleton_self
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ Membership.mem (γ := Submodule R M) (R ∙ v x) (v x)

Tactic:
exact mem_span_singleton_self (v x)

Premises used: Submodule.mem_span_singleton_self
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ Membership.mem (γ := Submodule R M) (span R (v '' {x})) (v x)

Tactic:
have h' : v x ∈ Submodule.span R (v '' {x}) := by
    rw [Set.image_singleton]
    exact mem_span_singleton_self (v x)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : Membership.mem (γ := Submodule R M) (span R (v '' {x})) (v x)
w : Membership.mem (γ := Submodule R M) (span R (v '' s)) (v x)
apply : v x = 0
⊢ False

Tactic:
apply LinearIndependent.ne_zero x hv

Premises used: LinearIndependent.ne_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : Membership.mem (γ := Submodule R M) (span R (v '' {x})) (v x)
w : Membership.mem (γ := Submodule R M) (span R (v '' s)) (v x)
⊢ v x = 0

Tactic:
disjoint_def.1 (hv.disjoint_span_image ?_) (v x) h' w

Premises used: LinearIndependent.disjoint_span_image, Iff.mp, Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : Membership.mem (γ := Submodule R M) (span R (v '' {x})) (v x)
w : Membership.mem (γ := Submodule R M) (span R (v '' s)) (v x)
refine : Disjoint {x} s
⊢ v x = 0

Tactic:
refine disjoint_def.1 (hv.disjoint_span_image ?_) (v x) h' w

Premises used: LinearIndependent.disjoint_span_image, Iff.mp, Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : Membership.mem (γ := Submodule R M) (span R (v '' {x})) (v x)
w : Membership.mem (γ := Submodule R M) (span R (v '' s)) (v x)
⊢ Disjoint {x} s

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
x : ι
f : ι →₀ R
h : x ∉ f.support
⊢ x ∉ (↑f.support : Set ι)

Tactic:
replace h : x ∉ (f.support : Set ι) := h
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
x : ι
f : ι →₀ R
h : x ∉ (↑f.support : Set ι)
w : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) f = v x
⊢ ∀ (x : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (↑f.support : Set ι)) x →
      Ne.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) x : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)

Tactic:
simpa [← w, Finsupp.span_image_eq_map_linearCombination] using hv.notMem_span_image h

Premises used: Finsupp.span_image_eq_map_linearCombination, LinearIndependent.notMem_span_image
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
x : ι
f : ι →₀ R
h : x ∉ (↑f.support : Set ι)
w : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) f = v x
⊢ ∀ (x : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (↑f.support : Set ι)) x →
      Ne.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) x : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)

Tactic:
have p : ∀ x ∈ Finsupp.supported R R f.support,
    Finsupp.linearCombination R v x ≠ f.linearCombination R v := by
    simpa [← w, Finsupp.span_image_eq_map_linearCombination] using hv.notMem_span_image h
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
x : ι
f : ι →₀ R
h : x ∉ (↑f.support : Set ι)
w : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) f = v x
p :
  ∀ (x : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (↑f.support : Set ι)) x →
      Ne.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) x : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
⊢ False

Tactic:
p f (f.mem_supported_support R) rfl

Premises used: Finsupp.mem_supported_support, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
x : ι
f : ι →₀ R
h : x ∉ (↑f.support : Set ι)
w : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) f = v x
p :
  ∀ (x : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (↑f.support : Set ι)) x →
      Ne.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) x : M)
        ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
⊢ False

Tactic:
exact p f (f.mem_supported_support R) rfl

Premises used: Finsupp.mem_supported_support, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
f : M →ₗ[R] M'
hs : LinearIndepOn R id s
hf_inj : InjOn.{u_4, u_5} (β := M') (⇑f : (a : M) → M') (↑(span R s) : Set M)
⊢ InjOn.{u_4, u_5} (β := M') (⇑f : (a : M) → M') (↑(span R (id '' s)) : Set M)

Tactic:
simpa using hf_inj
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
dsimp :
  (Finsupp.linearCombination R v : (a : ι →₀ R) → M)
      (Finsupp.mapDomain (⇑f : (a : ι') → ι)
        (repr
          (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
            (v i) ⋯))) =
    v i
⊢ (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i

Tactic:
dsimp only [l]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
rw :
  (Finsupp.linearCombination R (v ∘ (⇑f : (a : ι') → ι)) : (a : ι' →₀ R) → M)
      (repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯)) =
    v i
⊢ (Finsupp.linearCombination R v : (a : ι →₀ R) → M)
      (Finsupp.mapDomain (⇑f : (a : ι') → ι)
        (repr
          (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
            (v i) ⋯))) =
    v i

Tactic:
rw [Finsupp.linearCombination_mapDomain]

Premises used: Finsupp.linearCombination_mapDomain
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
rw rw₁ :
  (↑(Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯) :
      M) =
    v i
⊢ (Finsupp.linearCombination R (v ∘ (⇑f : (a : ι') → ι)) : (a : ι' →₀ R) → M)
      (repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯)) =
    v i

Tactic:
rw [(hv.comp f f.injective).linearCombination_repr]

Premises used: LinearIndependent.linearCombination_repr, Function.Embedding.injective, DFunLike.coe, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
⊢ (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i

Tactic:
have h_total_l : Finsupp.linearCombination R v l = v i := by
    dsimp only [l]
    rw [Finsupp.linearCombination_mapDomain]
    rw [(hv.comp f f.injective).linearCombination_repr]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
h_total_l : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i
rw : v i = (Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1)
rw₁ : v i = HSMul.hSMul.{u_2, u_4, u_4} (α := R) 1 (v i)
rw₂ rw₃ : v i = v i
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) : M)

Tactic:
rw [h_total_l, Finsupp.linearCombination_single, one_smul]

Premises used: Finsupp.linearCombination_single, one_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
h_total_l : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) : M)

Tactic:
have h_total_eq : Finsupp.linearCombination R v l = Finsupp.linearCombination R v
       (Finsupp.single i 1) := by
    rw [h_total_l, Finsupp.linearCombination_single, one_smul]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
h_total_l : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i
h_total_eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) : M)
⊢ l = Finsupp.single i 1

Tactic:
have l_eq : l = _ := hv h_total_eq
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
h_total_l : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i
h_total_eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) : M)
l_eq :
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
      (repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯)) =
    Finsupp.single i 1
⊢ Finsupp.embDomain f
      (repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯)) =
    Finsupp.single i 1

Tactic:
rw [← Finsupp.embDomain_eq_mapDomain] at l_eq

Premises used: Finsupp.embDomain_eq_mapDomain
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
h_total_l : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i
h_total_eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) : M)
l_eq :
  Finsupp.embDomain f
      (repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯)) =
    Finsupp.single i 1
rcases :
  ∀ (i' : ι')
    (hi' :
      repr
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
              (v i) ⋯) =
          Finsupp.single i' 1 ∧
        (f : (a : ι') → ι) i' = i),
    ∃ (a : ι'), (f : (a : ι') → ι) a = i
⊢ ∃ (a : ι'), (f : (a : ι') → ι) a = i

Tactic:
rcases Finsupp.single_of_embDomain_single (repr ⟨v i, _⟩) f i (1 : R) zero_ne_one.symm l_eq with
    ⟨i', hi'⟩

Premises used: zero_ne_one, Ne.symm, Subtype.mk, Finsupp.single_of_embDomain_single, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ (↑(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) : Set M)
i : ι
repr : ↥(span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) → ι' →₀ R :=
  (⇑⋯.repr : (a : ↥(span R (range (v ∘ (⇑f : (a : ι') → ι))))) → ι' →₀ R)
l : ι →₀ R :=
  Finsupp.mapDomain (⇑f : (a : ι') → ι)
    (repr
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x) (v i)
        ⋯))
h_total_l : (Finsupp.linearCombination R v : (a : ι →₀ R) → M) l = v i
h_total_eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1) : M)
l_eq :
  Finsupp.embDomain f
      (repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯)) =
    Finsupp.single i 1
i' : ι'
hi' :
  repr
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule R M) (span R (range.{u_4, u_1 + 1} (ι := ι') (v ∘ (⇑f : (a : ι') → ι)))) x)
          (v i) ⋯) =
      Finsupp.single i' 1 ∧
    (f : (a : ι') → ι) i' = i
h : (f : (a : ι') → ι) i' = i
⊢ ∃ (a : ι'), (f : (a : ι') → ι) a = i

Tactic:
use i'