-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem inter_eq_singleton_of_nonempty_of_isCompl {s₁ s₂ : AffineSubspace k P}
    (h1 : (s₁ : Set P).Nonempty) (h2 : (s₂ : Set P).Nonempty)
    (hd : IsCompl s₁.direction s₂.direction) : ∃ p, (s₁ : Set P) ∩ s₂ = {p}

Proof state:
case h.h.mp.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
hq1 : q ∈ ↑s₁
hq2 : q ∈ ↑s₂
⊢ q = p

Tactic:
have hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction :=
  ⟨vsub_mem_direction hq1 hp.1, vsub_mem_direction hq2 hp.2⟩

Result:
case h.h.mp.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
hq1 : q ∈ ↑s₁
hq2 : q ∈ ↑s₂
hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction
⊢ q = p

Proof state:
case h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
⊢ q ∈ ↑s₁ ∩ ↑s₂ ↔ q ∈ {p}

Tactic:
rw [Set.mem_singleton_iff]

Result:
case h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
⊢ q ∈ ↑s₁ ∩ ↑s₂ ↔ q = p

Proof state:
case h.h.mp.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
hq1 : q ∈ ↑s₁
hq2 : q ∈ ↑s₂
hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction
⊢ q = p

Tactic:
rwa [hd.inf_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hqp

Result:
no goals

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
⊢ ↑s₁ ∩ ↑s₂ = {p}

Tactic:
ext q

Result:
case h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
⊢ q ∈ ↑s₁ ∩ ↑s₂ ↔ q ∈ {p}

Proof state:
case h.h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
⊢ q ∈ ↑s₁ ∩ ↑s₂ → q = p

Tactic:
rintro ⟨hq1, hq2⟩

Result:
case h.h.mp.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
hq1 : q ∈ ↑s₁
hq2 : q ∈ ↑s₂
⊢ q = p

Proof state:
case h.h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
⊢ q = p → q ∈ ↑s₁ ∩ ↑s₂

Tactic:
exact fun h => h.symm ▸ hp

Result:
no goals

Proof state:
case h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
⊢ q ∈ ↑s₁ ∩ ↑s₂ ↔ q = p

Tactic:
constructor

Result:
case h.h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
⊢ q ∈ ↑s₁ ∩ ↑s₂ → q = p

case h.h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
⊢ q = p → q ∈ ↑s₁ ∩ ↑s₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
⊢ ∃ p, ↑s₁ ∩ ↑s₂ = {p}

Tactic:
obtain ⟨p, hp⟩ := inter_nonempty_of_nonempty_of_sup_direction_eq_top h1 h2 hd.sup_eq_top

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
⊢ ∃ p, ↑s₁ ∩ ↑s₂ = {p}

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
⊢ ∃ p, ↑s₁ ∩ ↑s₂ = {p}

Tactic:
use p

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
⊢ ↑s₁ ∩ ↑s₂ = {p}