awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hfv : LinearIndependent.{u', u_2, u_5} R (M := M') ((⇑f : (a : M) → M') ∘ v)
⊢ LinearIndependent R v
have hfv₁ : Injective (α := ι →₀ R) (β := M')
  (Function.comp (β := M) (⇑f : (a : M) → M') (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M))
Tactic: rw [LinearIndependent, Finsupp.linearCombination_linear_comp, LinearMap.coe_comp] at hfv
Cleared hypotheses: hfv
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn.{u_4, u_5} (β := M') (⇑f : (a : M) → M') (↑(span R (Set.range v)) : Set M)
⊢ LinearIndependent.{u', u_2, u_5} R (M := M') ((⇑f : (a : M) → M') ∘ v) ↔ LinearIndependent R v
have simp_rw : Injective (α := ι →₀ R) (β := M')
    (Function.comp (β := M) (⇑f : (a : M) → M') (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M)) ↔
  Injective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M)
Tactic: simp_rw [LinearIndependent, Finsupp.linearCombination_linear_comp, coe_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn.{u_4, u_5} (β := M') (⇑f : (a : M) → M') (↑(span R (Set.range v)) : Set M)
⊢ Injective (α := ι →₀ R) (β := M')
      (Function.comp (β := M) (⇑f : (a : M) → M') (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M)) ↔
    Injective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M)
have rw : Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) ⊆ (↑(span R (Set.range v)) : Set M)
Tactic: rw [hf_inj.injective_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn.{u_4, u_5} (β := M') (⇑f : (a : M) → M') (↑(span R (Set.range v)) : Set M)
⊢ Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) ⊆ (↑(span R (Set.range v)) : Set M)
have rw : Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) ⊆
  (↑(range (Finsupp.linearCombination R v)) : Set M)
Tactic: rw [← Finsupp.range_linearCombination, LinearMap.coe_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn.{u_4, u_5} (β := M') (⇑f : (a : M) → M') (↑(span R (Set.range v)) : Set M)
rw :
  Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) ⊆
    (↑(range (Finsupp.linearCombination R v)) : Set M)
⊢ Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) ⊆ (↑(span R (Set.range v)) : Set M)
have rw₁ : Subset.{u_4} (α := Set M) (Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M))
  (Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M))
Tactic: rw [← Finsupp.range_linearCombination, LinearMap.coe_range]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ (∀ (l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R),
      Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
          (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι)) →
        l₁ = l₂) ↔
    ∀ (f : ι →₀ R),
      (∀ x ∈ f.support, x ∈ s) →
        ∀ (g : ι →₀ R),
          (∀ x ∈ g.support, x ∈ s) →
            Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
have refine : ∀
  (h :
    ∀ (f : ι →₀ R),
      (∀ x ∈ f.support, x ∈ s) →
        ∀ (g : ι →₀ R),
          (∀ x ∈ g.support, x ∈ s) →
            Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g)
  (l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R)
  (eq :
    Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
      (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))),
  l₁ = l₂
Tactic: refine ⟨fun h l₁ h₁ l₂ h₂ eq ↦ (Finsupp.subtypeDomain_eq_iff h₁ h₂).1 <| h _ _ <|
    (Finsupp.sum_subtypeDomain_index h₁).trans eq ▸ (Finsupp.sum_subtypeDomain_index h₂).symm,
    fun h l₁ l₂ eq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
⊢ l₁ = l₂
have refine_1 : ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₁).support, x ∈ s
Tactic: refine Finsupp.embDomain_injective (Embedding.subtype (· ∈ s)) <| h _ ?_ _ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
refine_1 : ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₁).support, x ∈ s
⊢ l₁ = l₂
have refine_2 : ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₂).support, x ∈ s
Tactic: refine Finsupp.embDomain_injective (Embedding.subtype (· ∈ s)) <| h _ ?_ _ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
refine_1 : ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₁).support, x ∈ s
refine_2 : ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₂).support, x ∈ s
⊢ l₁ = l₂
have refine_3 : Eq.{u_4 + 1} (α := M) ((Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₁).sum fun (i : ι) (a : R) ↦ a • v i)
  ((Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₂).sum fun (i : ι) (a : R) ↦ a • v i)
Tactic: refine Finsupp.embDomain_injective (Embedding.subtype (· ∈ s)) <| h _ ?_ _ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
⊢ Eq.{u_4 + 1} (α := M)
    ((Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₁).sum fun (i : ι) (a : R) ↦ a • v i)
    ((Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₂).sum fun (i : ι) (a : R) ↦ a • v i)
have refine_3 : Eq.{u_4 + 1} (α := M)
  (Finsupp.sum (Finsupp.mapDomain (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s) : (a : { x : ι // x ∈ s }) → ι) l₁)
    fun (i : ι) (a : R) ↦ a • v i)
  (Finsupp.sum (Finsupp.mapDomain (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s) : (a : { x : ι // x ∈ s }) → ι) l₂)
    fun (i : ι) (a : R) ↦ a • v i)
Tactic: simp_rw [Finsupp.embDomain_eq_mapDomain]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
⊢ Eq.{u_4 + 1} (α := M)
    (Finsupp.sum (Finsupp.mapDomain (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s) : (a : { x : ι // x ∈ s }) → ι) l₁)
      fun (i : ι) (a : R) ↦ a • v i)
    (Finsupp.sum (Finsupp.mapDomain (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s) : (a : { x : ι // x ∈ s }) → ι) l₂)
      fun (i : ι) (a : R) ↦ a • v i)
have refine_3 : ∀ (b : ι), HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v b) = 0
Tactic: rwa [Finsupp.sum_mapDomain_index, Finsupp.sum_mapDomain_index]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
refine_3 : ∀ (b : ι), HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v b) = 0
⊢ Eq.{u_4 + 1} (α := M)
    (Finsupp.sum (Finsupp.mapDomain (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s) : (a : { x : ι // x ∈ s }) → ι) l₁)
      fun (i : ι) (a : R) ↦ a • v i)
    (Finsupp.sum (Finsupp.mapDomain (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s) : (a : { x : ι // x ∈ s }) → ι) l₂)
      fun (i : ι) (a : R) ↦ a • v i)
have refine_3₁ : ∀ (b : ι) (m₁ m₂ : R), (m₁ + m₂) • v b = m₁ • v b + m₂ • v b
Tactic: rwa [Finsupp.sum_mapDomain_index, Finsupp.sum_mapDomain_index]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ LinearIndepOn R v s ↔
    Injective (α := ↥(Finsupp.supported R R s)) (β := ↥(span R (v '' s)))
      (⇑(Finsupp.linearCombinationOn ι M R v s) : (a : ↥(Finsupp.supported R R s)) → ↥(span R (v '' s)))
have rw : LinearIndependent R (s.restrict (π := fun (a : ι) ↦ M) v) ↔
  Injective (α := ↥(Finsupp.supported R R s)) (β := ↥(span R (v '' s)))
    (⇑(Finsupp.linearCombinationOn ι M R v s) : (a : ↥(Finsupp.supported R R s)) → ↥(span R (v '' s)))
Tactic: rw [← linearIndependent_restrict_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
⊢ (ι →₀ R) ≃ₗ[R] ↥(span R (range v))
have refine_1 : ∀ (c : ι →₀ R),
  Membership.mem (α := M) (γ := Submodule R M) (span R (range v))
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) c : M)
Tactic: refine LinearEquiv.ofBijective (LinearMap.codRestrict (span R (range v))
    (Finsupp.linearCombination R v) ?_) ⟨hv.codRestrict _, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
refine_1 :
  ∀ (c : ι →₀ R),
    Membership.mem (α := M) (γ := Submodule R M) (span R (range v))
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) c : M)
⊢ (ι →₀ R) ≃ₗ[R] ↥(span R (range v))
have refine_2 : Surjective (α := ι →₀ R) (β := ↥(span R (range v)))
  (⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) sorry) : (a : ι →₀ R) → ↥(span R (range v)))
Tactic: refine LinearEquiv.ofBijective (LinearMap.codRestrict (span R (range v))
    (Finsupp.linearCombination R v) ?_) ⟨hv.codRestrict _, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
⊢ ∀ (c : ι →₀ R),
    Membership.mem (α := M) (γ := Submodule R M) (span R (range v))
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) c : M)
have refine_1 : ∀ (c : ι →₀ R),
  Membership.mem (α := M) (γ := Submodule R M) (LinearMap.range (Finsupp.linearCombination R v))
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) c : M)
Tactic: simp_rw [← Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
⊢ Surjective (α := ι →₀ R) (β := ↥(span R (range v)))
    (⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) : (a : ι →₀ R) → ↥(span R (range v)))
have refine_2 : Eq (α := Submodule R ↥(span R (range v)))
  (LinearMap.range (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) sorry)) ⊤
Tactic: rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top,
    Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
refine_2 :
  Eq (α := Submodule R ↥(span R (range v)))
    (LinearMap.range (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯)) ⊤
⊢ Surjective (α := ι →₀ R) (β := ↥(span R (range v)))
    (⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) : (a : ι →₀ R) → ↥(span R (range v)))
have refine_2₁ : Eq (α := Submodule R ↥(span R (range v)))
  (map (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) sorry) ⊤) ⊤
Tactic: rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top,
    Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
refine_2 :
  Eq (α := Submodule R ↥(span R (range v)))
    (LinearMap.range (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯)) ⊤
refine_2₁ :
  Eq (α := Submodule R ↥(span R (range v)))
    (map (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) ⊤) ⊤
⊢ Surjective (α := ι →₀ R) (β := ↥(span R (range v)))
    (⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) : (a : ι →₀ R) → ↥(span R (range v)))
have refine_2₂ : Eq (α := Submodule R ↥(span R (range v)))
  (comap (Submodule.subtype (span R (range v))) (map (Finsupp.linearCombination R v) ⊤)) ⊤
Tactic: rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top,
    Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
refine_2 :
  Eq (α := Submodule R ↥(span R (range v)))
    (LinearMap.range (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯)) ⊤
refine_2₁ :
  Eq (α := Submodule R ↥(span R (range v)))
    (map (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) ⊤) ⊤
refine_2₂ :
  Eq (α := Submodule R ↥(span R (range v)))
    (comap (Submodule.subtype (span R (range v))) (map (Finsupp.linearCombination R v) ⊤)) ⊤
⊢ Surjective (α := ι →₀ R) (β := ↥(span R (range v)))
    (⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) : (a : ι →₀ R) → ↥(span R (range v)))
have refine_2₃ : LE.le (α := Submodule R M) (LinearMap.range (M := ↥(span R (range v))) (Submodule.subtype (span R (range v))))
  (map (Finsupp.linearCombination R v) ⊤)
Tactic: rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top,
    Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
refine_2 :
  Eq (α := Submodule R ↥(span R (range v)))
    (LinearMap.range (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯)) ⊤
refine_2₁ :
  Eq (α := Submodule R ↥(span R (range v)))
    (map (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) ⊤) ⊤
refine_2₂ :
  Eq (α := Submodule R ↥(span R (range v)))
    (comap (Submodule.subtype (span R (range v))) (map (Finsupp.linearCombination R v) ⊤)) ⊤
refine_2₃ :
  LE.le (α := Submodule R M) (LinearMap.range (M := ↥(span R (range v))) (Submodule.subtype (span R (range v))))
    (map (Finsupp.linearCombination R v) ⊤)
⊢ Surjective (α := ι →₀ R) (β := ↥(span R (range v)))
    (⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) : (a : ι →₀ R) → ↥(span R (range v)))
have refine_2₄ : LE.le (α := Submodule R M) (span R (range v)) (map (Finsupp.linearCombination R v) ⊤)
Tactic: rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top,
    Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
refine_2 :
  Eq (α := Submodule R ↥(span R (range v)))
    (LinearMap.range (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯)) ⊤
refine_2₁ :
  Eq (α := Submodule R ↥(span R (range v)))
    (map (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) ⊤) ⊤
refine_2₂ :
  Eq (α := Submodule R ↥(span R (range v)))
    (comap (Submodule.subtype (span R (range v))) (map (Finsupp.linearCombination R v) ⊤)) ⊤
refine_2₃ :
  LE.le (α := Submodule R M) (LinearMap.range (M := ↥(span R (range v))) (Submodule.subtype (span R (range v))))
    (map (Finsupp.linearCombination R v) ⊤)
refine_2₄ : LE.le (α := Submodule R M) (span R (range v)) (map (Finsupp.linearCombination R v) ⊤)
⊢ Surjective (α := ι →₀ R) (β := ↥(span R (range v)))
    (⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) : (a : ι →₀ R) → ↥(span R (range v)))
have refine_2₅ : LE.le (α := Submodule R M) (span R (range v)) (LinearMap.range (Finsupp.linearCombination R v))
Tactic: rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top,
    Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
refine_2 :
  Eq (α := Submodule R ↥(span R (range v)))
    (LinearMap.range (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯)) ⊤
refine_2₁ :
  Eq (α := Submodule R ↥(span R (range v)))
    (map (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) ⊤) ⊤
refine_2₂ :
  Eq (α := Submodule R ↥(span R (range v)))
    (comap (Submodule.subtype (span R (range v))) (map (Finsupp.linearCombination R v) ⊤)) ⊤
refine_2₃ :
  LE.le (α := Submodule R M) (LinearMap.range (M := ↥(span R (range v))) (Submodule.subtype (span R (range v))))
    (map (Finsupp.linearCombination R v) ⊤)
refine_2₄ : LE.le (α := Submodule R M) (span R (range v)) (map (Finsupp.linearCombination R v) ⊤)
refine_2₅ : LE.le (α := Submodule R M) (span R (range v)) (LinearMap.range (Finsupp.linearCombination R v))
⊢ Surjective (α := ι →₀ R) (β := ↥(span R (range v)))
    (⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) : (a : ι →₀ R) → ↥(span R (range v)))
have refine_2₆ : LE.le (α := Submodule R M) (span R (range v)) (span R (range v))
Tactic: rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top,
    Finsupp.range_linearCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
⊢ hv.repr.ker = ⊥
have rw : (↑hv.linearCombinationEquiv.symm : ↥(span R (range v)) →ₗ[R] ι →₀ R).ker = ⊥
Tactic: rw [LinearIndependent.repr, LinearEquiv.ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Defs (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
rw : (↑hv.linearCombinationEquiv.symm : ↥(span R (range v)) →ₗ[R] ι →₀ R).ker = ⊥
⊢ hv.repr.ker = ⊥
have rw₁ : Eq.{u_4 + 1} (α := Submodule R ↥(span R (range v))) ⊥ ⊥
Tactic: rw [LinearIndependent.repr, LinearEquiv.ker]