case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y → Nullhomotopic (ContinuousMap.id Y)

case mpr
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ Nullhomotopic (ContinuousMap.id Y) → ContractibleSpace Y
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y ↔ Nullhomotopic (ContinuousMap.id Y)
constructor
case mpr.intro
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ ContractibleSpace Y
case mpr
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ Nullhomotopic (ContinuousMap.id Y) → ContractibleSpace Y
rintro ⟨p, h⟩
case mpr.intro.refine_1
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (comp (const Unit p) (const Y ())) (ContinuousMap.id Y)

case mpr.intro.refine_2
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (comp (const Y ()) (const Unit p)) (ContinuousMap.id Unit)
case mpr.intro
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ ContractibleSpace Y
refine
  { hequiv_unit' :=
      ⟨{  toFun := ContinuousMap.const _ ()
          invFun := ContinuousMap.const _ p
          left_inv := ?_
          right_inv := ?_ }⟩ }
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : ContractibleSpace Y
⊢ Nullhomotopic (ContinuousMap.id Y)
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y → Nullhomotopic (ContinuousMap.id Y)
intro
no goals
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : ContractibleSpace Y
⊢ Nullhomotopic (ContinuousMap.id Y)
apply id_nullhomotopic
no goals
case mpr.intro.refine_1
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (comp (const Unit p) (const Y ())) (ContinuousMap.id Y)
exact h.symm
no goals
case mpr.intro.refine_2
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (comp (const Y ()) (const Unit p)) (ContinuousMap.id Unit)
convert Homotopic.refl (ContinuousMap.id Unit)