-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
lemma ker_restrict_eq_of_codisjoint {p q : Submodule R M} (hpq : Codisjoint p q)
    {B : LinearMap.BilinForm R M} (hB : ∀ x ∈ p, ∀ y ∈ q, B x y = 0) :
    LinearMap.ker (B.restrict p) = (LinearMap.ker B).comap p.subtype

Proof state:
case h.mk.refine_1.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : (B.restrict p) ⟨z, hz⟩ = 0
w : M
⊢ (B z) w = 0 w

Tactic:
obtain ⟨x, hx, y, hy, rfl⟩ := Submodule.exists_add_eq_of_codisjoint hpq w

Result:
case h.mk.refine_1.h.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : (B.restrict p) ⟨z, hz⟩ = 0
x : M
hx : x ∈ p
y : M
hy : y ∈ q
⊢ (B z) (x + y) = 0 (x + y)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
⊢ ker (B.restrict p) = Submodule.comap p.subtype (ker B)

Tactic:
ext ⟨z, hz⟩

Result:
case h.mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
⊢ ⟨z, hz⟩ ∈ ker (B.restrict p) ↔ ⟨z, hz⟩ ∈ Submodule.comap p.subtype (ker B)

Proof state:
case h.mk.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : (B.restrict p) ⟨z, hz⟩ = 0
⊢ B z = 0

Tactic:
ext w

Result:
case h.mk.refine_1.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : (B.restrict p) ⟨z, hz⟩ = 0
w : M
⊢ (B z) w = 0 w

Proof state:
case h.mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
⊢ ⟨z, hz⟩ ∈ ker (B.restrict p) ↔ ⟨z, hz⟩ ∈ Submodule.comap p.subtype (ker B)

Tactic:
simp only [LinearMap.mem_ker, Submodule.mem_comap, Submodule.coe_subtype]

Result:
case h.mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
⊢ (B.restrict p) ⟨z, hz⟩ = 0 ↔ B z = 0

Proof state:
case h.mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
⊢ (B.restrict p) ⟨z, hz⟩ = 0 ↔ B z = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case h.mk.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : (B.restrict p) ⟨z, hz⟩ = 0
⊢ B z = 0

case h.mk.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : B z = 0
⊢ (B.restrict p) ⟨z, hz⟩ = 0

Proof state:
case h.mk.refine_2.h.mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : B z = 0
x : M
hx : x ∈ p
⊢ ((B.restrict p) ⟨z, hz⟩) ⟨x, hx⟩ = 0 ⟨x, hx⟩

Tactic:
simpa using LinearMap.congr_fun h x

Result:
no goals

Proof state:
case h.mk.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : B z = 0
⊢ (B.restrict p) ⟨z, hz⟩ = 0

Tactic:
ext ⟨x, hx⟩

Result:
case h.mk.refine_2.h.mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : B z = 0
x : M
hx : x ∈ p
⊢ ((B.restrict p) ⟨z, hz⟩) ⟨x, hx⟩ = 0 ⟨x, hx⟩

Proof state:
case h.mk.refine_1.h.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : (B.restrict p) ⟨z, hz⟩ = 0
x : M
hx : x ∈ p
y : M
hy : y ∈ q
⊢ (B z) (x + y) = 0 (x + y)

Tactic:
simpa [hB z hz y hy] using LinearMap.congr_fun h ⟨x, hx⟩

Result:
no goals