awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : MulAction G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
w : ι → G
h : LinearIndependent R (w • v)
⊢ LinearIndependent R v
have h₁ : v = HSMul.hSMul (α := ι → G) (fun (i : ι) ↦ (w i)⁻¹) (w • v)
Tactic: convert! h.group_smul (fun i ↦ (w i)⁻¹)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
hv : LinearIndependent R v
w : ι → Rˣ
⊢ LinearIndependent R (w • v)
have rw : ∀
  (hv :
    ∀ (s : Finset ι) (f g : ι → R),
      (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i)
  (w : ι → Rˣ) (s : Finset ι) (f g : ι → R),
  (∀ i ∉ s, f i = g i) →
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • (w • v) i) (∑ i ∈ s, g i • (w • v) i) → ∀ (i : ι), f i = g i
Tactic: rw [linearIndependent_iff''ₛ] at hv ⊢
Cleared hypotheses: hv, w
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
⊢ g₁ i = g₂ i
have rw : g₁ i * (↑(w i) : R) = g₂ i * (↑(w i) : R)
Tactic: rw [← (w i).mul_left_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
⊢ g₁ i * (↑(w i) : R) = g₂ i * (↑(w i) : R)
have refine_1 : ∀ (i : ι) (hi : i ∉ s),
  Eq.{u_2 + 1} (α := R) ((fun (i : ι) ↦ g₁ i • (↑(w i) : R)) i) ((fun (i : ι) ↦ g₂ i • (↑(w i) : R)) i)
Tactic: refine hv s (fun i ↦ g₁ i • w i) (fun i ↦ g₂ i • w i) (fun i hi ↦ ?_) ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
refine_1 :
  ∀ (i : ι) (hi : i ∉ s),
    Eq.{u_2 + 1} (α := R) ((fun (i : ι) ↦ g₁ i • (↑(w i) : R)) i) ((fun (i : ι) ↦ g₂ i • (↑(w i) : R)) i)
⊢ g₁ i * (↑(w i) : R) = g₂ i * (↑(w i) : R)
have refine_2 : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ g₁ i • (↑(w i) : R)) i) (v i))
  (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ g₂ i • (↑(w i) : R)) i) (v i))
Tactic: refine hv s (fun i ↦ g₁ i • w i) (fun i ↦ g₂ i • w i) (fun i hi ↦ ?_) ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
w : ι → Rˣ
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v
have refine : ∀ (h : LinearIndependent R (w • v)), LinearIndependent R v
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.units_smul w⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
w : ι → Rˣ
h : LinearIndependent R (w • v)
⊢ LinearIndependent R v
have h₁ : v = HSMul.hSMul (α := ι → Rˣ) (fun (i : ι) ↦ (w i)⁻¹) (w • v)
Tactic: convert! h.units_smul (fun i ↦ (w i)⁻¹)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
ι : Type u'
R : Type u_2
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
⊢ i = j
have h_single_eq : Eq (α := ι →₀ R) (Finsupp.single i c) (Finsupp.single j d)
Tactic: have h_single_eq : Finsupp.single i c = Finsupp.single j d :=
    li <| by simpa [Finsupp.linearCombination_apply] using h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Eq (α := ι →₀ R) (Finsupp.single i c) (Finsupp.single j d)
⊢ i = j
have inl : ∀ (H : i = j), c = d → i = j
Tactic: rcases (Finsupp.single_eq_single_iff ..).mp h_single_eq with (⟨H, _⟩ | ⟨hc, _⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
inst : Semiring R
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Eq (α := ι →₀ R) (Finsupp.single i c) (Finsupp.single j d)
inl : ∀ (H : i = j), c = d → i = j
⊢ i = j
have inr : ∀ (hc : c = 0), d = 0 → i = j
Tactic: rcases (Finsupp.single_eq_single_iff ..).mp h_single_eq with (⟨H, _⟩ | ⟨hc, _⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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
⊢ Disjoint (α := Submodule R M) (span R (v '' s)) (span R (v '' t))
have 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
Tactic: simp only [disjoint_def, Finsupp.mem_span_image_iff_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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)
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M) (0 : M)
have H₁ : l₂ = l₁
Tactic: rw [hv.finsuppLinearCombination_injective.eq_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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₁
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M) (0 : M)
have hl₃ : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R t) l₁
Tactic: subst l₂
Cleared hypotheses: l₂, hl₂, H
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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₁
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l₁ : M) (0 : M)
have this : l₁ = 0
Tactic: have : l₁ = 0 := Submodule.disjoint_def.mp (Finsupp.disjoint_supported_supported hs) _ hl₁ hl₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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)
have rw : Membership.mem (γ := Submodule R M) (R ∙ v x) (v x)
Tactic: rw [Set.image_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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
⊢ v x ∉ span R (v '' s)
have h' : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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)
⊢ False
have apply : v x = 0
Tactic: apply LinearIndependent.ne_zero x hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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
have refine : Disjoint {x} s
Tactic: refine disjoint_def.1 (hv.disjoint_span_image ?_) (v x) h' w
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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
⊢ (Finsupp.linearCombination R v : (a : ι →₀ R) → M) f ≠ v x
have h₁ : x ∉ (↑f.support : Set ι)
Tactic: replace h : x ∉ (f.support : Set ι) := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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
⊢ False
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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)
      (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
have 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)
        sorry)) =
  v i
Tactic: rw [Finsupp.linearCombination_mapDomain]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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 ∘ (⇑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
have 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)
        sorry) :
    M) =
  v i
Tactic: rw [(hv.comp f f.injective).linearCombination_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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)
        ⋯))
⊢ ∃ (a : ι'), (f : (a : ι') → ι) a = i
have h_total_l : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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)
have rw : v i = (Finsupp.linearCombination R v : (a : ι →₀ R) → M) (Finsupp.single i 1)
Tactic: rw [h_total_l, Finsupp.linearCombination_single, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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)
⊢ 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)
have rw₁ : v i = HSMul.hSMul.{u_2, u_4, u_4} (α := R) 1 (v i)
Tactic: rw [h_total_l, Finsupp.linearCombination_single, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
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)
⊢ 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)
have rw₂ : v i = v i
Tactic: rw [h_total_l, Finsupp.linearCombination_single, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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
⊢ ∃ (a : ι'), (f : (a : ι') → ι) a = i
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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)
⊢ ∃ (a : ι'), (f : (a : ι') → ι) a = i
have l_eq : l = Finsupp.single i 1
Tactic: have l_eq : l = _ := hv h_total_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
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
⊢ ∃ (a : ι'), (f : (a : ι') → ι) a = i
have 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)
        sorry)) =
  Finsupp.single i 1
Tactic: rw [← Finsupp.embDomain_eq_mapDomain] at l_eq
Cleared hypotheses: l_eq