-- 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:
rw [← Submodule.linearProjOfIsCompl_apply_eq_zero_iff hpq, LinearMap.map_add,
  Submodule.linearProjOfIsCompl_apply_right, add_zero,
  Submodule.linearProjOfIsCompl_apply_eq_zero_iff]

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) ∉ q

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 ∈ (↑q)ᶜ, ∀ y ∈ (↑q)ᶜ, JoinedIn (↑q)ᶜ x y

Tactic:
intro x hx y hy

Result:
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)ᶜ
⊢ JoinedIn (↑q)ᶜ x y

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 ⋯
⊢ JoinedIn (↑q)ᶜ x y

Tactic:
refine ⟨(γ₁'.add γ₂').cast (Submodule.linear_proj_add_linearProjOfIsCompl_eq_self hpq x).symm
  (Submodule.linear_proj_add_linearProjOfIsCompl_eq_self hpq y).symm, fun t ↦ ?_⟩

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
⊢ ((γ₁'.add γ₂').cast ⋯ ⋯) t ∈ (↑q)ᶜ

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)
⊢ JoinedIn (↑q)ᶜ x y

Tactic:
let γ₁' : Path (_ : E) _ := γ₁.map continuous_subtype_val

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 ⋯
⊢ JoinedIn (↑q)ᶜ x y