-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem comap_eq_sup_ker_of_disjoint {p : Submodule K V} [FiniteDimensional K p] {f : V →ₗ[K] V}
    (h : ∀ x ∈ p, f x ∈ p) (h' : Disjoint p (ker f)) :
    p.comap f = p ⊔ ker f

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p (ker f)
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : f y = f x
⊢ x - y ∈ ker f

Tactic:
simp [hxy]

Result:
no goals

Proof state:
case intro.mk
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p (ker f)
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : f y = f x
⊢ x ∈ p ⊔ ker f

Tactic:
exact Submodule.mem_sup.mpr ⟨y, hy, x - y, by simp [hxy], add_sub_cancel y x⟩

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p (ker f)
x : V
hx : x ∈ comap f p
⊢ x ∈ p ⊔ ker f

Tactic:
obtain ⟨⟨y, hy⟩, hxy⟩ :=
  surjective_of_injective ((injective_restrict_iff_disjoint h).mpr h') ⟨f x, hx⟩

Result:
case intro.mk
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p (ker f)
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : (f.restrict h) ⟨y, hy⟩ = ⟨f x, hx⟩
⊢ x ∈ p ⊔ ker f

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p (ker f)
⊢ comap f p = p ⊔ ker f

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (sup_le_iff.mpr ⟨h, ker_le_comap _⟩)

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p (ker f)
x : V
hx : x ∈ comap f p
⊢ x ∈ p ⊔ ker f

Proof state:
case intro.mk
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p (ker f)
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : (f.restrict h) ⟨y, hy⟩ = ⟨f x, hx⟩
⊢ x ∈ p ⊔ ker f

Tactic:
replace hxy : f y = f x := by simpa [Subtype.ext_iff] using hxy

Result:
case intro.mk
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p (ker f)
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : f y = f x
⊢ x ∈ p ⊔ ker f

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p (ker f)
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : (f.restrict h) ⟨y, hy⟩ = ⟨f x, hx⟩
⊢ f y = f x

Tactic:
simpa [Subtype.ext_iff] using hxy

Result:
no goals