-- Mathlib/LinearAlgebra/Dual.lean
lemma eq_of_ker_eq_of_apply_eq [FiniteDimensional K V₁] {f g : Module.Dual K V₁} (x : V₁)
    (h : LinearMap.ker f = LinearMap.ker g) (h' : f x = g x) (hx : f x ≠ 0) :
    f = g

Proof state:
case h.intro.intro.intro.intro
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
y : V₁
hy : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
⊢ f (y + z) = g (y + z)

Tactic:
have hy' : g y = 0 := by rwa [← LinearMap.mem_ker, ← h]

Result:
case h.intro.intro.intro.intro
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
y : V₁
hy : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
hy' : g y = 0
⊢ f (y + z) = g (y + z)

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
t : K
hfy : f (t • x) = 0
hpy : t • x ∈ p
⊢ t = 0

Tactic:
simpa [hx] using hfy

Result:
no goals

Proof state:
case intro.intro
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
t : K
hfy : f (t • x) = 0
hpy : t • x ∈ p
⊢ t • x = 0

Tactic:
have ht : t = 0 := by simpa [hx] using hfy

Result:
case intro.intro
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
t : K
hfy : f (t • x) = 0
hpy : t • x ∈ p
ht : t = 0
⊢ t • x = 0

Proof state:
case h
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
v : V₁
⊢ f v = g v

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ : ∃ᵉ (y ∈ LinearMap.ker f) (z ∈ p), y + z = v := by
  have : v ∈ (⊤ : Submodule K V₁) := Submodule.mem_top
  rwa [← (isCompl_ker_of_disjoint_of_ne_bot hf hpf hp).sup_eq_top, Submodule.mem_sup] at this

Result:
case h.intro.intro.intro.intro
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
y : V₁
hy : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
⊢ f (y + z) = g (y + z)

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
y : V₁
hy : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
⊢ g y = 0

Tactic:
rwa [← LinearMap.mem_ker, ← h]

Result:
no goals

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
⊢ f ≠ 0

Tactic:
aesop

Result:
no goals

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
⊢ p ≠ ⊥

Tactic:
aesop

Result:
no goals

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
y : V₁
hy : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
hy' : g y = 0
⊢ f y = 0

Tactic:
rwa [LinearMap.mem_ker] at hy

Result:
no goals

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
⊢ f = g

Tactic:
ext v

Result:
case h
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
v : V₁
⊢ f v = g v

Proof state:
case intro
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
y : V₁
hfy : f y = 0
hpy : y ∈ p
⊢ y = 0

Tactic:
obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hpy

Result:
case intro.intro
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
t : K
hfy : f (t • x) = 0
hpy : t • x ∈ p
⊢ t • x = 0

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
⊢ f = g

Tactic:
have hp : p ≠ ⊥ := by aesop

Result:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := span K {x}
hp : p ≠ ⊥
⊢ f = g