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


[GOAL]
⊢ Dense {x | Irrational x}
[PROOFSTEP]
refine' Real.isTopologicalBasis_Ioo_rat.dense_iff.2 _
[GOAL]
⊢ ∀ (o : Set ℝ), o ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b} → Set.Nonempty o → Set.Nonempty (o ∩ {x | Irrational x})
[PROOFSTEP]
simp only [gt_iff_lt, Rat.cast_lt, not_lt, ge_iff_le, Rat.cast_le, mem_iUnion, mem_singleton_iff, exists_prop,
  forall_exists_index, and_imp]
[GOAL]
⊢ ∀ (o : Set ℝ) (x x_1 : ℚ), x < x_1 → o = Ioo ↑x ↑x_1 → Set.Nonempty o → Set.Nonempty (o ∩ {x | Irrational x})
[PROOFSTEP]
rintro _ a b hlt rfl _
[GOAL]
a b : ℚ
hlt : a < b
a✝ : Set.Nonempty (Ioo ↑a ↑b)
⊢ Set.Nonempty (Ioo ↑a ↑b ∩ {x | Irrational x})
[PROOFSTEP]
rw [inter_comm]
[GOAL]
a b : ℚ
hlt : a < b
a✝ : Set.Nonempty (Ioo ↑a ↑b)
⊢ Set.Nonempty ({x | Irrational x} ∩ Ioo ↑a ↑b)
[PROOFSTEP]
exact exists_irrational_btwn (Rat.cast_lt.2 hlt)
[GOAL]
x✝¹ : ℝ
x✝ : { x // Irrational x }
x : ℝ
hx : Irrational x
⊢ { val := x, property := hx } < { val := x + ↑1, property := (_ : Irrational (x + ↑1)) }
[PROOFSTEP]
simp
[GOAL]
x✝¹ : ℝ
x✝ : { x // Irrational x }
x : ℝ
hx : Irrational x
⊢ { val := x - ↑1, property := (_ : Irrational (x - ↑1)) } < { val := x, property := hx }
[PROOFSTEP]
simp
[GOAL]
x : ℝ
hx : Irrational x
n : ℕ
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
[PROOFSTEP]
have A : IsClosed (range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ)) :=
  ((isClosedMap_smul₀ (n⁻¹ : ℝ)).comp Int.closedEmbedding_coe_real.isClosedMap).closed_range
[GOAL]
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
[PROOFSTEP]
have B : x ∉ range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ) :=
  by
  rintro ⟨m, rfl⟩
  simp at hx
[GOAL]
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
⊢ ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
[PROOFSTEP]
rintro ⟨m, rfl⟩
[GOAL]
case intro
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
m : ℤ
hx : Irrational ((fun m => (↑n)⁻¹ * ↑m) m)
⊢ False
[PROOFSTEP]
simp at hx
[GOAL]
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
B : ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
[PROOFSTEP]
rcases Metric.mem_nhds_iff.1 (A.isOpen_compl.mem_nhds B) with ⟨ε, ε0, hε⟩
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
B : ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
[PROOFSTEP]
refine' (ge_mem_nhds ε0).mono fun δ hδ m => not_lt.1 fun hlt => _
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
B : ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist x (↑m / ↑n) < δ
⊢ False
[PROOFSTEP]
rw [dist_comm] at hlt
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
B : ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist (↑m / ↑n) x < δ
⊢ False
[PROOFSTEP]
refine' hε (ball_subset_ball hδ hlt) ⟨m, _⟩
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
B : ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist (↑m / ↑n) x < δ
⊢ (fun m => (↑n)⁻¹ * ↑m) m = ↑m / ↑n
[PROOFSTEP]
simp [div_eq_inv_mul]
[GOAL]
x : ℝ
hx : Irrational x
n : ℕ
ε : ℝ
H : ∀ (k : ℕ), k ≤ n → ∀ (m : ℤ), ε ≤ dist x (↑m / ↑k)
r : ℚ
hr : r.den ≤ n
⊢ ε ≤ dist x ↑r
[PROOFSTEP]
simpa only [Rat.cast_def] using H r.den hr r.num


[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ OrdConnected (range Real.toEReal)
[PROOFSTEP]
rw [range_coe_eq_Ioo]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ OrdConnected (Ioo ⊥ ⊤)
[PROOFSTEP]
exact ordConnected_Ioo
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsOpen (range Real.toEReal)
[PROOFSTEP]
simp only [range_coe_eq_Ioo, isOpen_Ioo]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : EReal
ha : a ≠ ⊤
h'a : a ≠ ⊥
⊢ Tendsto toReal (𝓝 a) (𝓝 (toReal a))
[PROOFSTEP]
lift a to ℝ using ⟨ha, h'a⟩
[GOAL]
case intro
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto toReal (𝓝 ↑a) (𝓝 (toReal ↑a))
[PROOFSTEP]
rw [nhds_coe, tendsto_map'_iff]
[GOAL]
case intro
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (toReal ↑a))
[PROOFSTEP]
exact tendsto_id
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ OrdConnected (range ENNReal.toEReal)
[PROOFSTEP]
rw [range_coe_ennreal]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ OrdConnected (Ici 0)
[PROOFSTEP]
exact ordConnected_Ici
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsClosed (range ENNReal.toEReal)
[PROOFSTEP]
rw [range_coe_ennreal]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsClosed (Ici 0)
[PROOFSTEP]
exact isClosed_Ici
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ⨅ (l : EReal) (_ : l < ⊤), 𝓟 (Ioi l) = ⨅ (a : EReal) (_ : a ≠ ⊤), 𝓟 (Ioi a)
[PROOFSTEP]
simp only [lt_top_iff_ne_top]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ HasBasis (𝓝 ⊤) (fun x => True) fun x => Ioi ↑x
[PROOFSTEP]
refine nhds_top_basis.to_hasBasis (fun x hx => ?_) fun _ _ ↦ ⟨_, coe_lt_top _, Subset.rfl⟩
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
x : EReal
hx : x < ⊤
⊢ ∃ i', True ∧ Ioi ↑i' ⊆ Ioi x
[PROOFSTEP]
rcases exists_rat_btwn_of_lt hx with ⟨y, hxy, -⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
x : EReal
hx : x < ⊤
y : ℚ
hxy : x < ↑↑y
⊢ ∃ i', True ∧ Ioi ↑i' ⊆ Ioi x
[PROOFSTEP]
exact ⟨_, trivial, Ioi_subset_Ioi hxy.le⟩
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
s : Set EReal
⊢ (∃ i, True ∧ Ioi ↑i ⊆ s) ↔ ∃ y, Ioi ↑y ⊆ s
[PROOFSTEP]
simp only [true_and]
[GOAL]
α✝ : Type u_1
inst✝ : TopologicalSpace α✝
α : Type u_2
m : α → EReal
f : Filter α
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Ioi ↑i) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a
[PROOFSTEP]
simp only [true_implies, mem_Ioi]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ⨅ (l : EReal) (_ : ⊥ < l), 𝓟 (Iio l) = ⨅ (a : EReal) (_ : a ≠ ⊥), 𝓟 (Iio a)
[PROOFSTEP]
simp only [bot_lt_iff_ne_bot]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ HasBasis (𝓝 ⊥) (fun x => True) fun x => Iio ↑x
[PROOFSTEP]
refine nhds_bot_basis.to_hasBasis (fun x hx => ?_) fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
x : EReal
hx : ⊥ < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x
[PROOFSTEP]
rcases exists_rat_btwn_of_lt hx with ⟨y, -, hxy⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
x : EReal
hx : ⊥ < x
y : ℚ
hxy : ↑↑y < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x
[PROOFSTEP]
exact ⟨_, trivial, Iio_subset_Iio hxy.le⟩
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
s : Set EReal
⊢ (∃ i, True ∧ Iio ↑i ⊆ s) ↔ ∃ y, Iio ↑y ⊆ s
[PROOFSTEP]
simp only [true_and]
[GOAL]
α✝ : Type u_1
inst✝ : TopologicalSpace α✝
α : Type u_2
m : α → EReal
f : Filter α
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Iio ↑i) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x
[PROOFSTEP]
simp only [true_implies, mem_Iio]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a b : ℝ
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a, ↑b)
[PROOFSTEP]
simp only [ContinuousAt, nhds_coe_coe, ← coe_add, tendsto_map'_iff, (· ∘ ·), tendsto_coe, tendsto_add]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ↑a)
[PROOFSTEP]
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_coe]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.fst + a.snd
[PROOFSTEP]
refine fun r ↦
  ((lt_mem_nhds (coe_lt_top (r - (a - 1)))).prod_nhds (lt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| sub_one_lt _)).mono
    fun _ h ↦ ?_
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a r : ℝ
x✝ : EReal × EReal
h : ↑(r - (a - 1)) < x✝.fst ∧ ↑(a - 1) < x✝.snd
⊢ ↑r < x✝.fst + x✝.snd
[PROOFSTEP]
simpa only [← coe_add, sub_add_cancel] using add_lt_add h.1 h.2
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a, ⊤)
[PROOFSTEP]
simpa only [add_comm, (· ∘ ·), ContinuousAt, Prod.swap] using
  Tendsto.comp (continuousAt_add_top_coe a) (continuous_swap.tendsto ((a : EReal), ⊤))
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊤)
[PROOFSTEP]
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.fst + a.snd
[PROOFSTEP]
refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
r : ℝ
x✝ : EReal × EReal
h : ↑0 < x✝.fst ∧ ↑r < x✝.snd
⊢ ↑r < x✝.fst + x✝.snd
[PROOFSTEP]
simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ↑a)
[PROOFSTEP]
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ↑a), a.fst + a.snd < ↑x
[PROOFSTEP]
refine fun r ↦
  ((gt_mem_nhds (bot_lt_coe (r - (a + 1)))).prod_nhds (gt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| lt_add_one _)).mono
    fun _ h ↦ ?_
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a r : ℝ
x✝ : EReal × EReal
h : x✝.fst < ↑(r - (a + 1)) ∧ x✝.snd < ↑(a + 1)
⊢ x✝.fst + x✝.snd < ↑r
[PROOFSTEP]
simpa only [← coe_add, sub_add_cancel] using add_lt_add h.1 h.2
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
a : ℝ
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a, ⊥)
[PROOFSTEP]
simpa only [add_comm, (· ∘ ·), ContinuousAt, Prod.swap] using
  Tendsto.comp (continuousAt_add_bot_coe a) (continuous_swap.tendsto ((a : EReal), ⊥))
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊥)
[PROOFSTEP]
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.fst + a.snd < ↑x
[PROOFSTEP]
refine fun r ↦ ((gt_mem_nhds (bot_lt_coe 0)).prod_nhds (gt_mem_nhds <| bot_lt_coe r)).mono fun _ h ↦ ?_
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
r : ℝ
x✝ : EReal × EReal
h : x✝.fst < ↑0 ∧ x✝.snd < ↑r
⊢ x✝.fst + x✝.snd < ↑r
[PROOFSTEP]
simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2
[GOAL]
α : Type u_1
inst✝ : TopologicalSpace α
p : EReal × EReal
h : p.fst ≠ ⊤ ∨ p.snd ≠ ⊥
h' : p.fst ≠ ⊥ ∨ p.snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) p
[PROOFSTEP]
rcases p with ⟨x, y⟩
[GOAL]
case mk
α : Type u_1
inst✝ : TopologicalSpace α
x y : EReal
h : (x, y).fst ≠ ⊤ ∨ (x, y).snd ≠ ⊥
h' : (x, y).fst ≠ ⊥ ∨ (x, y).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (x, y)
[PROOFSTEP]
induction x using EReal.rec
[GOAL]
case mk.h_bot
α : Type u_1
inst✝ : TopologicalSpace α
y : EReal
h : (⊥, y).fst ≠ ⊤ ∨ (⊥, y).snd ≠ ⊥
h' : (⊥, y).fst ≠ ⊥ ∨ (⊥, y).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, y)
[PROOFSTEP]
induction y using EReal.rec
[GOAL]
case mk.h_real
α : Type u_1
inst✝ : TopologicalSpace α
y : EReal
a✝ : ℝ
h : (↑a✝, y).fst ≠ ⊤ ∨ (↑a✝, y).snd ≠ ⊥
h' : (↑a✝, y).fst ≠ ⊥ ∨ (↑a✝, y).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝, y)
[PROOFSTEP]
induction y using EReal.rec
[GOAL]
case mk.h_top
α : Type u_1
inst✝ : TopologicalSpace α
y : EReal
h : (⊤, y).fst ≠ ⊤ ∨ (⊤, y).snd ≠ ⊥
h' : (⊤, y).fst ≠ ⊥ ∨ (⊤, y).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, y)
[PROOFSTEP]
induction y using EReal.rec
[GOAL]
case mk.h_bot.h_bot
α : Type u_1
inst✝ : TopologicalSpace α
h : (⊥, ⊥).fst ≠ ⊤ ∨ (⊥, ⊥).snd ≠ ⊥
h' : (⊥, ⊥).fst ≠ ⊥ ∨ (⊥, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊥)
[PROOFSTEP]
exact continuousAt_add_bot_bot
[GOAL]
case mk.h_bot.h_real
α : Type u_1
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (⊥, ↑a✝).fst ≠ ⊤ ∨ (⊥, ↑a✝).snd ≠ ⊥
h' : (⊥, ↑a✝).fst ≠ ⊥ ∨ (⊥, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ↑a✝)
[PROOFSTEP]
exact continuousAt_add_bot_coe _
[GOAL]
case mk.h_bot.h_top
α : Type u_1
inst✝ : TopologicalSpace α
h : (⊥, ⊤).fst ≠ ⊤ ∨ (⊥, ⊤).snd ≠ ⊥
h' : (⊥, ⊤).fst ≠ ⊥ ∨ (⊥, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊤)
[PROOFSTEP]
simp at h'
[GOAL]
case mk.h_real.h_bot
α : Type u_1
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (↑a✝, ⊥).fst ≠ ⊤ ∨ (↑a✝, ⊥).snd ≠ ⊥
h' : (↑a✝, ⊥).fst ≠ ⊥ ∨ (↑a✝, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝, ⊥)
[PROOFSTEP]
exact continuousAt_add_coe_bot _
[GOAL]
case mk.h_real.h_real
α : Type u_1
inst✝ : TopologicalSpace α
a✝¹ a✝ : ℝ
h : (↑a✝¹, ↑a✝).fst ≠ ⊤ ∨ (↑a✝¹, ↑a✝).snd ≠ ⊥
h' : (↑a✝¹, ↑a✝).fst ≠ ⊥ ∨ (↑a✝¹, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝¹, ↑a✝)
[PROOFSTEP]
exact continuousAt_add_coe_coe _ _
[GOAL]
case mk.h_real.h_top
α : Type u_1
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (↑a✝, ⊤).fst ≠ ⊤ ∨ (↑a✝, ⊤).snd ≠ ⊥
h' : (↑a✝, ⊤).fst ≠ ⊥ ∨ (↑a✝, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝, ⊤)
[PROOFSTEP]
exact continuousAt_add_coe_top _
[GOAL]
case mk.h_top.h_bot
α : Type u_1
inst✝ : TopologicalSpace α
h : (⊤, ⊥).fst ≠ ⊤ ∨ (⊤, ⊥).snd ≠ ⊥
h' : (⊤, ⊥).fst ≠ ⊥ ∨ (⊤, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊥)
[PROOFSTEP]
simp at h
[GOAL]
case mk.h_top.h_real
α : Type u_1
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (⊤, ↑a✝).fst ≠ ⊤ ∨ (⊤, ↑a✝).snd ≠ ⊥
h' : (⊤, ↑a✝).fst ≠ ⊥ ∨ (⊤, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ↑a✝)
[PROOFSTEP]
exact continuousAt_add_top_coe _
[GOAL]
case mk.h_top.h_top
α : Type u_1
inst✝ : TopologicalSpace α
h : (⊤, ⊤).fst ≠ ⊤ ∨ (⊤, ⊤).snd ≠ ⊥
h' : (⊤, ⊤).fst ≠ ⊥ ∨ (⊤, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊤)
[PROOFSTEP]
exact continuousAt_add_top_top