-- Mathlib/LinearAlgebra/Basis/VectorSpace.lean
theorem Submodule.exists_le_ker_of_lt_top (p : Submodule K V) (hp : p < ⊤) :
    ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ ker f

Proof state:
case intro.intro.intro.refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hf :
  f ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
x : V
hx : x ∈ p
⊢ f x = 0

Tactic:
have := LinearPMap.supSpanSingleton_apply_mk ⟨p, 0⟩ v (1 : K) hpv x hx 0

Result:
case intro.intro.intro.refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hf :
  f ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
x : V
hx : x ∈ p
this :
  ↑({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv) ⟨x + 0 • v, ⋯⟩ = ↑{ domain := p, toFun := 0 } ⟨x, hx⟩ + 0 • 1
⊢ f x = 0

Proof state:
case intro.intro.intro.refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hf :
  f ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
x : V
hx : x ∈ p
this :
  ↑({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv) ⟨x + 0 • v, ⋯⟩ = ↑{ domain := p, toFun := 0 } ⟨x, hx⟩ + 0 • 1
⊢ f x = 0

Tactic:
simpa using (LinearMap.congr_fun hf _).trans this

Result:
no goals

Proof state:
case intro.intro.intro.refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hf :
  f ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
⊢ f ≠ 0

Tactic:
rintro rfl

Result:
case intro.intro.intro.refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
hf :
  0 ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
⊢ False

Proof state:
case intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hf :
  f ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f

Tactic:
refine ⟨f, ?_, ?_⟩

Result:
case intro.intro.intro.refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hf :
  f ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
⊢ f ≠ 0

case intro.intro.intro.refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hf :
  f ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
⊢ p ≤ ker f

Proof state:
case intro.intro.intro.refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
hf : 0 = ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
⊢ False

Tactic:
have := LinearPMap.supSpanSingleton_apply_mk ⟨p, 0⟩ v (1 : K) hpv 0 p.zero_mem 1

Result:
case intro.intro.intro.refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
hf : 0 = ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
this :
  ↑({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv) ⟨0 + 1 • v, ⋯⟩ = ↑{ domain := p, toFun := 0 } ⟨0, ⋯⟩ + 1 • 1
⊢ False

Proof state:
case intro.intro.intro.refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hf :
  f ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
⊢ p ≤ ker f

Tactic:
refine fun x hx => mem_ker.2 ?_

Result:
case intro.intro.intro.refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hf :
  f ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
x : V
hx : x ∈ p
⊢ f x = 0

Proof state:
case intro.intro.intro.refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
hf :
  0 ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
⊢ False

Tactic:
rw [LinearMap.zero_comp] at hf

Result:
case intro.intro.intro.refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
hf : 0 = ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
⊢ False

Proof state:
case intro.intro.intro.refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
hf : 0 = ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
this :
  ↑({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv) ⟨0 + 1 • v, ⋯⟩ = ↑{ domain := p, toFun := 0 } ⟨0, ⋯⟩ + 1 • 1
⊢ False

Tactic:
simpa using (LinearMap.congr_fun hf _).trans this

Result:
no goals

Proof state:
case intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
hp : p < ⊤
v : V
hpv : v ∉ p
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f

Tactic:
clear hp

Result:
case intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f

Proof state:
case intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f

Tactic:
rcases (LinearPMap.supSpanSingleton ⟨p, 0⟩ v (1 : K) hpv).toFun.exists_extend with ⟨f, hf⟩

Result:
case intro.intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hpv : v ∉ p
f : V →ₗ[K] K
hf :
  f ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype =
    ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f

Proof state:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
hp : p < ⊤
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f

Tactic:
rcases SetLike.exists_of_lt hp with ⟨v, -, hpv⟩

Result:
case intro.intro
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
hp : p < ⊤
v : V
hpv : v ∉ p
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f