-- 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
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

Tactic:
have : π hpq x ≠ 0 ∧ π hpq y ≠ 0 := by
  constructor <;> intro h <;> rw [Submodule.linearProjOfIsCompl_apply_eq_zero_iff hpq] at h <;>
    [exact hx h; exact hy h]

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)ᶜ
this : (p.linearProjOfIsCompl q hpq) x ≠ 0 ∧ (p.linearProjOfIsCompl q hpq) y ≠ 0
⊢ 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 ⋯
t : ↑unitInterval
⊢ ((γ₁'.add γ₂').cast ⋯ ⋯) t ∈ (↑q)ᶜ

Tactic:
rw [Path.cast_coe, Path.add_apply]

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:
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

Tactic:
let γ₂ := PathConnectedSpace.somePath (π hpq.symm x) (π hpq.symm y)

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

Proof state:
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

Tactic:
exact ⟨a, mt (Submodule.eq_zero_of_coe_mem_of_disjoint hpq.disjoint) ha⟩

Result:
no goals

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

Tactic:
exact mt (Submodule.eq_zero_of_coe_mem_of_disjoint hpq.disjoint) (hγ₁ t)

Result:
no goals

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 ⋯
⊢ 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 ⋯
γ₂' : Path ↑((q.linearProjOfIsCompl p ⋯) x) ↑((q.linearProjOfIsCompl p ⋯) y) := γ₂.map ⋯
⊢ JoinedIn (↑q)ᶜ x y