awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : Fin 2 → V
rw :
  LinearIndependent K (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f) ∧
      f 0 ∉ span K (range (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f)) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₁ :
  Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      f 0 ∉ span K (range (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f)) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
⊢ LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
have rw₂ : Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
    f 0 ∉ K ∙ Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ↔
  f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
Tactic: rw [linearIndependent_finSucc, linearIndependent_unique_iff, range_unique, mem_span_singleton,
    not_exists, show Fin.tail f default = f 1 by rw [← Fin.succ_zero_eq_one]; rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : Fin 2 → V
rw :
  LinearIndependent K (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f) ∧
      f 0 ∉ span K (range (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f)) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₁ :
  Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      f 0 ∉ span K (range (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f)) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₂ :
  Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      f 0 ∉ K ∙ Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
⊢ LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
have rw₃ : (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
    ¬∃ (a : K), a • Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default = f 0) ↔
  f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
Tactic: rw [linearIndependent_finSucc, linearIndependent_unique_iff, range_unique, mem_span_singleton,
    not_exists, show Fin.tail f default = f 1 by rw [← Fin.succ_zero_eq_one]; rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : Fin 2 → V
rw :
  LinearIndependent K (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f) ∧
      f 0 ∉ span K (range (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f)) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₁ :
  Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      f 0 ∉ span K (range (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f)) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₂ :
  Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      f 0 ∉ K ∙ Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₃ :
  (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      ¬∃ (a : K), a • Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default = f 0) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
⊢ LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
have rw₄ : (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
    ∀ (x : K), ¬x • Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default = f 0) ↔
  f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
Tactic: rw [linearIndependent_finSucc, linearIndependent_unique_iff, range_unique, mem_span_singleton,
    not_exists, show Fin.tail f default = f 1 by rw [← Fin.succ_zero_eq_one]; rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : Fin 2 → V
rw :
  LinearIndependent K (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f) ∧
      f 0 ∉ span K (range (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f)) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₁ :
  Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      f 0 ∉ span K (range (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f)) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₂ :
  Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      f 0 ∉ K ∙ Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₃ :
  (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      ¬∃ (a : K), a • Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default = f 0) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw₄ :
  (Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default ≠ 0 ∧
      ∀ (x : K), ¬x • Fin.tail (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ V) f default = f 0) ↔
    f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
⊢ LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
have rw₅ : (f 1 ≠ 0 ∧ ∀ (x : K), ¬x • f 1 = f 0) ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
Tactic: rw [linearIndependent_finSucc, linearIndependent_unique_iff, range_unique, mem_span_singleton,
    not_exists, show Fin.tail f default = f 1 by rw [← Fin.succ_zero_eq_one]; rfl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ ∃ (m : Set ι),
    s ⊆ m ∧ Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) m
have refine : ∀ c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b},
  IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c →
    c.Nonempty →
      ∃ (ub : Set ι), Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} ub ∧ ∀ s ∈ c, s ⊆ ub
Tactic: refine zorn_subset_nonempty { b | b ⊆ t ∧ LinearIndepOn K v b} ?_ _ ⟨hst, hs⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ ∀ c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b},
    IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c →
      c.Nonempty →
        ∃ (ub : Set ι), Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} ub ∧ ∀ s ∈ c, s ⊆ ub
have refine_1 : ∀ (c : Set (Set ι)) (hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b})
  (cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c) (_c0 : c.Nonempty), ⋃₀ c ⊆ t
Tactic: refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
refine_1 :
  ∀ (c : Set (Set ι)) (hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b})
    (cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c) (_c0 : c.Nonempty), ⋃₀ c ⊆ t
⊢ ∀ c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b},
    IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c →
      c.Nonempty →
        ∃ (ub : Set ι), Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} ub ∧ ∀ s ∈ c, s ⊆ ub
have refine_2 : ∀ (c : Set (Set ι)) (hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b})
  (cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c) (_c0 : c.Nonempty), LinearIndepOn K v (⋃₀ c)
Tactic: refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
refine_1 :
  ∀ (c : Set (Set ι)) (hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b})
    (cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c) (_c0 : c.Nonempty), ⋃₀ c ⊆ t
refine_2 :
  ∀ (c : Set (Set ι)) (hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b})
    (cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c) (_c0 : c.Nonempty), LinearIndepOn K v (⋃₀ c)
⊢ ∀ c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b},
    IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c →
      c.Nonempty →
        ∃ (ub : Set ι), Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} ub ∧ ∀ s ∈ c, s ⊆ ub
have refine_3 : ∀ (c : Set (Set ι)) (hc : c ⊆ {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b})
  (cc : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) c) (_c0 : c.Nonempty), ∀ x ∈ c, x ⊆ ⋃₀ c
Tactic: refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ ∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ (↑(span K (v '' b)) : Set V) ∧ LinearIndepOn K v b
have obtain : ∀ (b : Set ι) (sb : s ⊆ b)
  (h : Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) b),
  ∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ (↑(span K (v '' b)) : Set V) ∧ LinearIndepOn K v b
Tactic: obtain ⟨b, sb, h⟩ := by
    refine zorn_subset_nonempty { b | b ⊆ t ∧ LinearIndepOn K v b} ?_ _ ⟨hst, hs⟩
    · refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩
      · exact sUnion_subset fun x xc => (hc xc).1
      · exact linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2
      · exact subset_sUnion_of_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
b : Set ι
sb : s ⊆ b
h : Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) b
⊢ ∃ b ⊆ t, s ⊆ b ∧ v '' t ⊆ (↑(span K (v '' b)) : Set V) ∧ LinearIndepOn K v b
have refine : ∀ x ∈ v '' t,
  ∀ (x_2 : ι) (hx : x_2 ∈ t) (hvx : v x_2 = x) (hn : x ∉ (↑(span K (v '' b)) : Set V)), x ∈ (↑(span K (v '' b)) : Set V)
Tactic: refine ⟨b, h.prop.1, sb, fun _ ⟨x, hx, hvx⟩ => by_contra fun hn ↦ hn ?_, h.prop.2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
b : Set ι
sb : s ⊆ b
h : Maximal (fun (x : Set ι) ↦ Membership.mem (γ := Set (Set ι)) {b : Set ι | b ⊆ t ∧ LinearIndepOn K v b} x) b
x_1 : V
h_1 : x_1 ∈ v '' t
x : ι
hx : x ∈ t
hvx : v x = x_1
hn : x_1 ∉ (↑(span K (v '' b)) : Set V)
⊢ x_1 ∈ (↑(span K (v '' b)) : Set V)
have subst : v x ∈ v '' t → ∀ (hn : v x ∉ (↑(span K (v '' b)) : Set V)), v x ∈ (↑(span K (v '' b)) : Set V)
Tactic: subst hvx
Cleared hypotheses: x_1, h_1, hvx, hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ ∃ b ⊆ t, s ⊆ b ∧ t ⊆ (↑(span K b) : Set V) ∧ LinearIndepOn K id b
have h : ∀ (x : Set V), t = id '' t
Tactic: convert! exists_linearIndepOn_extension hs hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
h : ∀ (x : Set V), t = id '' t
⊢ ∃ b ⊆ t, s ⊆ b ∧ t ⊆ (↑(span K b) : Set V) ∧ LinearIndepOn K id b
have h₁ : ∀ (x : Set V), x = id '' x
Tactic: convert! exists_linearIndepOn_extension hs hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
t : Set V
⊢ ∃ b ⊆ t,
    Eq (α := Submodule K V) (span K b) (span K t) ∧
      LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ b }) K (Subtype.val (p := fun (x : V) ↦ x ∈ b))
have obtain : ∀ (b : Set V) (hb₁ : b ⊆ t) (hb₂ : t ⊆ (↑(span K b) : Set V)) (hb₃ : LinearIndepOn K id b),
  ∃ b ⊆ t,
    Eq (α := Submodule K V) (span K b) (span K t) ∧
      LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ b }) K (Subtype.val (p := fun (x : V) ↦ x ∈ b))
Tactic: obtain ⟨b, hb₁, -, hb₂, hb₃⟩ :=
    exists_linearIndepOn_id_extension (linearIndependent_empty K V) (Set.empty_subset t)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
⊢ ∃ (κ : Type u') (a : κ → ι),
    Injective a ∧ Eq (α := Submodule K V) (span K (range (v ∘ a))) (span K (range v)) ∧ LinearIndependent K (v ∘ a)
have obtain : ∀ (t : Set V) (ht : t ⊆ range v) (hsp : Eq (α := Submodule K V) (span K t) (span K (range v)))
  (hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))),
  ∃ (κ : Type u') (a : κ → ι),
    Injective a ∧ Eq (α := Submodule K V) (span K (range (v ∘ a))) (span K (range v)) ∧ LinearIndependent K (v ∘ a)
Tactic: obtain ⟨t, ht, hsp, hli⟩ := exists_linearIndependent K (Set.range v)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
ht : t ⊆ range v
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
⊢ ∃ (κ : Type u') (a : κ → ι),
    Injective a ∧ Eq (α := Submodule K V) (span K (range (v ∘ a))) (span K (range v)) ∧ LinearIndependent K (v ∘ a)
have choose : ∀ (f : ⦃a : V⦄ → a ∈ t → ι) (hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a),
  ∃ (κ : Type u') (a : κ → ι),
    Injective a ∧ Eq (α := Submodule K V) (span K (range (v ∘ a))) (span K (range v)) ∧ LinearIndependent K (v ∘ a)
Tactic: choose f hf using ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
i : ι
hi : i ∈ s
⊢ v i ∈ t
have obtain : ∀ (a : (↑t : Type u)), v ((fun (a : (↑t : Type u)) ↦ f sorry) a) ∈ t
Tactic: obtain ⟨a, rfl⟩ := hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
⊢ ∃ (κ : Type u') (a : κ → ι),
    Injective a ∧ Eq (α := Submodule K V) (span K (range (v ∘ a))) (span K (range v)) ∧ LinearIndependent K (v ∘ a)
have hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
Tactic: have hs {i : ι} (hi : i ∈ s) : v i ∈ t := by obtain ⟨a, rfl⟩ := hi; simp [hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
⊢ Eq (α := Submodule K V) (span K (range (ι := (↑s : Type u')) (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)))) (span K t)
have e_s : range (ι := (↑s : Type u')) (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) = t
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
⊢ ∃ (κ : Type u') (a : κ → ι),
    Injective a ∧ Eq (α := Submodule K V) (span K (range (v ∘ a))) (span K (range v)) ∧ LinearIndependent K (v ∘ a)
have refine : LinearIndependent (ι := (↑s : Type u')) K (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
Tactic: refine ⟨s, Subtype.val, Subtype.val_injective, hsp.symm ▸ by congr; aesop, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
⊢ Subtype.val (p := fun (x : V) ↦ x ∈ t) ∘ f' = v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)
have h : ∀ (x : (↑s : Type u')), (Subtype.val (p := fun (x : V) ↦ x ∈ t) ∘ f') x = (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
⊢ LinearIndependent (ι := (↑s : Type u')) K (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
have rw : LinearIndependent K (Subtype.val (p := fun (x : V) ↦ x ∈ t) ∘ f')
Tactic: rw [← show Subtype.val ∘ f' = v ∘ Subtype.val by ext; simp [f']]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
⊢ LinearIndependent K (Subtype.val (p := fun (x : V) ↦ x ∈ t) ∘ f')
have hf₁ : Injective f'
Tactic: apply hli.comp
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : ι → V
t : Set V
hsp : Eq (α := Submodule K V) (span K t) (span K (range v))
hli : LinearIndependent.{u, u_3, u} (ι := { x : V // x ∈ t }) K (Subtype.val (p := fun (x : V) ↦ x ∈ t))
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun (a : (↑t : Type u)) ↦ f ⋯
hs : ∀ {i : ι} (hi : i ∈ s), v i ∈ t
f' : (a : (↑s : Type u')) → (↑t : Type u) :=
  fun (a : (↑s : Type u')) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ t) (v (↑a : ι)) ⋯
x y : (↑t : Type u)
hij :
  f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) ((fun (a : (↑t : Type u)) ↦ f ⋯) x) ⋯) =
    f' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) ((fun (a : (↑t : Type u)) ↦ f ⋯) y) ⋯)
⊢ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) ((fun (a : (↑t : Type u)) ↦ f ⋯) x) ⋯ =
    Subtype.mk (p := fun (x : ι) ↦ x ∈ s) ((fun (a : (↑t : Type u)) ↦ f ⋯) y) ⋯
have hij₁ : (↑x : V) = (↑y : V)
Tactic: simp only [Subtype.ext_iff, hf, f'] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ t ⊆ (↑(span K (hs.extend (s := s) (t := t) hst)) : Set V)
have h : t = id '' t
Tactic: convert! hs.image_subset_span_image_extend hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
h : t = id '' t
⊢ t ⊆ (↑(span K (hs.extend (s := s) (t := t) hst)) : Set V)
have h₁ : hs.extend (s := s) (t := t) hst = id '' hs.extend (s := s) (t := t) hst
Tactic: convert! hs.image_subset_span_image_extend hst
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
h : b₁ ∈ s
⊢ False
have this : b₁ ∈ s ∩ (↑(insert b₁ t) : Set V)
Tactic: have : b₁ ∈ s ∩ ↑(insert b₁ t) := ⟨h, Finset.mem_insert_self _ _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    (↑s' : Set V) ⊆ s →
      s ∩ (↑t : Set V) = ∅ →
        s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
          ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
h : b₁ ∈ s
this : b₁ ∈ s ∩ (↑(insert b₁ t) : Set V)
⊢ False
have rwa : ∀ (this : Membership.mem (γ := Set V) ∅ b₁), False
Tactic: rwa [hst] at this
Cleared hypotheses: this