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
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
b : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)
⊢ Eq (α := V)
    (((hC.constr ℕ : (a : (↑(this.extend ⋯) : 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)
have rw : ∀ (BC : B ⊆ (⇑f : (a : V) → V') ⁻¹' this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) sorry),
  let hC := Basis.extend (s := (⇑f : (a : V) → V') '' B) this;
  ∀ (Vinh : Inhabited V) (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: rw [image_subset_iff] at BC
Cleared hypotheses: BC, hC, Vinh, b
-- 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) ⋯
BC : B ⊆ (⇑f : (a : V) → V') ⁻¹' 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
b : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)
⊢ Eq (α := V)
    (((hC.constr ℕ : (a : (↑(this.extend ⋯) : 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)
have fb_eq : Eq.{u_5 + 1} (α := V') ((f : (a : V) → V') (↑b : V) : V')
  ((hC : (a : (↑(this.extend sorry) : Type u_5)) → V')
      (Subtype.mk (p := fun (x : V') ↦ x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) sorry)
          ((f : (a : V) → V') (↑b : V)) sorry :
        { x : V' // x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) sorry }) :
    V')
Tactic: have fb_eq : f b = hC ⟨f b, BC b.2⟩ := by
    change f b = Basis.extend this _
    simp_rw [Basis.extend_apply_self]
-- 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 : B ⊆ (⇑f : (a : V) → V') ⁻¹' 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
b : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)
fb_eq :
  Eq.{u_5 + 1} (α := V') ((f : (a : V) → V') (↑b : V) : V')
    ((hC : (a : (↑(this.extend ⋯) : Type u_5)) → V')
        (Subtype.mk (p := fun (x : V') ↦ x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯)
            ((f : (a : V) → V') (↑b : V)) ⋯ :
          { x : V' // x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯ }) :
      V')
⊢ Eq (α := V)
    (((hC.constr ℕ : (a : (↑(this.extend ⋯) : 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)
have dsimp : Eq.{u_4 + 1} (α := 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'))) :
          V' →ₗ[K] V) :
        (a : V') → V)
      ((f : (a : V) → V') ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V) : V') :
    V)
  ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V)
Tactic: dsimp
-- 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 : B ⊆ (⇑f : (a : V) → V') ⁻¹' 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
b : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)
fb_eq :
  Eq.{u_5 + 1} (α := V') ((f : (a : V) → V') (↑b : V) : V')
    ((hC : (a : (↑(this.extend ⋯) : Type u_5)) → V')
        (Subtype.mk (p := fun (x : V') ↦ x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯)
            ((f : (a : V) → V') (↑b : V)) ⋯ :
          { x : V' // x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) ⋯ }) :
      V')
⊢ Eq.{u_4 + 1} (α := V)
    ((((hC.constr ℕ : (a : (↑(this.extend ⋯) : Type u_5) → V) → V' →ₗ[K] V)
              (C.restrict (π := fun (a : V') ↦ V) (invFun (⇑f : (a : V) → V'))) :
            V' →ₗ[K] V) :
          (a : V') → V)
        ((f : (a : V) → V') ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V) : V') :
      V)
    ((hB : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type u_4)) → V) b : V)
have rw : C.restrict (π := fun (a : V') ↦ V) (invFun (⇑f : (a : V) → V'))
    (Subtype.mk (p := fun (x : V') ↦ x ∈ this.extend (s := (⇑f : (a : V) → V') '' B) (t := univ) sorry)
      ((f : (a : V) → V') (↑b : V)) sorry) =
  (↑b : V)
Tactic: rw [Basis.ofVectorSpace_apply_self, fb_eq, hC.constr_basis]
-- 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'
p : Submodule K V
f : LinearMap.{u_3, u_3, u_4, u_5} (RingHom.id K) (↥p) V'
g : V →ₗ[K] ↥p
hg : g ∘ₗ p.subtype = id
⊢ (f ∘ₗ g) ∘ₗ p.subtype = f
have rw : f ∘ₗ g ∘ₗ p.subtype = f
Tactic: rw [LinearMap.comp_assoc, hg, f.comp_id]
-- 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'
p : Submodule K V
f : LinearMap.{u_3, u_3, u_4, u_5} (RingHom.id K) (↥p) V'
g : V →ₗ[K] ↥p
hg : g ∘ₗ p.subtype = id
rw : f ∘ₗ g ∘ₗ p.subtype = f
⊢ (f ∘ₗ g) ∘ₗ p.subtype = f
have rw₁ : f ∘ₗ id = f
Tactic: rw [LinearMap.comp_assoc, hg, f.comp_id]
-- 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'
p : Submodule K V
f : LinearMap.{u_3, u_3, u_4, u_5} (RingHom.id K) (↥p) V'
g : V →ₗ[K] ↥p
hg : g ∘ₗ p.subtype = id
rw : f ∘ₗ g ∘ₗ p.subtype = f
rw₁ : f ∘ₗ id = f
⊢ (f ∘ₗ g) ∘ₗ p.subtype = f
have rw₂ : f = f
Tactic: rw [LinearMap.comp_assoc, hg, f.comp_id]
-- 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'
p : Submodule K V
v : V
f : LinearMap.{u_3, u_3, u_4, u_5} (RingHom.id K) (↥p) V'
hv : v ∉ p
y : V'
⊢ ∃ (g : V →ₗ[K] V'), g ∘ₗ p.subtype = f ∧ (g : (a : V) → V') v = y
have rcases : ∀ (g : V →ₗ[K] V')
  (hg :
    g ∘ₗ ({ domain := p, toFun := f : V →ₗ.[K] V' }.supSpanSingleton v y hv).domain.subtype =
      ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun),
  ∃ (g : V →ₗ[K] V'), g ∘ₗ p.subtype = f ∧ (g : (a : V) → V') v = y
Tactic: rcases (LinearPMap.supSpanSingleton ⟨p, f⟩ v y hv).toFun.exists_extend with ⟨g, hg⟩
-- 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'
p : Submodule K V
v : V
f : LinearMap.{u_3, u_3, u_4, u_5} (RingHom.id K) (↥p) V'
hv : v ∉ p
y : V'
g : V →ₗ[K] V'
hg :
  g ∘ₗ ({ domain := p, toFun := f : V →ₗ.[K] V' }.supSpanSingleton v y hv).domain.subtype =
    ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun
⊢ ∃ (g : V →ₗ[K] V'), g ∘ₗ p.subtype = f ∧ (g : (a : V) → V') v = y
have refine_1 : g ∘ₗ p.subtype = f
Tactic: refine ⟨g, ?_, ?_⟩
-- 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'
p : Submodule K V
v : V
f : LinearMap.{u_3, u_3, u_4, u_5} (RingHom.id K) (↥p) V'
hv : v ∉ p
y : V'
g : V →ₗ[K] V'
hg :
  g ∘ₗ ({ domain := p, toFun := f : V →ₗ.[K] V' }.supSpanSingleton v y hv).domain.subtype =
    ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun
refine_1 : g ∘ₗ p.subtype = f
⊢ ∃ (g : V →ₗ[K] V'), g ∘ₗ p.subtype = f ∧ (g : (a : V) → V') v = y
have refine_2 : (g : (a : V) → V') v = y
Tactic: refine ⟨g, ?_, ?_⟩
-- 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'
p : Submodule K V
v : V
f : LinearMap.{u_3, u_3, u_4, u_5} (RingHom.id K) (↥p) V'
hv : v ∉ p
y : V'
g : V →ₗ[K] V'
hg :
  g ∘ₗ ({ domain := p, toFun := f : V →ₗ.[K] V' }.supSpanSingleton v y hv).domain.subtype =
    ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun
⊢ g ∘ₗ p.subtype = f
have refine_1 : ∀ (x : ↥p), Eq.{u_5 + 1} (α := V') ((g ∘ₗ p.subtype : (a : ↥p) → V') x : V') ((f : (a : ↥p) → V') x : V')
Tactic: ext x
-- 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'
p : Submodule K V
v : V
f : LinearMap.{u_3, u_3, u_4, u_5} (RingHom.id K) (↥p) V'
hv : v ∉ p
y : V'
g : V →ₗ[K] V'
hg :
  g ∘ₗ ({ domain := p, toFun := f : V →ₗ.[K] V' }.supSpanSingleton v y hv).domain.subtype =
    ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun
x : ↥p
⊢ Eq.{u_5 + 1} (α := V') ((g ∘ₗ p.subtype : (a : ↥p) → V') x : V') ((f : (a : ↥p) → V') x : V')
have this : (↑({ domain := p, toFun := f : V →ₗ.[K] V' }.supSpanSingleton v y hv) :
      ↥({ domain := p, toFun := f }.supSpanSingleton v y hv).domain → V')
    (Subtype.mk (p := fun (x : V) ↦ x ∈ ({ domain := p, toFun := f : V →ₗ.[K] V' }.supSpanSingleton v y hv).domain)
      (↑x : V) sorry) =
  (↑{ domain := p, toFun := f : V →ₗ.[K] V' } : ↥{ domain := p, toFun := f }.domain → V')
    (Subtype.mk (p := fun (x : V) ↦ x ∈ { domain := p, toFun := f : V →ₗ.[K] V' }.domain) (↑x : V) sorry)
Tactic: have := LinearPMap.supSpanSingleton_apply_mk_of_mem ⟨p, f⟩ y hv x.2
-- 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'
p : Submodule K V
v : V
f : LinearMap.{u_3, u_3, u_4, u_5} (RingHom.id K) (↥p) V'
hv : v ∉ p
y : V'
g : V →ₗ[K] V'
hg :
  g ∘ₗ ({ domain := p, toFun := f : V →ₗ.[K] V' }.supSpanSingleton v y hv).domain.subtype =
    ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun
⊢ (g : (a : V) → V') v = y
have this : (↑({ domain := p, toFun := f : V →ₗ.[K] V' }.supSpanSingleton v y hv) :
      ↥({ domain := p, toFun := f }.supSpanSingleton v y hv).domain → V')
    (Subtype.mk (p := fun (x : V) ↦ x ∈ ({ domain := p, toFun := f : V →ₗ.[K] V' }.supSpanSingleton v y hv).domain) v
      sorry) =
  y
Tactic: have := LinearPMap.supSpanSingleton_apply_self ⟨p, f⟩ y 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
p : Submodule K V
v : V
hv : v ∉ p
⊢ ∃ (f : V →ₗ[K] K), Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K) ∧ p ≤ f.ker
have rcases : ∀ (f : V →ₗ[K] K) (hpf : f ∘ₗ p.subtype = 0) (hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (1 : K)),
  ∃ (f : V →ₗ[K] K), Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K) ∧ p ≤ f.ker
Tactic: rcases LinearMap.exists_extend_of_notMem (0 : p →ₗ[K] K) hv 1 with ⟨f, hpf, hfv⟩
-- 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
p : Submodule K V
v : V
hv : v ∉ p
f : V →ₗ[K] K
hpf : f ∘ₗ p.subtype = 0
hfv : Eq.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (1 : K)
⊢ ∃ (f : V →ₗ[K] K), Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K) ∧ p ≤ f.ker
have refine : ∀ (x : V) (hx : x ∈ p), x ∈ f.ker
Tactic: refine ⟨f, by simp [hfv], fun x hx ↦ ?_⟩
-- 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
inst_5 : Nontrivial V
inst_6 : Nontrivial V'
⊢ Nontrivial (V →ₗ[K] V')
have obtain : ∀ (v : V) (hv : v ≠ 0), Nontrivial (V →ₗ[K] V')
Tactic: obtain ⟨v, hv⟩ := exists_ne (0 : V)
-- 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_1 : ι → V
s t : Set V
x y z : V
inst_5 : Nontrivial V
inst_6 : Nontrivial V'
v : V
hv : v ≠ 0
⊢ Nontrivial (V →ₗ[K] V')
have obtain : ∀ (w : V') (hw : w ≠ 0), Nontrivial (V →ₗ[K] V')
Tactic: obtain ⟨w, hw⟩ := exists_ne (0 : V')
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
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_1 : ι → V
s t : Set V
x y z : V
inst_5 : Nontrivial V
inst_6 : Nontrivial V'
v : V
hv : v ≠ 0
w : V'
hw : w ≠ 0
⊢ Nontrivial (V →ₗ[K] V')
have this : v ∉ ⊥
Tactic: have : v ∉ (⊥ : Submodule K V) := by simp only [mem_bot, hv, not_false_eq_true]
-- 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_1 : ι → V
s t : Set V
x y z : V
inst_5 : Nontrivial V
inst_6 : Nontrivial V'
v : V
hv : v ≠ 0
w : V'
hw : w ≠ 0
this : v ∉ ⊥
⊢ Nontrivial (V →ₗ[K] V')
have obtain : ∀ (g : V →ₗ[K] V'),
  Eq (α := LinearMap.{u_3, u_3, u_4, u_5} (RingHom.id K) (↥⊥) V') (g ∘ₗ Submodule.subtype ⊥) 0 →
    ∀ (hg : (g : (a : V) → V') v = w), Nontrivial (V →ₗ[K] V')
Tactic: obtain ⟨g, _, hg⟩ := LinearMap.exists_extend_of_notMem (K := K) 0 this w
-- 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
p : Submodule K V
hp : p < ⊤
⊢ ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ f.ker
have rcases : ∀ (v : V) (hpv : v ∉ p), ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ f.ker
Tactic: rcases SetLike.exists_of_lt hp with ⟨v, -, hpv⟩
-- 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
p : Submodule K V
hp : p < ⊤
v : V
hpv : v ∉ p
⊢ ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ f.ker
have rcases : ∀ (f : V →ₗ[K] K) (hfv : Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)) (hpf : p ≤ f.ker),
  ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ f.ker
Tactic: rcases exists_le_ker_of_notMem hpv with ⟨f, hfv, hpf⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
⊢ span K s = f.ker
have simp : map f.ker.subtype
    (span K
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
        (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))) =
  f.ker
Tactic: simp only [s, span_image]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (hypothesis)
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
⊢ ∃ (n : Set V) (b : Basis (↑n : Type u_7) K V) (i : (↑n : Type u_7)),
    v = (b : (a : (↑n : Type u_7)) → V) i ∧ f = HSMul.hSMul (α := K) ((f : (a : V) → K) v : K) (b.coord i)
have hs : span K s = f.ker
Tactic: have hs : span K s = ker f := by
    simp only [s, span_image]
    simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
⊢ LinearIndepOn K _root_.id n
have hs₁ : LinearIndepOn K _root_.id s
Tactic: apply LinearIndepOn.id_insert
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
hs₁ : LinearIndepOn K _root_.id s
⊢ LinearIndepOn K _root_.id n
have hx : v ∉ span K s
Tactic: apply LinearIndepOn.id_insert
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
⊢ LinearIndepOn K _root_.id s
have hs₁ : LinearIndepOn.{u_7, u_6, u_7} (ι := ↥f.ker) K _root_.id
  (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
    (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
Tactic: apply LinearIndepOn.image
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.VectorSpace (goal)
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
hs₁ :
  LinearIndepOn.{u_7, u_6, u_7} (ι := ↥f.ker) K _root_.id
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
⊢ LinearIndepOn K _root_.id s
have hs₂ : Disjoint
  (span K
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker)))
  f.ker.subtype.ker
Tactic: apply LinearIndepOn.image