-- 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
hy' : g y = 0
⊢ f (y + z) = g (y + z)

Tactic:
replace hy : f y = 0 := by rwa [LinearMap.mem_ker] at hy

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 z : V₁
hz : z ∈ p
hy' : g y = 0
hy : f 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 ≠ ⊥
⊢ Disjoint (LinearMap.ker f) p

Tactic:
rw [disjoint_iff, Submodule.eq_bot_iff]

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 ≠ ⊥
⊢ ∀ x ∈ LinearMap.ker f ⊓ p, x = 0

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
ht : t = 0
⊢ t • x = 0

Tactic:
simp [ht]

Result:
no goals

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 z : V₁
hz : z ∈ p
hy' : g y = 0
hy : f y = 0
⊢ f (y + z) = g (y + z)

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

Result:
case h.intro.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' : g y = 0
hy : f y = 0
t : K
hz : t • x ∈ p
⊢ f (y + t • x) = g (y + t • x)

Proof state:
case h.intro.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' : g y = 0
hy : f y = 0
t : K
hz : t • x ∈ p
⊢ f (y + t • x) = g (y + t • x)

Tactic:
simp [h', hy, 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
⊢ f = g

Tactic:
let p := K ∙ x

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}
⊢ f = g

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 ≠ ⊥
⊢ ∀ x ∈ LinearMap.ker f ⊓ p, x = 0

Tactic:
rintro y ⟨hfy : f y = 0, hpy : y ∈ p⟩

Result:
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

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
v : V₁
this : v ∈ ⊤
⊢ ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v

Tactic:
rwa [← (isCompl_ker_of_disjoint_of_ne_bot hf hpf hp).sup_eq_top, Submodule.mem_sup] at this

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 ≠ ⊥
⊢ f = g

Tactic:
have hpf : Disjoint (LinearMap.ker f) p := by
  rw [disjoint_iff, Submodule.eq_bot_iff]
  rintro y ⟨hfy : f y = 0, hpy : y ∈ p⟩
  obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hpy
  have ht : t = 0 := by simpa [hx] using hfy
  simp [ht]

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 ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
⊢ f = g

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 = g

Tactic:
have hf : f ≠ 0 := 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 ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
⊢ f = g

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
v : V₁
⊢ ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v

Tactic:
have : v ∈ (⊤ : Submodule K V₁) := Submodule.mem_top

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 ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
v : V₁
this : v ∈ ⊤
⊢ ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v