awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
hs : LinearIndepOn K id s
rw :
  range (ι := (↑(hs.extend (s := s) (t := univ) ⋯) : Type u_4))
      (Subtype.val (p := fun (x : V) ↦ x ∈ hs.extend (s := s) (t := univ) ⋯)) =
    hs.extend (s := s) (t := univ) ⋯
⊢ range (ι := (↑(hs.extend (s := s) (t := univ) ⋯) : Type u_4))
      (⇑(extend (s := s) hs) : (a : (↑(hs.extend ⋯) : Type u_4)) → V) =
    hs.extend (s := s) (t := univ) ⋯
have rw₁ : {x : V | x ∈ hs.extend (s := s) (t := univ) sorry} = hs.extend (s := s) (t := univ) sorry
Tactic: rw [coe_extend, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
hs : LinearIndepOn K id s
rw :
  range (ι := (↑(hs.extend (s := s) (t := univ) ⋯) : Type u_4))
      (Subtype.val (p := fun (x : V) ↦ x ∈ hs.extend (s := s) (t := univ) ⋯)) =
    hs.extend (s := s) (t := univ) ⋯
rw₁ : {x : V | x ∈ hs.extend (s := s) (t := univ) ⋯} = hs.extend (s := s) (t := univ) ⋯
⊢ range (ι := (↑(hs.extend (s := s) (t := univ) ⋯) : Type u_4))
      (⇑(extend (s := s) hs) : (a : (↑(hs.extend ⋯) : Type u_4)) → V) =
    hs.extend (s := s) (t := univ) ⋯
have rw₂ : hs.extend (s := s) (t := univ) sorry = hs.extend (s := s) (t := univ) sorry
Tactic: rw [coe_extend, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : LE.le (α := Submodule K V) ⊤ (span K t)
⊢ range (ι := (↑(hs.extend (s := s) (t := t) hst) : Type u_4))
      (⇑(extendLe (s := s) (t := t) hs hst ht) : (a : (↑(hs.extend hst) : Type u_4)) → V) =
    hs.extend (s := s) (t := t) hst
have rw : range (ι := (↑(hs.extend (s := s) (t := t) hst) : Type u_4))
    (Subtype.val (p := fun (x : V) ↦ x ∈ hs.extend (s := s) (t := t) hst)) =
  hs.extend (s := s) (t := t) hst
Tactic: rw [coe_extendLe, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : LE.le (α := Submodule K V) ⊤ (span K t)
rw :
  range (ι := (↑(hs.extend (s := s) (t := t) hst) : Type u_4))
      (Subtype.val (p := fun (x : V) ↦ x ∈ hs.extend (s := s) (t := t) hst)) =
    hs.extend (s := s) (t := t) hst
⊢ range (ι := (↑(hs.extend (s := s) (t := t) hst) : Type u_4))
      (⇑(extendLe (s := s) (t := t) hs hst ht) : (a : (↑(hs.extend hst) : Type u_4)) → V) =
    hs.extend (s := s) (t := t) hst
have rw₁ : {x : V | x ∈ hs.extend (s := s) (t := t) hst} = hs.extend (s := s) (t := t) hst
Tactic: rw [coe_extendLe, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : LE.le (α := Submodule K V) ⊤ (span K t)
rw :
  range (ι := (↑(hs.extend (s := s) (t := t) hst) : Type u_4))
      (Subtype.val (p := fun (x : V) ↦ x ∈ hs.extend (s := s) (t := t) hst)) =
    hs.extend (s := s) (t := t) hst
rw₁ : {x : V | x ∈ hs.extend (s := s) (t := t) hst} = hs.extend (s := s) (t := t) hst
⊢ range (ι := (↑(hs.extend (s := s) (t := t) hst) : Type u_4))
      (⇑(extendLe (s := s) (t := t) hs hst ht) : (a : (↑(hs.extend hst) : Type u_4)) → V) =
    hs.extend (s := s) (t := t) hst
have rw₂ : hs.extend (s := s) (t := t) hst = hs.extend (s := s) (t := t) hst
Tactic: rw [coe_extendLe, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
hs : LE.le (α := Submodule K V) ⊤ (span K s)
⊢ range (ι := (↑(LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯) : Type u_4))
      (⇑(ofSpan (s := s) hs) : (a : (↑(⋯.extend ⋯) : Type u_4)) → V) =
    LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯
have rw : range (ι := (↑(LinearIndepOn.extend (v := id) (s := ∅) (t := s) sorry sorry) : Type u_4))
    (Subtype.val (p := fun (x : V) ↦ x ∈ LinearIndepOn.extend (v := id) (s := ∅) (t := s) sorry sorry)) =
  LinearIndepOn.extend (v := id) (s := ∅) (t := s) sorry sorry
Tactic: rw [coe_ofSpan, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
hs : LE.le (α := Submodule K V) ⊤ (span K s)
rw :
  range (ι := (↑(LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯) : Type u_4))
      (Subtype.val (p := fun (x : V) ↦ x ∈ LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯)) =
    LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯
⊢ range (ι := (↑(LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯) : Type u_4))
      (⇑(ofSpan (s := s) hs) : (a : (↑(⋯.extend ⋯) : Type u_4)) → V) =
    LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯
have rw₁ : {x : V | x ∈ LinearIndepOn.extend (v := id) (s := ∅) (t := s) sorry sorry} =
  LinearIndepOn.extend (v := id) (s := ∅) (t := s) sorry sorry
Tactic: rw [coe_ofSpan, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
hs : LE.le (α := Submodule K V) ⊤ (span K s)
rw :
  range (ι := (↑(LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯) : Type u_4))
      (Subtype.val (p := fun (x : V) ↦ x ∈ LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯)) =
    LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯
rw₁ :
  {x : V | x ∈ LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯} =
    LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯
⊢ range (ι := (↑(LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯) : Type u_4))
      (⇑(ofSpan (s := s) hs) : (a : (↑(⋯.extend ⋯) : Type u_4)) → V) =
    LinearIndepOn.extend (v := id) (s := ∅) (t := s) ⋯ ⋯
have rw₂ : LinearIndepOn.extend (v := id) (s := ∅) (t := s) sorry sorry = LinearIndepOn.extend (v := id) (s := ∅) (t := s) sorry sorry
Tactic: rw [coe_ofSpan, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x : (↑(ofVectorSpaceIndex K V) : Type u_4)
⊢ (ofVectorSpace K V : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V) x = (↑x : V)
have unfold : (extend (s := ∅) sorry : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V) x = (↑x : V)
Tactic: unfold ofVectorSpace
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ LinearIndependent.{u_4, u_3, u_4} (ι := { x : V // x ∈ ofVectorSpaceIndex K V }) K
    (Subtype.val (p := fun (x : V) ↦ x ∈ ofVectorSpaceIndex K V))
have h : Eq.{u_4 + 1} (α := { x : V // x ∈ ofVectorSpaceIndex K V } → V)
  (Subtype.val (p := fun (x : V) ↦ x ∈ ofVectorSpaceIndex K V))
  (⇑(ofVectorSpace K V) : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V)
Tactic: convert! (ofVectorSpace K V).linearIndependent
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Eq.{u_4 + 1} (α := { x : V // x ∈ ofVectorSpaceIndex K V } → V)
    (Subtype.val (p := fun (x : V) ↦ x ∈ ofVectorSpaceIndex K V))
    (⇑(ofVectorSpace K V) : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V)
have h : ∀ (x : { x : V // x ∈ ofVectorSpaceIndex K V }),
  (↑x : V) = (ofVectorSpace K V : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
x : { x : V // x ∈ ofVectorSpaceIndex K V }
⊢ (↑x : V) = (ofVectorSpace K V : (a : (↑(ofVectorSpaceIndex K V) : Type u_4)) → V) x
have h : (↑x : V) = (↑x : V)
Tactic: rw [ofVectorSpace_apply_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ IsAtom (α := Submodule K V) (K ∙ v)
have left : Ne (α := Submodule K V) (K ∙ v) ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
left : Ne (α := Submodule K V) (K ∙ v) ⊥
⊢ IsAtom (α := Submodule K V) (K ∙ v)
have right : ∀ b < K ∙ v, b = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
⊢ Ne (α := Submodule K V) (K ∙ v) ⊥
have left : ∃ (x : V), Membership.mem (γ := Submodule K V) (K ∙ v) x ∧ x ≠ 0
Tactic: rw [Submodule.ne_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
⊢ T = ⊥
have right : ∀ (h : ¬T = ⊥), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
h : ¬T = ⊥
⊢ False
have right : (↑(K ∙ v) : Set V) ⊆ (↑T : Set V)
Tactic: apply hT.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
h : ¬T = ⊥
⊢ K ∙ v ≤ T
have right : ∀ (h : ∃ x ∈ T, x ≠ 0), v ∈ T
Tactic: simp_rw [span_singleton_le_iff_mem, ← Ne.eq_def, Submodule.ne_bot_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
h : ∃ x ∈ T, x ≠ 0
⊢ v ∈ T
have right : ∀ (s : V) (hs : s ∈ T) (hz : s ≠ 0), v ∈ T
Tactic: rcases h with ⟨s, ⟨hs, hz⟩⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
s : V
hs : s ∈ T
hz : s ≠ 0
⊢ v ∈ T
have right : ∀ (a : K) (hs : a • v ∈ T) (hz : a • v ≠ 0), v ∈ T
Tactic: rcases mem_span_singleton.1 (hT.1 hs) with ⟨a, rfl⟩
Cleared hypotheses: s, hs, hz
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
⊢ v ∈ T
have right : ∀ (hs : HSMul.hSMul.{u_3, u_4, u_4} (α := K) 0 v ∈ T) (hz : HSMul.hSMul.{u_3, u_4, u_4} (α := K) 0 v ≠ 0), v ∈ T
Tactic: rcases eq_or_ne a 0 with rfl | h
Cleared hypotheses: a, hs, hz
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
right : ∀ (hs : HSMul.hSMul.{u_3, u_4, u_4} (α := K) 0 v ∈ T) (hz : HSMul.hSMul.{u_3, u_4, u_4} (α := K) 0 v ≠ 0), v ∈ T
⊢ v ∈ T
have right₁ : ∀ (h : a ≠ 0), v ∈ T
Tactic: rcases eq_or_ne a 0 with rfl | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
h : a ≠ 0
⊢ v ∈ T
have right : ∀ (hs : v ∈ T) (hz : a • v ≠ 0) (h : a ≠ 0), v ∈ T
Tactic: rwa [T.smul_mem_iff h] at hs
Cleared hypotheses: hs, hz, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
⊢ IsAtom W ↔ ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
have refine_1 : ∀ (h : IsAtom W), ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
refine_1 : ∀ (h : IsAtom W), ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
⊢ IsAtom W ↔ ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
have refine_2 : ∀ (h : ∃ (v : V), v ≠ 0 ∧ W = K ∙ v), IsAtom W
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
h : IsAtom W
⊢ ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
have hbot : W ≠ ⊥
Tactic: obtain ⟨hbot, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
h : IsAtom W
hbot : W ≠ ⊥
⊢ ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
have h₁ : ∀ b < W, b = ⊥
Tactic: obtain ⟨hbot, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
⊢ ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
have refine_1 : ∀ (v : V) (hW : v ∈ W) (hv : v ≠ 0), ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
Tactic: rcases (Submodule.ne_bot_iff W).1 hbot with ⟨v, ⟨hW, hv⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
have refine_1 : W = K ∙ v
Tactic: refine ⟨v, ⟨hv, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ W = K ∙ v
have refine_1 : ∀ (heq : ¬W = K ∙ v), False
Tactic: by_contra heq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
⊢ False
have h₁ : K ∙ v < W → Eq (α := Submodule K V) (K ∙ v) ⊥
Tactic: specialize h (span K {v})
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
h : K ∙ v < W → Eq (α := Submodule K V) (K ∙ v) ⊥
⊢ False
have h₁ : K ∙ v ≤ W ∧ K ∙ v ≠ W → v = 0
Tactic: rw [span_singleton_eq_bot, lt_iff_le_and_ne] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K V
h : ∃ (v : V), v ≠ 0 ∧ W = K ∙ v
⊢ IsAtom W
have refine_2 : ∀ (v : V) (hv : v ≠ 0), IsAtom (α := Submodule K V) (K ∙ v)
Tactic: rcases h with ⟨v, ⟨hv, rfl⟩⟩
Cleared hypotheses: W, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
⊢ ∃ (s : Set (Submodule K V)), W = sSup s ∧ ∀ a ∈ s, IsAtom a
have refine : ∀ (a : Submodule K V),
  Membership.mem (γ := Set (Submodule K V)) {T : Submodule K V | ∃ m ∈ W, m ≠ 0 ∧ T = K ∙ m} a → IsAtom a
Tactic: refine ⟨_, submodule_eq_sSup_le_nonzero_spans W, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
⊢ ∃ (g : V' →ₗ[K] V), g ∘ₗ f = id
have hB₀ : LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
  (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
    (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
Tactic: have hB₀ : _ := hB.linearIndependent.linearIndepOn_id
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
⊢ LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
have h₁ : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id
  (image.{u_4, u_5} (α := V) (⇑f : (a : V) → V')
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑(Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V)))
Tactic: have h₁ : LinearIndepOn K _root_.id (f '' Set.range (Basis.ofVectorSpace K V)) :=
      LinearIndepOn.image (f := f) hB₀ (show Disjoint _ _ by simp [hf_inj])
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
h₁ :
  LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id
    (image.{u_4, u_5} (α := V) (⇑f : (a : V) → V')
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
        (⇑(Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V)))
⊢ LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
have rwa : ∀ (h₁ : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' Basis.ofVectorSpaceIndex K V)),
  LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
Tactic: rwa [Basis.range_ofVectorSpace K V] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
⊢ ∃ (g : V' →ₗ[K] V), g ∘ₗ f = id
have this : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
Tactic: have : LinearIndepOn K _root_.id (f '' B) := by
    have h₁ : LinearIndepOn K _root_.id (f '' Set.range (Basis.ofVectorSpace K V)) :=
      LinearIndepOn.image (f := f) hB₀ (show Disjoint _ _ by simp [hf_inj])
    rwa [Basis.range_ofVectorSpace K V] at h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
this : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
C : Set V' := this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
⊢ ∃ (g : V' →ₗ[K] V), g ∘ₗ f = id
have BC : (⇑f : (a : V) → V') '' B ⊆ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) sorry
Tactic: have BC := this.subset_extend (subset_univ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
this : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
C : Set V' := this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
BC : (⇑f : (a : V) → V') '' B ⊆ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
hC : Basis (↑(this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯) : Type u_5) K V' :=
  Basis.extend (s := (⇑f : (a : V) → V') '' B) this
⊢ ∃ (g : V' →ₗ[K] V), g ∘ₗ f = id
have haveI : ∀ (Vinh : Inhabited V), ∃ (g : V' →ₗ[K] V), g ∘ₗ f = id
Tactic: haveI Vinh : Inhabited V := ⟨0⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_3
V : Type u_4
V' : Type u_5
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V'
inst_3 : Module K V
inst_4 : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V) : Type u_4) K V := Basis.ofVectorSpace K V
hB₀ :
  LinearIndepOn.{u_4, u_3, u_4} (ι := V) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K V) : Type u_4))
      (⇑hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V))
this : LinearIndepOn.{u_5, u_3, u_5} (ι := V') K _root_.id ((⇑f : (a : V) → V') '' B)
C : Set V' := this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
BC : (⇑f : (a : V) → V') '' B ⊆ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯
hC : Basis (↑(this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯) : Type u_5) K V' :=
  Basis.extend (s := (⇑f : (a : V) → V') '' B) this
Vinh : Inhabited V
⊢ ∃ (g : V' →ₗ[K] V), g ∘ₗ f = id
have refine : ∀ (b : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)),
  Eq (α := V)
    (((hC.constr ℕ : (a : (↑(this.extend sorry) : Type u_5) → V) → V' →ₗ[K] V)
              (C.restrict (π := fun (a : V') ↦ V) (invFun (⇑f : (a : V) → V'))) ∘ₗ
            f :
          (a : V) → V)
        ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V) :
      V)
    ((id : (a : V) → V) ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V) : V)
Tactic: refine ⟨(hC.constr ℕ : _ → _) (C.restrict (invFun f)), hB.ext fun b => ?_⟩