awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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.{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')

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]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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')
dsimp :
  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)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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')
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) ⋯)
        ((f : (a : V) → V') (↑b : V)) ⋯) =
    (↑b : 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)

Tactic:
rw [Basis.ofVectorSpace_apply_self, fb_eq, hC.constr_basis]

Premises used: Module.Basis.ofVectorSpace_apply_self, Module.Basis.constr_basis
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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')
⊢ 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) ⋯)
        ((f : (a : V) → V') (↑b : V)) ⋯) =
    (↑b : V)

Tactic:
leftInverse_invFun (LinearMap.ker_eq_bot.1 hf_inj) _

Premises used: LinearMap.ker_eq_bot, Function.leftInverse_invFun, Iff.mp, Set.restrict
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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')
⊢ 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) ⋯)
        ((f : (a : V) → V') (↑b : V)) ⋯) =
    (↑b : V)

Tactic:
exact leftInverse_invFun (LinearMap.ker_eq_bot.1 hf_inj) _

Premises used: LinearMap.ker_eq_bot, Function.leftInverse_invFun, Iff.mp
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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'
h_inj : f.ker = ⊥
⊢ f.leftInverse ∘ₗ f = id

Tactic:
simpa [leftInverse, h_inj] using (f.exists_leftInverse_of_injective h_inj).choose_spec

Premises used: Exists.choose_spec, LinearMap.exists_leftInverse_of_injective, LinearMap.leftInverse
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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'
h_inj : f.ker = ⊥
x : V
⊢ (f.leftInverse : (a : V') → V) ((f : (a : V) → V') x : V') = x

Tactic:
LinearMap.ext_iff.mp (f.leftInverse_comp_of_inj h_inj) x

Premises used: LinearMap.ext_iff, LinearMap.leftInverse_comp_of_inj, Iff.mp
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
⊢ ∃ (q : Submodule K V), IsCompl p q

Tactic:
⟨LinearMap.ker p.subtype.leftInverse,
    LinearMap.isCompl_of_proj <| LinearMap.leftInverse_apply_of_inj p.ker_subtype⟩

Premises used: Submodule.ker_subtype, LinearMap.ker, LinearMap.leftInverse, LinearMap.leftInverse_apply_of_inj, Exists.intro, Submodule.subtype, LinearMap.isCompl_of_proj
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
⊢ ComplementedLattice.{u_4} (Submodule K V)

Tactic:
⟨Submodule.exists_isCompl⟩

Premises used: ComplementedLattice.mk, Submodule.exists_isCompl
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
rw₂ rw₃ : f = f
⊢ (f ∘ₗ g) ∘ₗ p.subtype = f

Tactic:
rw [LinearMap.comp_assoc, hg, f.comp_id]

Premises used: LinearMap.comp_assoc, LinearMap.comp_id
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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'
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
⊢ ∃ (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⟩

Premises used: LinearPMap.toFun, LinearMap.exists_extend, LinearPMap.supSpanSingleton, LinearPMap.mk
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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

Tactic:
⟨g, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
refine_2 : (g : (a : V) → V') v = y
⊢ ∃ (g : V →ₗ[K] V'), g ∘ₗ p.subtype = f ∧ (g : (a : V) → V') v = y

Tactic:
refine ⟨g, ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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 : ∀ (x : ↥p), Eq.{u_5 + 1} (α := V') ((g ∘ₗ p.subtype : (a : ↥p) → V') x : V') ((f : (a : ↥p) → V') x : V')
⊢ g ∘ₗ p.subtype = f

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
⊢ (↑({ 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) ⋯) =
    (↑{ 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) ⋯)

Tactic:
have := LinearPMap.supSpanSingleton_apply_mk_of_mem ⟨p, f⟩ y hv x.2
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
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) ⋯) =
    (↑{ 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) ⋯)
⊢ Eq.{u_5 + 1} (α := V') ((g ∘ₗ p.subtype : (a : ↥p) → V') x : V') ((f : (a : ↥p) → V') x : V')

Tactic:
simpa using congr($hg _).trans this

Premises used: congrArg, id, DFunLike.coe, Eq.trans
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
⊢ (↑({ 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
        ⋯) =
    y

Tactic:
have := LinearPMap.supSpanSingleton_apply_self ⟨p, f⟩ y hv
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
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
        ⋯) =
    y
⊢ (g : (a : V) → V') v = y

Tactic:
simpa using congr($hg _).trans this

Premises used: congrArg, id, DFunLike.coe, Eq.trans
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
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
⊢ ∃ (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⟩

Premises used: OfNat.ofNat, LinearMap.exists_extend_of_notMem
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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)
⊢ Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)

Tactic:
simp [hfv]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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)
refine : ∀ (x : V) (hx : x ∈ p), x ∈ f.ker
⊢ ∃ (f : V →ₗ[K] K), Ne.{u_3 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K) ∧ p ≤ f.ker

Tactic:
refine ⟨f, by simp [hfv], fun x hx ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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)
x : V
hx : x ∈ p
⊢ x ∈ f.ker

Tactic:
simpa using congr($hpf ⟨x, hx⟩)
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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'
obtain : ∀ (v : V) (hv : v ≠ 0), Nontrivial (V →ₗ[K] V')
⊢ Nontrivial (V →ₗ[K] V')

Tactic:
obtain ⟨v, hv⟩ := exists_ne (0 : V)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
obtain : ∀ (w : V') (hw : w ≠ 0), Nontrivial (V →ₗ[K] V')
⊢ Nontrivial (V →ₗ[K] V')

Tactic:
obtain ⟨w, hw⟩ := exists_ne (0 : V')

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
⊢ v ∉ ⊥

Tactic:
simp only [mem_bot, hv, not_false_eq_true]

Premises used: Submodule.mem_bot, not_false_eq_true
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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
⊢ v ∉ ⊥

Tactic:
have : v ∉ (⊥ : Submodule K V) := by simp only [mem_bot, hv, not_false_eq_true]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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 ∉ ⊥
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')
⊢ Nontrivial (V →ₗ[K] V')

Tactic:
obtain ⟨g, _, hg⟩ := LinearMap.exists_extend_of_notMem (K := K) 0 this w

Premises used: OfNat.ofNat, LinearMap.exists_extend_of_notMem
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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 ∉ ⊥
g : V →ₗ[K] V'
left : 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
⊢ Ne.{u_5 + 1} (α := V') ((g : (a : V) → V') v : V') ((0 : (a : V) → V') v : V')

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
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 ∉ ⊥
g : V →ₗ[K] V'
left : 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:
exact ⟨g, 0, DFunLike.ne_iff.mpr ⟨v, by simp_all⟩⟩