[GOAL]
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ Continuous fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd))
[PROOFSTEP]
exact
  ((map_continuous HSpace.hmul).comp
        ((continuous_fst.comp continuous_fst).prod_mk (continuous_fst.comp continuous_snd))).prod_mk
    ((map_continuous HSpace.hmul).comp
      ((continuous_snd.comp continuous_fst).prod_mk (continuous_snd.comp continuous_snd)))
[GOAL]
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ ↑(ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd))) ((e, e), e, e) = (e, e)
[PROOFSTEP]
simp only [ContinuousMap.coe_mk, Prod.mk.inj_iff]
[GOAL]
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ ↑hmul (e, e) = e ∧ ↑hmul (e, e) = e
[PROOFSTEP]
exact ⟨HSpace.hmul_e_e, HSpace.hmul_e_e⟩
[GOAL]
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ HomotopyRel
    (comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
      (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
    (ContinuousMap.id (X × Y)) {(e, e)}
[PROOFSTEP]
let G : I × X × Y → X × Y := fun p => (HSpace.eHmul (p.1, p.2.1), HSpace.eHmul (p.1, p.2.2))
[GOAL]
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑eHmul (p.fst, p.snd.fst), ↑eHmul (p.fst, p.snd.snd))
⊢ HomotopyRel
    (comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
      (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
    (ContinuousMap.id (X × Y)) {(e, e)}
[PROOFSTEP]
have hG : Continuous G :=
  (Continuous.comp HSpace.eHmul.1.1.2 (continuous_fst.prod_mk (continuous_fst.comp continuous_snd))).prod_mk
    (Continuous.comp HSpace.eHmul.1.1.2 (continuous_fst.prod_mk (continuous_snd.comp continuous_snd)))
[GOAL]
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑eHmul (p.fst, p.snd.fst), ↑eHmul (p.fst, p.snd.snd))
hG : Continuous G
⊢ HomotopyRel
    (comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
      (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
    (ContinuousMap.id (X × Y)) {(e, e)}
[PROOFSTEP]
use!⟨G, hG⟩
[GOAL]
case map_zero_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑eHmul (p.fst, p.snd.fst), ↑eHmul (p.fst, p.snd.snd))
hG : Continuous G
⊢ ∀ (x : X × Y),
    ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
      ↑(comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
            (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
        x
[PROOFSTEP]
rintro ⟨x, y⟩
[GOAL]
case map_zero_left.mk
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑eHmul (p.fst, p.snd.fst), ↑eHmul (p.fst, p.snd.snd))
hG : Continuous G
x : X
y : Y
⊢ ContinuousMap.toFun (ContinuousMap.mk G) (0, x, y) =
    ↑(comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
          (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
      (x, y)
[PROOFSTEP]
exacts [Prod.mk.inj_iff.mpr ⟨HSpace.eHmul.1.2 x, HSpace.eHmul.1.2 y⟩]
[GOAL]
case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑eHmul (p.fst, p.snd.fst), ↑eHmul (p.fst, p.snd.snd))
hG : Continuous G
⊢ ∀ (x : X × Y), ContinuousMap.toFun (ContinuousMap.mk G) (1, x) = ↑(ContinuousMap.id (X × Y)) x
[PROOFSTEP]
rintro ⟨x, y⟩
[GOAL]
case map_one_left.mk
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑eHmul (p.fst, p.snd.fst), ↑eHmul (p.fst, p.snd.snd))
hG : Continuous G
x : X
y : Y
⊢ ContinuousMap.toFun (ContinuousMap.mk G) (1, x, y) = ↑(ContinuousMap.id (X × Y)) (x, y)
[PROOFSTEP]
exact Prod.mk.inj_iff.mpr ⟨HSpace.eHmul.1.3 x, HSpace.eHmul.1.3 y⟩
[GOAL]
case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑eHmul (p.fst, p.snd.fst), ↑eHmul (p.fst, p.snd.snd))
hG : Continuous G
⊢ ∀ (t : ↑I) (x : X × Y),
    x ∈ {(e, e)} →
      ↑(ContinuousMap.mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := ContinuousMap.mk G,
                      map_zero_left :=
                        (_ :
                          ∀ (x : X × Y),
                            ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                              ↑(comp
                                    (ContinuousMap.mk fun p =>
                                      (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                    (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
                                x),
                      map_one_left :=
                        (_ :
                          ∀ (x : X × Y),
                            ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                              ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
            x ∧
        ↑(ContinuousMap.mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := ContinuousMap.mk G,
                      map_zero_left :=
                        (_ :
                          ∀ (x : X × Y),
                            ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                              ↑(comp
                                    (ContinuousMap.mk fun p =>
                                      (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                    (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
                                x),
                      map_one_left :=
                        (_ :
                          ∀ (x : X × Y),
                            ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                              ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(ContinuousMap.id (X × Y)) x
[PROOFSTEP]
rintro t ⟨x, y⟩ h
[GOAL]
case prop'.mk
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑eHmul (p.fst, p.snd.fst), ↑eHmul (p.fst, p.snd.snd))
hG : Continuous G
t : ↑I
x : X
y : Y
h : (x, y) ∈ {(e, e)}
⊢ ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk G,
                  map_zero_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                          ↑(comp
                                (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
                            x),
                  map_one_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                          ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
              (t, x))
        (x, y) =
      ↑(comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
            (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
        (x, y) ∧
    ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk G,
                  map_zero_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                          ↑(comp
                                (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
                            x),
                  map_one_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                          ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
              (t, x))
        (x, y) =
      ↑(ContinuousMap.id (X × Y)) (x, y)
[PROOFSTEP]
replace h := Prod.mk.inj_iff.mp (Set.mem_singleton_iff.mp h)
[GOAL]
case prop'.mk
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑eHmul (p.fst, p.snd.fst), ↑eHmul (p.fst, p.snd.snd))
hG : Continuous G
t : ↑I
x : X
y : Y
h : x = e ∧ y = e
⊢ ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk G,
                  map_zero_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                          ↑(comp
                                (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
                            x),
                  map_one_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                          ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
              (t, x))
        (x, y) =
      ↑(comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
            (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
        (x, y) ∧
    ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk G,
                  map_zero_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                          ↑(comp
                                (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                (prodMk (const (X × Y) (e, e)) (ContinuousMap.id (X × Y))))
                            x),
                  map_one_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                          ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
              (t, x))
        (x, y) =
      ↑(ContinuousMap.id (X × Y)) (x, y)
[PROOFSTEP]
exact
  ⟨Prod.mk.inj_iff.mpr
      ⟨HomotopyRel.eq_fst HSpace.eHmul t (Set.mem_singleton_iff.mpr h.1),
        HomotopyRel.eq_fst HSpace.eHmul t (Set.mem_singleton_iff.mpr h.2)⟩,
    Prod.mk.inj_iff.mpr ⟨(HSpace.eHmul.2 t x h.1).2, (HSpace.eHmul.2 t y h.2).2⟩⟩
[GOAL]
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ HomotopyRel
    (comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
      (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
    (ContinuousMap.id (X × Y)) {(e, e)}
[PROOFSTEP]
let G : I × X × Y → X × Y := fun p => (HSpace.hmulE (p.1, p.2.1), HSpace.hmulE (p.1, p.2.2))
[GOAL]
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑hmulE (p.fst, p.snd.fst), ↑hmulE (p.fst, p.snd.snd))
⊢ HomotopyRel
    (comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
      (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
    (ContinuousMap.id (X × Y)) {(e, e)}
[PROOFSTEP]
have hG : Continuous G :=
  (Continuous.comp HSpace.hmulE.1.1.2 (continuous_fst.prod_mk (continuous_fst.comp continuous_snd))).prod_mk
    (Continuous.comp HSpace.hmulE.1.1.2 (continuous_fst.prod_mk (continuous_snd.comp continuous_snd)))
[GOAL]
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑hmulE (p.fst, p.snd.fst), ↑hmulE (p.fst, p.snd.snd))
hG : Continuous G
⊢ HomotopyRel
    (comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
      (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
    (ContinuousMap.id (X × Y)) {(e, e)}
[PROOFSTEP]
use!⟨G, hG⟩
[GOAL]
case map_zero_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑hmulE (p.fst, p.snd.fst), ↑hmulE (p.fst, p.snd.snd))
hG : Continuous G
⊢ ∀ (x : X × Y),
    ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
      ↑(comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
            (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
        x
[PROOFSTEP]
rintro ⟨x, y⟩
[GOAL]
case map_zero_left.mk
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑hmulE (p.fst, p.snd.fst), ↑hmulE (p.fst, p.snd.snd))
hG : Continuous G
x : X
y : Y
⊢ ContinuousMap.toFun (ContinuousMap.mk G) (0, x, y) =
    ↑(comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
          (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
      (x, y)
[PROOFSTEP]
exacts [Prod.mk.inj_iff.mpr ⟨HSpace.hmulE.1.2 x, HSpace.hmulE.1.2 y⟩]
[GOAL]
case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑hmulE (p.fst, p.snd.fst), ↑hmulE (p.fst, p.snd.snd))
hG : Continuous G
⊢ ∀ (x : X × Y), ContinuousMap.toFun (ContinuousMap.mk G) (1, x) = ↑(ContinuousMap.id (X × Y)) x
[PROOFSTEP]
rintro ⟨x, y⟩
[GOAL]
case map_one_left.mk
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑hmulE (p.fst, p.snd.fst), ↑hmulE (p.fst, p.snd.snd))
hG : Continuous G
x : X
y : Y
⊢ ContinuousMap.toFun (ContinuousMap.mk G) (1, x, y) = ↑(ContinuousMap.id (X × Y)) (x, y)
[PROOFSTEP]
exact Prod.mk.inj_iff.mpr ⟨HSpace.hmulE.1.3 x, HSpace.hmulE.1.3 y⟩
[GOAL]
case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑hmulE (p.fst, p.snd.fst), ↑hmulE (p.fst, p.snd.snd))
hG : Continuous G
⊢ ∀ (t : ↑I) (x : X × Y),
    x ∈ {(e, e)} →
      ↑(ContinuousMap.mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := ContinuousMap.mk G,
                      map_zero_left :=
                        (_ :
                          ∀ (x : X × Y),
                            ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                              ↑(comp
                                    (ContinuousMap.mk fun p =>
                                      (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                    (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
                                x),
                      map_one_left :=
                        (_ :
                          ∀ (x : X × Y),
                            ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                              ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
            x ∧
        ↑(ContinuousMap.mk fun x =>
                ContinuousMap.toFun
                  { toContinuousMap := ContinuousMap.mk G,
                      map_zero_left :=
                        (_ :
                          ∀ (x : X × Y),
                            ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                              ↑(comp
                                    (ContinuousMap.mk fun p =>
                                      (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                    (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
                                x),
                      map_one_left :=
                        (_ :
                          ∀ (x : X × Y),
                            ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                              ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
                  (t, x))
            x =
          ↑(ContinuousMap.id (X × Y)) x
[PROOFSTEP]
rintro t ⟨x, y⟩ h
[GOAL]
case prop'.mk
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑hmulE (p.fst, p.snd.fst), ↑hmulE (p.fst, p.snd.snd))
hG : Continuous G
t : ↑I
x : X
y : Y
h : (x, y) ∈ {(e, e)}
⊢ ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk G,
                  map_zero_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                          ↑(comp
                                (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
                            x),
                  map_one_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                          ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
              (t, x))
        (x, y) =
      ↑(comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
            (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
        (x, y) ∧
    ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk G,
                  map_zero_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                          ↑(comp
                                (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
                            x),
                  map_one_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                          ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
              (t, x))
        (x, y) =
      ↑(ContinuousMap.id (X × Y)) (x, y)
[PROOFSTEP]
replace h := Prod.mk.inj_iff.mp (Set.mem_singleton_iff.mp h)
[GOAL]
case prop'.mk
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p => (↑hmulE (p.fst, p.snd.fst), ↑hmulE (p.fst, p.snd.snd))
hG : Continuous G
t : ↑I
x : X
y : Y
h : x = e ∧ y = e
⊢ ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk G,
                  map_zero_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                          ↑(comp
                                (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
                            x),
                  map_one_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                          ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
              (t, x))
        (x, y) =
      ↑(comp (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
            (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
        (x, y) ∧
    ↑(ContinuousMap.mk fun x =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk G,
                  map_zero_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (0, x) =
                          ↑(comp
                                (ContinuousMap.mk fun p => (↑hmul (p.fst.fst, p.snd.fst), ↑hmul (p.fst.snd, p.snd.snd)))
                                (prodMk (ContinuousMap.id (X × Y)) (const (X × Y) (e, e))))
                            x),
                  map_one_left :=
                    (_ :
                      ∀ (x : X × Y),
                        ContinuousMap.toFun (ContinuousMap.mk G) (1, x) =
                          ↑(ContinuousMap.id (X × Y)) x) }.toContinuousMap
              (t, x))
        (x, y) =
      ↑(ContinuousMap.id (X × Y)) (x, y)
[PROOFSTEP]
exact
  ⟨Prod.mk.inj_iff.mpr
      ⟨HomotopyRel.eq_fst HSpace.hmulE t (Set.mem_singleton_iff.mpr h.1),
        HomotopyRel.eq_fst HSpace.hmulE t (Set.mem_singleton_iff.mpr h.2)⟩,
    Prod.mk.inj_iff.mpr ⟨(HSpace.hmulE.2 t x h.1).2, (HSpace.hmulE.2 t y h.2).2⟩⟩
[GOAL]
M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
⊢ comp (ContinuousMap.mk (Function.uncurry Mul.mul)) (prodMk (const M 1) (ContinuousMap.id M)) = ContinuousMap.id M
[PROOFSTEP]
ext1
[GOAL]
case h
M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a✝ : M
⊢ ↑(comp (ContinuousMap.mk (Function.uncurry Mul.mul)) (prodMk (const M 1) (ContinuousMap.id M))) a✝ =
    ↑(ContinuousMap.id M) a✝
[PROOFSTEP]
apply one_mul
[GOAL]
M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
⊢ comp (ContinuousMap.mk (Function.uncurry Mul.mul)) (prodMk (ContinuousMap.id M) (const M 1)) = ContinuousMap.id M
[PROOFSTEP]
ext1
[GOAL]
case h
M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a✝ : M
⊢ ↑(comp (ContinuousMap.mk (Function.uncurry Mul.mul)) (prodMk (ContinuousMap.id M) (const M 1))) a✝ =
    ↑(ContinuousMap.id M) a✝
[PROOFSTEP]
apply mul_one
[GOAL]
G G' : Type u
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : Group G'
inst✝ : TopologicalGroup G'
⊢ hSpace (G × G') = HSpace.prod G G'
[PROOFSTEP]
simp only [HSpace.prod]
[GOAL]
G G' : Type u
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : Group G'
inst✝ : TopologicalGroup G'
⊢ hSpace (G × G') =
    { hmul := ContinuousMap.mk fun p => (↑HSpace.hmul (p.fst.fst, p.snd.fst), ↑HSpace.hmul (p.fst.snd, p.snd.snd)),
      e := (HSpace.e, HSpace.e),
      hmul_e_e :=
        (_ :
          ↑(ContinuousMap.mk fun p => (↑HSpace.hmul (p.fst.fst, p.snd.fst), ↑HSpace.hmul (p.fst.snd, p.snd.snd)))
              ((HSpace.e, HSpace.e), HSpace.e, HSpace.e) =
            (HSpace.e, HSpace.e)),
      eHmul :=
        {
          toHomotopy :=
            {
              toContinuousMap :=
                ContinuousMap.mk fun p => (↑HSpace.eHmul (p.fst, p.snd.fst), ↑HSpace.eHmul (p.fst, p.snd.snd)),
              map_zero_left :=
                (_ :
                  ∀ (x : G × G'),
                    ContinuousMap.toFun
                        (ContinuousMap.mk fun p => (↑HSpace.eHmul (p.fst, p.snd.fst), ↑HSpace.eHmul (p.fst, p.snd.snd)))
                        (0, x) =
                      ↑(comp
                            (ContinuousMap.mk fun p =>
                              (↑HSpace.hmul (p.fst.fst, p.snd.fst), ↑HSpace.hmul (p.fst.snd, p.snd.snd)))
                            (prodMk (const (G × G') (HSpace.e, HSpace.e)) (ContinuousMap.id (G × G'))))
                        x),
              map_one_left :=
                (_ :
                  ∀ (x : G × G'),
                    ContinuousMap.toFun
                        (ContinuousMap.mk fun p => (↑HSpace.eHmul (p.fst, p.snd.fst), ↑HSpace.eHmul (p.fst, p.snd.snd)))
                        (1, x) =
                      ↑(ContinuousMap.id (G × G')) x) },
          prop' :=
            (_ :
              ∀ (t : ↑I) (x : G × G'),
                x ∈ {(HSpace.e, HSpace.e)} →
                  ↑(ContinuousMap.mk fun x =>
                            ContinuousMap.toFun
                              {
                                  toContinuousMap :=
                                    ContinuousMap.mk fun p =>
                                      (↑HSpace.eHmul (p.fst, p.snd.fst), ↑HSpace.eHmul (p.fst, p.snd.snd)),
                                  map_zero_left :=
                                    (_ :
                                      ∀ (x : G × G'),
                                        ContinuousMap.toFun
                                            (ContinuousMap.mk fun p =>
                                              (↑HSpace.eHmul (p.fst, p.snd.fst), ↑HSpace.eHmul (p.fst, p.snd.snd)))
                                            (0, x) =
                                          ↑(comp
                                                (ContinuousMap.mk fun p =>
                                                  (↑HSpace.hmul (p.fst.fst, p.snd.fst),
                                                    ↑HSpace.hmul (p.fst.snd, p.snd.snd)))
                                                (prodMk (const (G × G') (HSpace.e, HSpace.e))
                                                  (ContinuousMap.id (G × G'))))
                                            x),
                                  map_one_left :=
                                    (_ :
                                      ∀ (x : G × G'),
                                        ContinuousMap.toFun
                                            (ContinuousMap.mk fun p =>
                                              (↑HSpace.eHmul (p.fst, p.snd.fst), ↑HSpace.eHmul (p.fst, p.snd.snd)))
                                            (1, x) =
                                          ↑(ContinuousMap.id (G × G')) x) }.toContinuousMap
                              (t, x))
                        x =
                      ↑(comp
                            (ContinuousMap.mk fun p =>
                              (↑HSpace.hmul (p.fst.fst, p.snd.fst), ↑HSpace.hmul (p.fst.snd, p.snd.snd)))
                            (prodMk (const (G × G') (HSpace.e, HSpace.e)) (ContinuousMap.id (G × G'))))
                        x ∧
                    ↑(ContinuousMap.mk fun x =>
                            ContinuousMap.toFun
                              {
                                  toContinuousMap :=
                                    ContinuousMap.mk fun p =>
                                      (↑HSpace.eHmul (p.fst, p.snd.fst), ↑HSpace.eHmul (p.fst, p.snd.snd)),
                                  map_zero_left :=
                                    (_ :
                                      ∀ (x : G × G'),
                                        ContinuousMap.toFun
                                            (ContinuousMap.mk fun p =>
                                              (↑HSpace.eHmul (p.fst, p.snd.fst), ↑HSpace.eHmul (p.fst, p.snd.snd)))
                                            (0, x) =
                                          ↑(comp
                                                (ContinuousMap.mk fun p =>
                                                  (↑HSpace.hmul (p.fst.fst, p.snd.fst),
                                                    ↑HSpace.hmul (p.fst.snd, p.snd.snd)))
                                                (prodMk (const (G × G') (HSpace.e, HSpace.e))
                                                  (ContinuousMap.id (G × G'))))
                                            x),
                                  map_one_left :=
                                    (_ :
                                      ∀ (x : G × G'),
                                        ContinuousMap.toFun
                                            (ContinuousMap.mk fun p =>
                                              (↑HSpace.eHmul (p.fst, p.snd.fst), ↑HSpace.eHmul (p.fst, p.snd.snd)))
                                            (1, x) =
                                          ↑(ContinuousMap.id (G × G')) x) }.toContinuousMap
                              (t, x))
                        x =
                      ↑(ContinuousMap.id (G × G')) x) },
      hmulE :=
        {
          toHomotopy :=
            {
              toContinuousMap :=
                ContinuousMap.mk fun p => (↑HSpace.hmulE (p.fst, p.snd.fst), ↑HSpace.hmulE (p.fst, p.snd.snd)),
              map_zero_left :=
                (_ :
                  ∀ (x : G × G'),
                    ContinuousMap.toFun
                        (ContinuousMap.mk fun p => (↑HSpace.hmulE (p.fst, p.snd.fst), ↑HSpace.hmulE (p.fst, p.snd.snd)))
                        (0, x) =
                      ↑(comp
                            (ContinuousMap.mk fun p =>
                              (↑HSpace.hmul (p.fst.fst, p.snd.fst), ↑HSpace.hmul (p.fst.snd, p.snd.snd)))
                            (prodMk (ContinuousMap.id (G × G')) (const (G × G') (HSpace.e, HSpace.e))))
                        x),
              map_one_left :=
                (_ :
                  ∀ (x : G × G'),
                    ContinuousMap.toFun
                        (ContinuousMap.mk fun p => (↑HSpace.hmulE (p.fst, p.snd.fst), ↑HSpace.hmulE (p.fst, p.snd.snd)))
                        (1, x) =
                      ↑(ContinuousMap.id (G × G')) x) },
          prop' :=
            (_ :
              ∀ (t : ↑I) (x : G × G'),
                x ∈ {(HSpace.e, HSpace.e)} →
                  ↑(ContinuousMap.mk fun x =>
                            ContinuousMap.toFun
                              {
                                  toContinuousMap :=
                                    ContinuousMap.mk fun p =>
                                      (↑HSpace.hmulE (p.fst, p.snd.fst), ↑HSpace.hmulE (p.fst, p.snd.snd)),
                                  map_zero_left :=
                                    (_ :
                                      ∀ (x : G × G'),
                                        ContinuousMap.toFun
                                            (ContinuousMap.mk fun p =>
                                              (↑HSpace.hmulE (p.fst, p.snd.fst), ↑HSpace.hmulE (p.fst, p.snd.snd)))
                                            (0, x) =
                                          ↑(comp
                                                (ContinuousMap.mk fun p =>
                                                  (↑HSpace.hmul (p.fst.fst, p.snd.fst),
                                                    ↑HSpace.hmul (p.fst.snd, p.snd.snd)))
                                                (prodMk (ContinuousMap.id (G × G'))
                                                  (const (G × G') (HSpace.e, HSpace.e))))
                                            x),
                                  map_one_left :=
                                    (_ :
                                      ∀ (x : G × G'),
                                        ContinuousMap.toFun
                                            (ContinuousMap.mk fun p =>
                                              (↑HSpace.hmulE (p.fst, p.snd.fst), ↑HSpace.hmulE (p.fst, p.snd.snd)))
                                            (1, x) =
                                          ↑(ContinuousMap.id (G × G')) x) }.toContinuousMap
                              (t, x))
                        x =
                      ↑(comp
                            (ContinuousMap.mk fun p =>
                              (↑HSpace.hmul (p.fst.fst, p.snd.fst), ↑HSpace.hmul (p.fst.snd, p.snd.snd)))
                            (prodMk (ContinuousMap.id (G × G')) (const (G × G') (HSpace.e, HSpace.e))))
                        x ∧
                    ↑(ContinuousMap.mk fun x =>
                            ContinuousMap.toFun
                              {
                                  toContinuousMap :=
                                    ContinuousMap.mk fun p =>
                                      (↑HSpace.hmulE (p.fst, p.snd.fst), ↑HSpace.hmulE (p.fst, p.snd.snd)),
                                  map_zero_left :=
                                    (_ :
                                      ∀ (x : G × G'),
                                        ContinuousMap.toFun
                                            (ContinuousMap.mk fun p =>
                                              (↑HSpace.hmulE (p.fst, p.snd.fst), ↑HSpace.hmulE (p.fst, p.snd.snd)))
                                            (0, x) =
                                          ↑(comp
                                                (ContinuousMap.mk fun p =>
                                                  (↑HSpace.hmul (p.fst.fst, p.snd.fst),
                                                    ↑HSpace.hmul (p.fst.snd, p.snd.snd)))
                                                (prodMk (ContinuousMap.id (G × G'))
                                                  (const (G × G') (HSpace.e, HSpace.e))))
                                            x),
                                  map_one_left :=
                                    (_ :
                                      ∀ (x : G × G'),
                                        ContinuousMap.toFun
                                            (ContinuousMap.mk fun p =>
                                              (↑HSpace.hmulE (p.fst, p.snd.fst), ↑HSpace.hmulE (p.fst, p.snd.snd)))
                                            (1, x) =
                                          ↑(ContinuousMap.id (G × G')) x) }.toContinuousMap
                              (t, x))
                        x =
                      ↑(ContinuousMap.id (G × G')) x) } }
[PROOFSTEP]
rfl
[GOAL]
⊢ Continuous fun p => 2 * ↑p.fst
[PROOFSTEP]
continuity
[GOAL]
⊢ Continuous fun p => 1 + ↑p.snd
[PROOFSTEP]
continuity
[GOAL]
θ : ↑I
⊢ 2 * ↑(0, θ).fst / (1 + ↑(0, θ).snd) ≤ 0
[PROOFSTEP]
simp only [coe_zero, mul_zero, zero_div, le_refl]
[GOAL]
θ : ↑I
⊢ 1 * (1 + ↑(1, θ).snd) ≤ 2 * ↑(1, θ).fst
[PROOFSTEP]
dsimp only
[GOAL]
θ : ↑I
⊢ 1 * (1 + ↑θ) ≤ 2 * ↑1
[PROOFSTEP]
rw [coe_one, one_mul, mul_one, add_comm, ← one_add_one_eq_two]
[GOAL]
θ : ↑I
⊢ ↑θ + 1 ≤ 1 + 1
[PROOFSTEP]
simp only [add_le_add_iff_right]
[GOAL]
θ : ↑I
⊢ ↑θ ≤ 1
[PROOFSTEP]
exact le_one _
[GOAL]
t : ↑I
⊢ ↑(qRight (t, 0)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1
[PROOFSTEP]
simp only [qRight, coe_zero, add_zero, div_one]
[GOAL]
t : ↑I
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = 2 * ↑t
[PROOFSTEP]
rw [Set.projIcc_of_mem _ ((mul_pos_mem_iff zero_lt_two).2 _)]
[GOAL]
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ∈ Set.Icc 0 (1 / 2)
[PROOFSTEP]
refine' ⟨t.2.1, _⟩
[GOAL]
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ≤ 1 / 2
[PROOFSTEP]
tauto
[GOAL]
case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = 1
[PROOFSTEP]
rw [(Set.projIcc_eq_right _).2]
[GOAL]
case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 2 * ↑t
[PROOFSTEP]
linarith
[GOAL]
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
t : ↑I
⊢ qRight (t, 1) = Set.projIcc 0 1 (_ : 0 ≤ 1) ↑t
[PROOFSTEP]
rw [qRight]
[GOAL]
t : ↑I
⊢ Set.projIcc 0 1 qRight.proof_1 (2 * ↑(t, 1).fst / (1 + ↑(t, 1).snd)) = Set.projIcc 0 1 (_ : 0 ≤ 1) ↑t
[PROOFSTEP]
congr
[GOAL]
case e_x
t : ↑I
⊢ 2 * ↑(t, 1).fst / (1 + ↑(t, 1).snd) = ↑t
[PROOFSTEP]
norm_num
[GOAL]
case e_x
t : ↑I
⊢ 2 * ↑t / 2 = ↑t
[PROOFSTEP]
apply mul_div_cancel_left
[GOAL]
case e_x.ha
t : ↑I
⊢ 2 ≠ 0
[PROOFSTEP]
exact two_ne_zero
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ ContinuousMap.toFun (ContinuousMap.mk fun t => ↑γ (qRight (t, θ))) 0 = x
[PROOFSTEP]
dsimp only
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ ↑γ (qRight (0, θ)) = x
[PROOFSTEP]
rw [qRight_zero_left, γ.source]
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ ContinuousMap.toFun (ContinuousMap.mk fun t => ↑γ (qRight (t, θ))) 1 = y
[PROOFSTEP]
dsimp only
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ ↑γ (qRight (1, θ)) = y
[PROOFSTEP]
rw [qRight_one_left, γ.target]
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflRight 0 γ = trans γ (refl y)
[PROOFSTEP]
ext t
[GOAL]
case a.h
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ ↑(delayReflRight 0 γ) t = ↑(trans γ (refl y)) t
[PROOFSTEP]
simp only [delayReflRight, trans_apply, refl_extend, Path.coe_mk_mk, Function.comp_apply, refl_apply]
[GOAL]
case a.h
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ ↑γ (qRight (t, 0)) = if h : ↑t ≤ 1 / 2 then ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) } else y
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
case neg X : Type u inst✝ : TopologicalSpace X x y : X γ : Path x y t : ↑I h : ¬↑t ≤ 1 / 2 ⊢ ↑γ (qRight (t, 0)) = y
[PROOFSTEP]
swap
[GOAL]
case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = y
case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
[PROOFSTEP]
conv_rhs => rw [← γ.target]
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
| y
[PROOFSTEP]
rw [← γ.target]
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
| y
[PROOFSTEP]
rw [← γ.target]
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
| y
[PROOFSTEP]
rw [← γ.target]
[GOAL]
case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ 1
case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
[PROOFSTEP]
all_goals apply congr_arg γ; ext1; rw [qRight_zero_right]
[GOAL]
case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ 1
[PROOFSTEP]
apply congr_arg γ
[GOAL]
case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ qRight (t, 0) = 1
[PROOFSTEP]
ext1
[GOAL]
case neg.a
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑(qRight (t, 0)) = ↑1
[PROOFSTEP]
rw [qRight_zero_right]
[GOAL]
case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑γ (qRight (t, 0)) = ↑γ { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
[PROOFSTEP]
apply congr_arg γ
[GOAL]
case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ qRight (t, 0) = { val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
[PROOFSTEP]
ext1
[GOAL]
case pos.a
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑(qRight (t, 0)) = ↑{ val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
[PROOFSTEP]
rw [qRight_zero_right]
[GOAL]
case neg.a
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑1
case pos.a
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑{ val := 2 * ↑t, property := (_ : 2 * ↑t ∈ I) }
[PROOFSTEP]
exacts [if_neg h, if_pos h]
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflRight 1 γ = γ
[PROOFSTEP]
ext t
[GOAL]
case a.h
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ ↑(delayReflRight 1 γ) t = ↑γ t
[PROOFSTEP]
exact congr_arg γ (qRight_one_right t)
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflLeft 0 γ = trans (refl x) γ
[PROOFSTEP]
simp only [delayReflLeft, delayReflRight_zero, trans_symm, refl_symm, Path.symm_symm]
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflLeft 1 γ = γ
[PROOFSTEP]
simp only [delayReflLeft, delayReflRight_one, Path.symm_symm]
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
⊢ ∀ (t : ↑I) (x_1 : Path x x),
    x_1 ∈ {refl x} →
      ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  { toContinuousMap := ContinuousMap.mk fun p => delayReflLeft p.fst p.snd,
                      map_zero_left := (_ : ∀ (γ : Path x x), delayReflLeft 0 γ = trans (refl x) γ),
                      map_one_left := (_ : ∀ (γ : Path x x), delayReflLeft 1 γ = γ) }.toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(comp (ContinuousMap.mk fun ρ => trans ρ.fst ρ.snd)
                (prodMk (const (Path x x) (refl x)) (ContinuousMap.id (Path x x))))
            x_1 ∧
        ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  { toContinuousMap := ContinuousMap.mk fun p => delayReflLeft p.fst p.snd,
                      map_zero_left := (_ : ∀ (γ : Path x x), delayReflLeft 0 γ = trans (refl x) γ),
                      map_one_left := (_ : ∀ (γ : Path x x), delayReflLeft 1 γ = γ) }.toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(ContinuousMap.id (Path x x)) x_1
[PROOFSTEP]
rintro t _ (rfl : _ = _)
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
t : ↑I
⊢ ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk fun p => delayReflLeft p.fst p.snd,
                  map_zero_left := (_ : ∀ (γ : Path x x), delayReflLeft 0 γ = trans (refl x) γ),
                  map_one_left := (_ : ∀ (γ : Path x x), delayReflLeft 1 γ = γ) }.toContinuousMap
              (t, x_1))
        (refl x) =
      ↑(comp (ContinuousMap.mk fun ρ => trans ρ.fst ρ.snd)
            (prodMk (const (Path x x) (refl x)) (ContinuousMap.id (Path x x))))
        (refl x) ∧
    ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk fun p => delayReflLeft p.fst p.snd,
                  map_zero_left := (_ : ∀ (γ : Path x x), delayReflLeft 0 γ = trans (refl x) γ),
                  map_one_left := (_ : ∀ (γ : Path x x), delayReflLeft 1 γ = γ) }.toContinuousMap
              (t, x_1))
        (refl x) =
      ↑(ContinuousMap.id (Path x x)) (refl x)
[PROOFSTEP]
exact ⟨refl_trans_refl.symm, rfl⟩
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
⊢ ∀ (t : ↑I) (x_1 : Path x x),
    x_1 ∈ {refl x} →
      ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  { toContinuousMap := ContinuousMap.mk fun p => delayReflRight p.fst p.snd,
                      map_zero_left := (_ : ∀ (γ : Path x x), delayReflRight 0 γ = trans γ (refl x)),
                      map_one_left := (_ : ∀ (γ : Path x x), delayReflRight 1 γ = γ) }.toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(comp (ContinuousMap.mk fun ρ => trans ρ.fst ρ.snd)
                (prodMk (ContinuousMap.id (Path x x)) (const (Path x x) (refl x))))
            x_1 ∧
        ↑(ContinuousMap.mk fun x_2 =>
                ContinuousMap.toFun
                  { toContinuousMap := ContinuousMap.mk fun p => delayReflRight p.fst p.snd,
                      map_zero_left := (_ : ∀ (γ : Path x x), delayReflRight 0 γ = trans γ (refl x)),
                      map_one_left := (_ : ∀ (γ : Path x x), delayReflRight 1 γ = γ) }.toContinuousMap
                  (t, x_2))
            x_1 =
          ↑(ContinuousMap.id (Path x x)) x_1
[PROOFSTEP]
rintro t _ (rfl : _ = _)
[GOAL]
X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
t : ↑I
⊢ ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk fun p => delayReflRight p.fst p.snd,
                  map_zero_left := (_ : ∀ (γ : Path x x), delayReflRight 0 γ = trans γ (refl x)),
                  map_one_left := (_ : ∀ (γ : Path x x), delayReflRight 1 γ = γ) }.toContinuousMap
              (t, x_1))
        (refl x) =
      ↑(comp (ContinuousMap.mk fun ρ => trans ρ.fst ρ.snd)
            (prodMk (ContinuousMap.id (Path x x)) (const (Path x x) (refl x))))
        (refl x) ∧
    ↑(ContinuousMap.mk fun x_1 =>
            ContinuousMap.toFun
              { toContinuousMap := ContinuousMap.mk fun p => delayReflRight p.fst p.snd,
                  map_zero_left := (_ : ∀ (γ : Path x x), delayReflRight 0 γ = trans γ (refl x)),
                  map_one_left := (_ : ∀ (γ : Path x x), delayReflRight 1 γ = γ) }.toContinuousMap
              (t, x_1))
        (refl x) =
      ↑(ContinuousMap.id (Path x x)) (refl x)
[PROOFSTEP]
exact ⟨refl_trans_refl.symm, rfl⟩
