-- Mathlib/Analysis/Convex/Topology.lean
theorem isPathConnected_compl_of_isPathConnected_compl_zero [ContinuousSMul ℝ E]
    {p q : Submodule ℝ E} (hpq : IsCompl p q) (hpc : IsPathConnected ({0}ᶜ : Set p)) :
    IsPathConnected (qᶜ : Set E)

Proof state:
case right.intro
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y
x : E
hx : x ∈ (↑q)ᶜ
y : E
hy : y ∈ (↑q)ᶜ
this : (p.linearProjOfIsCompl q hpq) x ≠ 0 ∧ (p.linearProjOfIsCompl q hpq) y ≠ 0
γ₁ : Path ((p.linearProjOfIsCompl q hpq) x) ((p.linearProjOfIsCompl q hpq) y)
hγ₁ : ∀ (t : ↑unitInterval), γ₁ t ∈ {0}ᶜ
γ₂ : Path ((q.linearProjOfIsCompl p ⋯) x) ((q.linearProjOfIsCompl p ⋯) y) :=
  PathConnectedSpace.somePath ((q.linearProjOfIsCompl p ⋯) x) ((q.linearProjOfIsCompl p ⋯) y)
γ₁' : Path ↑((p.linearProjOfIsCompl q hpq) x) ↑((p.linearProjOfIsCompl q hpq) y) := γ₁.map ⋯
γ₂' : Path ↑((q.linearProjOfIsCompl p ⋯) x) ↑((q.linearProjOfIsCompl p ⋯) y) := γ₂.map ⋯
t : ↑unitInterval
⊢ γ₁' t + γ₂' t ∈ (↑q)ᶜ

Tactic:
change γ₁ t + (γ₂ t : E) ∉ q

Result:
case right.intro
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y
x : E
hx : x ∈ (↑q)ᶜ
y : E
hy : y ∈ (↑q)ᶜ
this : (p.linearProjOfIsCompl q hpq) x ≠ 0 ∧ (p.linearProjOfIsCompl q hpq) y ≠ 0
γ₁ : Path ((p.linearProjOfIsCompl q hpq) x) ((p.linearProjOfIsCompl q hpq) y)
hγ₁ : ∀ (t : ↑unitInterval), γ₁ t ∈ {0}ᶜ
γ₂ : Path ((q.linearProjOfIsCompl p ⋯) x) ((q.linearProjOfIsCompl p ⋯) y) :=
  PathConnectedSpace.somePath ((q.linearProjOfIsCompl p ⋯) x) ((q.linearProjOfIsCompl p ⋯) y)
γ₁' : Path ↑((p.linearProjOfIsCompl q hpq) x) ↑((p.linearProjOfIsCompl q hpq) y) := γ₁.map ⋯
γ₂' : Path ↑((q.linearProjOfIsCompl p ⋯) x) ↑((q.linearProjOfIsCompl p ⋯) y) := γ₂.map ⋯
t : ↑unitInterval
⊢ ↑(γ₁ t) + ↑(γ₂ t) ∉ q

Proof state:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected {0}ᶜ
⊢ IsPathConnected (↑q)ᶜ

Tactic:
rw [isPathConnected_iff] at hpc ⊢

Result:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y
⊢ (↑q)ᶜ.Nonempty ∧ ∀ x ∈ (↑q)ᶜ, ∀ y ∈ (↑q)ᶜ, JoinedIn (↑q)ᶜ x y

Proof state:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y
⊢ (↑q)ᶜ.Nonempty ∧ ∀ x ∈ (↑q)ᶜ, ∀ y ∈ (↑q)ᶜ, JoinedIn (↑q)ᶜ x y

Tactic:
constructor

Result:
case left
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y
⊢ (↑q)ᶜ.Nonempty

case right
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y
⊢ ∀ x ∈ (↑q)ᶜ, ∀ y ∈ (↑q)ᶜ, JoinedIn (↑q)ᶜ x y

Proof state:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y
x : E
hx : x ∈ (↑q)ᶜ
y : E
hy : y ∈ (↑q)ᶜ
⊢ (p.linearProjOfIsCompl q hpq) x ≠ 0 ∧ (p.linearProjOfIsCompl q hpq) y ≠ 0

Tactic:
constructor <;> intro h <;> rw [Submodule.linearProjOfIsCompl_apply_eq_zero_iff hpq] at h <;>
  [exact hx h; exact hy h]

Result:
no goals

Proof state:
case left
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y
⊢ (↑q)ᶜ.Nonempty

Tactic:
rcases hpc.1 with ⟨a, ha⟩

Result:
case left.intro
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y
a : ↥p
ha : a ∈ {0}ᶜ
⊢ (↑q)ᶜ.Nonempty

Proof state:
case right
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y
x : E
hx : x ∈ (↑q)ᶜ
y : E
hy : y ∈ (↑q)ᶜ
this : (p.linearProjOfIsCompl q hpq) x ≠ 0 ∧ (p.linearProjOfIsCompl q hpq) y ≠ 0
⊢ JoinedIn (↑q)ᶜ x y

Tactic:
rcases hpc.2 (π hpq x) this.1 (π hpq y) this.2 with ⟨γ₁, hγ₁⟩

Result:
case right.intro
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y
x : E
hx : x ∈ (↑q)ᶜ
y : E
hy : y ∈ (↑q)ᶜ
this : (p.linearProjOfIsCompl q hpq) x ≠ 0 ∧ (p.linearProjOfIsCompl q hpq) y ≠ 0
γ₁ : Path ((p.linearProjOfIsCompl q hpq) x) ((p.linearProjOfIsCompl q hpq) y)
hγ₁ : ∀ (t : ↑unitInterval), γ₁ t ∈ {0}ᶜ
⊢ JoinedIn (↑q)ᶜ x y