[GOAL]
n : ℕ
inst✝ : Zero (Fin n)
x : EuclideanSpace ℝ (Fin n)
⊢ 0 ≤ update x 0 (max (x 0) 0) 0
[PROOFSTEP]
simp [le_refl]
[GOAL]
n : ℕ
inst✝ : Zero (Fin n)
x✝¹ : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval 0
x✝ : { val := xval, property := xprop } ∈ univ
⊢ (fun x => { val := update x 0 (max (x 0) 0), property := (_ : 0 ≤ update x 0 (max (x 0) 0) 0) })
      ↑{ val := xval, property := xprop } =
    { val := xval, property := xprop }
[PROOFSTEP]
rw [Subtype.mk_eq_mk, update_eq_iff]
[GOAL]
n : ℕ
inst✝ : Zero (Fin n)
x✝¹ : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval 0
x✝ : { val := xval, property := xprop } ∈ univ
⊢ max (↑{ val := xval, property := xprop } 0) 0 = xval 0 ∧
    ∀ (x : Fin n), x ≠ 0 → ↑{ val := xval, property := xprop } x = xval x
[PROOFSTEP]
exact ⟨max_eq_left xprop, fun i _ => rfl⟩
[GOAL]
n : ℕ
inst✝ : Zero (Fin n)
⊢ UniqueDiffOn ℝ
    { toFun := Subtype.val,
        invFun := fun x => { val := update x 0 (max (x 0) 0), property := (_ : 0 ≤ update x 0 (max (x 0) 0) 0) },
        source := univ, target := {x | 0 ≤ x 0}, map_source' := (_ : ∀ (x : EuclideanHalfSpace n), x ∈ univ → 0 ≤ ↑x 0),
        map_target' :=
          (_ :
            ∀ (x : EuclideanSpace ℝ (Fin n)),
              x ∈ {x | 0 ≤ x 0} →
                (fun x => { val := update x 0 (max (x 0) 0), property := (_ : 0 ≤ update x 0 (max (x 0) 0) 0) }) x ∈
                  univ),
        left_inv' :=
          (_ :
            ∀ (x : EuclideanHalfSpace n),
              x ∈ univ →
                (fun x => { val := update x 0 (max (x 0) 0), property := (_ : 0 ≤ update x 0 (max (x 0) 0) 0) }) ↑x =
                  x),
        right_inv' :=
          (_ : ∀ (x : EuclideanSpace ℝ (Fin n)), x ∈ {x | 0 ≤ x 0} → update (fun a => x a) 0 (max (x 0) 0) = x) }.target
[PROOFSTEP]
have : UniqueDiffOn ℝ _ :=
  UniqueDiffOn.pi (Fin n) (fun _ => ℝ) _ _ fun i (_ : i ∈ ({0} : Set (Fin n))) => uniqueDiffOn_Ici 0
[GOAL]
n : ℕ
inst✝ : Zero (Fin n)
this : UniqueDiffOn ℝ (pi {0} fun i => Ici 0)
⊢ UniqueDiffOn ℝ
    { toFun := Subtype.val,
        invFun := fun x => { val := update x 0 (max (x 0) 0), property := (_ : 0 ≤ update x 0 (max (x 0) 0) 0) },
        source := univ, target := {x | 0 ≤ x 0}, map_source' := (_ : ∀ (x : EuclideanHalfSpace n), x ∈ univ → 0 ≤ ↑x 0),
        map_target' :=
          (_ :
            ∀ (x : EuclideanSpace ℝ (Fin n)),
              x ∈ {x | 0 ≤ x 0} →
                (fun x => { val := update x 0 (max (x 0) 0), property := (_ : 0 ≤ update x 0 (max (x 0) 0) 0) }) x ∈
                  univ),
        left_inv' :=
          (_ :
            ∀ (x : EuclideanHalfSpace n),
              x ∈ univ →
                (fun x => { val := update x 0 (max (x 0) 0), property := (_ : 0 ≤ update x 0 (max (x 0) 0) 0) }) ↑x =
                  x),
        right_inv' :=
          (_ : ∀ (x : EuclideanSpace ℝ (Fin n)), x ∈ {x | 0 ≤ x 0} → update (fun a => x a) 0 (max (x 0) 0) = x) }.target
[PROOFSTEP]
simpa only [singleton_pi] using this
[GOAL]
n : ℕ
x : EuclideanSpace ℝ (Fin n)
i : Fin n
⊢ 0 ≤ (fun i => max (x i) 0) i
[PROOFSTEP]
simp only [le_refl, or_true_iff, le_max_iff]
[GOAL]
n : ℕ
x : EuclideanQuadrant n
x✝ : x ∈ univ
⊢ (fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) }) ↑x = x
[PROOFSTEP]
ext i
[GOAL]
case h.h
n : ℕ
x : EuclideanQuadrant n
x✝ : x ∈ univ
i : Fin n
⊢ ↑((fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) }) ↑x) i = ↑x i
[PROOFSTEP]
simp only [Subtype.coe_mk, x.2 i, max_eq_left]
[GOAL]
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : x ∈ {x | ∀ (i : Fin n), 0 ≤ x i}
⊢ ↑((fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) }) x) = x
[PROOFSTEP]
ext1 i
[GOAL]
case h
n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : x ∈ {x | ∀ (i : Fin n), 0 ≤ x i}
i : Fin n
⊢ ↑((fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) }) x) i = x i
[PROOFSTEP]
simp only [hx i, max_eq_left]
[GOAL]
n : ℕ
⊢ UniqueDiffOn ℝ
    { toFun := Subtype.val,
        invFun := fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) },
        source := univ, target := {x | ∀ (i : Fin n), 0 ≤ x i},
        map_source' := (_ : ∀ (x : EuclideanQuadrant n), x ∈ univ → ∀ (i : Fin n), 0 ≤ ↑x i),
        map_target' :=
          (_ :
            ∀ (x : EuclideanSpace ℝ (Fin n)),
              x ∈ {x | ∀ (i : Fin n), 0 ≤ x i} →
                (fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) }) x ∈ univ),
        left_inv' :=
          (_ :
            ∀ (x : EuclideanQuadrant n),
              x ∈ univ →
                (fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) }) ↑x = x),
        right_inv' :=
          (_ :
            ∀ (x : EuclideanSpace ℝ (Fin n)),
              x ∈ {x | ∀ (i : Fin n), 0 ≤ x i} →
                ↑((fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) }) x) =
                  x) }.target
[PROOFSTEP]
have this : UniqueDiffOn ℝ _ := UniqueDiffOn.univ_pi (Fin n) (fun _ => ℝ) _ fun _ => uniqueDiffOn_Ici 0
[GOAL]
n : ℕ
this : UniqueDiffOn ℝ (pi univ fun x => Ici 0)
⊢ UniqueDiffOn ℝ
    { toFun := Subtype.val,
        invFun := fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) },
        source := univ, target := {x | ∀ (i : Fin n), 0 ≤ x i},
        map_source' := (_ : ∀ (x : EuclideanQuadrant n), x ∈ univ → ∀ (i : Fin n), 0 ≤ ↑x i),
        map_target' :=
          (_ :
            ∀ (x : EuclideanSpace ℝ (Fin n)),
              x ∈ {x | ∀ (i : Fin n), 0 ≤ x i} →
                (fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) }) x ∈ univ),
        left_inv' :=
          (_ :
            ∀ (x : EuclideanQuadrant n),
              x ∈ univ →
                (fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) }) ↑x = x),
        right_inv' :=
          (_ :
            ∀ (x : EuclideanSpace ℝ (Fin n)),
              x ∈ {x | ∀ (i : Fin n), 0 ≤ x i} →
                ↑((fun x => { val := fun i => max (x i) 0, property := (_ : ∀ (i : Fin n), 0 ≤ max (x i) 0) }) x) =
                  x) }.target
[PROOFSTEP]
simpa only [pi_univ_Ici] using this
[GOAL]
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
⊢ min (↑z 0 + x) y ∈ Icc x y
[PROOFSTEP]
simp [le_refl, z.prop, le_of_lt h.out]
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : ↑(Icc x y)⦄,
    x_1 ∈ {z | ↑z < y} → (fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) x_1 ∈ {z | ↑z 0 < y - x}
[PROOFSTEP]
simp only [imp_self, sub_lt_sub_iff_right, mem_setOf_eq, forall_true_iff]
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
    x_1 ∈ {z | ↑z 0 < y - x} →
      (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1 ∈ {z | ↑z < y}
[PROOFSTEP]
simp only [min_lt_iff, mem_setOf_eq]
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : EuclideanHalfSpace 1⦄, ↑x_1 0 < y - x → ↑x_1 0 + x < y ∨ y < y
[PROOFSTEP]
intro z hz
[GOAL]
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
hz : ↑z 0 < y - x
⊢ ↑z 0 + x < y ∨ y < y
[PROOFSTEP]
left
[GOAL]
case h
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
hz : ↑z 0 < y - x
⊢ ↑z 0 + x < y
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : ↑(Icc x y)⦄,
    x_1 ∈ {z | ↑z < y} →
      (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
          ((fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) x_1) =
        x_1
[PROOFSTEP]
rintro ⟨z, hz⟩ h'z
[GOAL]
case mk
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
h'z : { val := z, property := hz } ∈ {z | ↑z < y}
⊢ (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
      ((fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) { val := z, property := hz }) =
    { val := z, property := hz }
[PROOFSTEP]
simp only [mem_setOf_eq, mem_Icc] at hz h'z 
[GOAL]
case mk
x y : ℝ
h : Fact (x < y)
z : ℝ
hz✝ : z ∈ Icc x y
h'z : z < y
hz : x ≤ z ∧ z ≤ y
⊢ (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
      ((fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) { val := z, property := hz✝ }) =
    { val := z, property := hz✝ }
[PROOFSTEP]
simp only [hz, min_eq_left, sub_add_cancel]
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
    x_1 ∈ {z | ↑z 0 < y - x} →
      (fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) })
          ((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1) =
        x_1
[PROOFSTEP]
rintro ⟨z, hz⟩ h'z
[GOAL]
case mk
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : { val := z, property := hz } ∈ {z | ↑z 0 < y - x}
⊢ (fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) })
      ((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
        { val := z, property := hz }) =
    { val := z, property := hz }
[PROOFSTEP]
rw [Subtype.mk_eq_mk]
[GOAL]
case mk
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : { val := z, property := hz } ∈ {z | ↑z 0 < y - x}
⊢ (fun x_1 =>
      ↑((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
            { val := z, property := hz }) -
        x) =
    z
[PROOFSTEP]
funext i
[GOAL]
case mk.h
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : { val := z, property := hz } ∈ {z | ↑z 0 < y - x}
i : Fin 1
⊢ ↑((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) { val := z, property := hz }) -
      x =
    z i
[PROOFSTEP]
dsimp at hz h'z 
[GOAL]
case mk.h
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : z 0 < y - x
i : Fin 1
⊢ ↑((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) { val := z, property := hz }) -
      x =
    z i
[PROOFSTEP]
have A : x + z 0 ≤ y := by linarith
[GOAL]
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : z 0 < y - x
i : Fin 1
⊢ x + z 0 ≤ y
[PROOFSTEP]
linarith
[GOAL]
case mk.h
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : z 0 < y - x
i : Fin 1
A : x + z 0 ≤ y
⊢ ↑((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) { val := z, property := hz }) -
      x =
    z i
[PROOFSTEP]
rw [Subsingleton.elim i 0]
[GOAL]
case mk.h
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : z 0 < y - x
i : Fin 1
A : x + z 0 ≤ y
⊢ ↑((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) { val := z, property := hz }) -
      x =
    z 0
[PROOFSTEP]
simp only [A, add_comm, add_sub_cancel', min_eq_left]
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ IsOpen
    { toFun := fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) },
        invFun := fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) },
        source := {z | ↑z < y}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), ↑a < y → ↑a - x < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1 ∈
                  {z | ↑z < y}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | ↑z < y} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) })
                    ((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1) =
                  x_1) }.target
[PROOFSTEP]
have : IsOpen {z : ℝ | z < y - x} := isOpen_Iio
[GOAL]
x y : ℝ
h : Fact (x < y)
this : IsOpen {z | z < y - x}
⊢ IsOpen
    { toFun := fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) },
        invFun := fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) },
        source := {z | ↑z < y}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), ↑a < y → ↑a - x < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1 ∈
                  {z | ↑z < y}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | ↑z < y} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) })
                    ((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1) =
                  x_1) }.target
[PROOFSTEP]
have : IsOpen {z : EuclideanSpace ℝ (Fin 1) | z 0 < y - x} := this.preimage (@continuous_apply (Fin 1) (fun _ => ℝ) _ 0)
[GOAL]
x y : ℝ
h : Fact (x < y)
this✝ : IsOpen {z | z < y - x}
this : IsOpen {z | z 0 < y - x}
⊢ IsOpen
    { toFun := fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) },
        invFun := fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) },
        source := {z | ↑z < y}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), ↑a < y → ↑a - x < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1 ∈
                  {z | ↑z < y}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | ↑z < y} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) })
                    ((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1) =
                  x_1) }.target
[PROOFSTEP]
exact this.preimage continuous_subtype_val
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ContinuousOn
    ↑{ toFun := fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) },
        invFun := fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) },
        source := {z | ↑z < y}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), ↑a < y → ↑a - x < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1 ∈
                  {z | ↑z < y}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | ↑z < y} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) })
                    ((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1) =
                  x_1) }
    { toFun := fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) },
        invFun := fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) },
        source := {z | ↑z < y}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), ↑a < y → ↑a - x < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1 ∈
                  {z | ↑z < y}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | ↑z < y} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) })
                    ((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1) =
                  x_1) }.source
[PROOFSTEP]
apply Continuous.continuousOn
[GOAL]
case h
x y : ℝ
h : Fact (x < y)
⊢ Continuous
    ↑{ toFun := fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) },
        invFun := fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) },
        source := {z | ↑z < y}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), ↑a < y → ↑a - x < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1 ∈
                  {z | ↑z < y}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | ↑z < y} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) })
                    ((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1) =
                  x_1) }
[PROOFSTEP]
apply Continuous.subtype_mk
[GOAL]
case h.h
x y : ℝ
h : Fact (x < y)
⊢ Continuous fun x_1 x_2 => ↑x_1 - x
[PROOFSTEP]
have : Continuous fun (z : ℝ) (_ : Fin 1) => z - x :=
  Continuous.sub (continuous_pi fun _ => continuous_id) continuous_const
[GOAL]
case h.h
x y : ℝ
h : Fact (x < y)
this : Continuous fun z x_1 => z - x
⊢ Continuous fun x_1 x_2 => ↑x_1 - x
[PROOFSTEP]
exact this.comp continuous_subtype_val
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ContinuousOn
    { toFun := fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) },
        invFun := fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) },
        source := {z | ↑z < y}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), ↑a < y → ↑a - x < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1 ∈
                  {z | ↑z < y}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | ↑z < y} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) })
                    ((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1) =
                  x_1) }.invFun
    { toFun := fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) },
        invFun := fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) },
        source := {z | ↑z < y}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), ↑a < y → ↑a - x < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1 ∈
                  {z | ↑z < y}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | ↑z < y} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) })
                    ((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1) =
                  x_1) }.target
[PROOFSTEP]
apply Continuous.continuousOn
[GOAL]
case h
x y : ℝ
h : Fact (x < y)
⊢ Continuous
    { toFun := fun z => { val := fun x_1 => ↑z - x, property := (_ : 0 ≤ ↑z - x) },
        invFun := fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) },
        source := {z | ↑z < y}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), ↑a < y → ↑a - x < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1 ∈
                  {z | ↑z < y}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | ↑z < y} →
                (fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => ↑z - x, property := (_ : 0 ≤ ↑z - x) })
                    ((fun z => { val := min (↑z 0 + x) y, property := (_ : min (↑z 0 + x) y ∈ Icc x y) }) x_1) =
                  x_1) }.invFun
[PROOFSTEP]
apply Continuous.subtype_mk
[GOAL]
case h.h
x y : ℝ
h : Fact (x < y)
⊢ Continuous fun x_1 => min (↑x_1 0 + x) y
[PROOFSTEP]
have A : Continuous fun z : ℝ => min (z + x) y := (continuous_id.add continuous_const).min continuous_const
[GOAL]
case h.h
x y : ℝ
h : Fact (x < y)
A : Continuous fun z => min (z + x) y
⊢ Continuous fun x_1 => min (↑x_1 0 + x) y
[PROOFSTEP]
have B : Continuous fun z : EuclideanSpace ℝ (Fin 1) => z 0 := continuous_apply 0
[GOAL]
case h.h
x y : ℝ
h : Fact (x < y)
A : Continuous fun z => min (z + x) y
B : Continuous fun z => z 0
⊢ Continuous fun x_1 => min (↑x_1 0 + x) y
[PROOFSTEP]
exact (A.comp B).comp continuous_subtype_val
[GOAL]
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
⊢ max (y - ↑z 0) x ∈ Icc x y
[PROOFSTEP]
simp [le_refl, z.prop, le_of_lt h.out, sub_eq_add_neg]
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : ↑(Icc x y)⦄,
    x_1 ∈ {z | x < ↑z} → (fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) x_1 ∈ {z | ↑z 0 < y - x}
[PROOFSTEP]
simp only [imp_self, mem_setOf_eq, sub_lt_sub_iff_left, forall_true_iff]
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
    x_1 ∈ {z | ↑z 0 < y - x} →
      (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1 ∈ {z | x < ↑z}
[PROOFSTEP]
simp only [lt_max_iff, mem_setOf_eq]
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : EuclideanHalfSpace 1⦄, ↑x_1 0 < y - x → x < y - ↑x_1 0 ∨ x < x
[PROOFSTEP]
intro z hz
[GOAL]
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
hz : ↑z 0 < y - x
⊢ x < y - ↑z 0 ∨ x < x
[PROOFSTEP]
left
[GOAL]
case h
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
hz : ↑z 0 < y - x
⊢ x < y - ↑z 0
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : ↑(Icc x y)⦄,
    x_1 ∈ {z | x < ↑z} →
      (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
          ((fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) x_1) =
        x_1
[PROOFSTEP]
rintro ⟨z, hz⟩ h'z
[GOAL]
case mk
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
h'z : { val := z, property := hz } ∈ {z | x < ↑z}
⊢ (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
      ((fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) { val := z, property := hz }) =
    { val := z, property := hz }
[PROOFSTEP]
simp only [mem_setOf_eq, mem_Icc] at hz h'z 
[GOAL]
case mk
x y : ℝ
h : Fact (x < y)
z : ℝ
hz✝ : z ∈ Icc x y
h'z : x < z
hz : x ≤ z ∧ z ≤ y
⊢ (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
      ((fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) { val := z, property := hz✝ }) =
    { val := z, property := hz✝ }
[PROOFSTEP]
simp only [hz, sub_eq_add_neg, max_eq_left, add_add_neg_cancel'_right, neg_add_rev, neg_neg]
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
    x_1 ∈ {z | ↑z 0 < y - x} →
      (fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) })
          ((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1) =
        x_1
[PROOFSTEP]
rintro ⟨z, hz⟩ h'z
[GOAL]
case mk
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : { val := z, property := hz } ∈ {z | ↑z 0 < y - x}
⊢ (fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) })
      ((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
        { val := z, property := hz }) =
    { val := z, property := hz }
[PROOFSTEP]
rw [Subtype.mk_eq_mk]
[GOAL]
case mk
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : { val := z, property := hz } ∈ {z | ↑z 0 < y - x}
⊢ (fun x_1 =>
      y -
        ↑((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
            { val := z, property := hz })) =
    z
[PROOFSTEP]
funext i
[GOAL]
case mk.h
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : { val := z, property := hz } ∈ {z | ↑z 0 < y - x}
i : Fin 1
⊢ y -
      ↑((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
          { val := z, property := hz }) =
    z i
[PROOFSTEP]
dsimp at hz h'z 
[GOAL]
case mk.h
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : z 0 < y - x
i : Fin 1
⊢ y -
      ↑((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
          { val := z, property := hz }) =
    z i
[PROOFSTEP]
have A : x ≤ y - z 0 := by linarith
[GOAL]
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : z 0 < y - x
i : Fin 1
⊢ x ≤ y - z 0
[PROOFSTEP]
linarith
[GOAL]
case mk.h
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : z 0 < y - x
i : Fin 1
A : x ≤ y - z 0
⊢ y -
      ↑((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
          { val := z, property := hz }) =
    z i
[PROOFSTEP]
rw [Subsingleton.elim i 0]
[GOAL]
case mk.h
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z 0
h'z : z 0 < y - x
i : Fin 1
A : x ≤ y - z 0
⊢ y -
      ↑((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
          { val := z, property := hz }) =
    z 0
[PROOFSTEP]
simp only [A, sub_sub_cancel, max_eq_left]
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ IsOpen
    { toFun := fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) },
        invFun := fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) },
        source := {z | x < ↑z}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), x < ↑a → y - ↑a < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1 ∈
                  {z | x < ↑z}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | x < ↑z} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) })
                    ((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1) =
                  x_1) }.target
[PROOFSTEP]
have : IsOpen {z : ℝ | z < y - x} := isOpen_Iio
[GOAL]
x y : ℝ
h : Fact (x < y)
this : IsOpen {z | z < y - x}
⊢ IsOpen
    { toFun := fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) },
        invFun := fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) },
        source := {z | x < ↑z}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), x < ↑a → y - ↑a < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1 ∈
                  {z | x < ↑z}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | x < ↑z} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) })
                    ((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1) =
                  x_1) }.target
[PROOFSTEP]
have : IsOpen {z : EuclideanSpace ℝ (Fin 1) | z 0 < y - x} := this.preimage (@continuous_apply (Fin 1) (fun _ => ℝ) _ 0)
[GOAL]
x y : ℝ
h : Fact (x < y)
this✝ : IsOpen {z | z < y - x}
this : IsOpen {z | z 0 < y - x}
⊢ IsOpen
    { toFun := fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) },
        invFun := fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) },
        source := {z | x < ↑z}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), x < ↑a → y - ↑a < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1 ∈
                  {z | x < ↑z}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | x < ↑z} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) })
                    ((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1) =
                  x_1) }.target
[PROOFSTEP]
exact this.preimage continuous_subtype_val
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ContinuousOn
    ↑{ toFun := fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) },
        invFun := fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) },
        source := {z | x < ↑z}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), x < ↑a → y - ↑a < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1 ∈
                  {z | x < ↑z}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | x < ↑z} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) })
                    ((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1) =
                  x_1) }
    { toFun := fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) },
        invFun := fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) },
        source := {z | x < ↑z}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), x < ↑a → y - ↑a < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1 ∈
                  {z | x < ↑z}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | x < ↑z} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) })
                    ((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1) =
                  x_1) }.source
[PROOFSTEP]
apply Continuous.continuousOn
[GOAL]
case h
x y : ℝ
h : Fact (x < y)
⊢ Continuous
    ↑{ toFun := fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) },
        invFun := fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) },
        source := {z | x < ↑z}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), x < ↑a → y - ↑a < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1 ∈
                  {z | x < ↑z}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | x < ↑z} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) })
                    ((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1) =
                  x_1) }
[PROOFSTEP]
apply Continuous.subtype_mk
[GOAL]
case h.h
x y : ℝ
h : Fact (x < y)
⊢ Continuous fun x_1 x_2 => y - ↑x_1
[PROOFSTEP]
have : Continuous fun (z : ℝ) (_ : Fin 1) => y - z := continuous_const.sub (continuous_pi fun _ => continuous_id)
[GOAL]
case h.h
x y : ℝ
h : Fact (x < y)
this : Continuous fun z x => y - z
⊢ Continuous fun x_1 x_2 => y - ↑x_1
[PROOFSTEP]
exact this.comp continuous_subtype_val
[GOAL]
x y : ℝ
h : Fact (x < y)
⊢ ContinuousOn
    { toFun := fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) },
        invFun := fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) },
        source := {z | x < ↑z}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), x < ↑a → y - ↑a < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1 ∈
                  {z | x < ↑z}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | x < ↑z} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) })
                    ((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1) =
                  x_1) }.invFun
    { toFun := fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) },
        invFun := fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) },
        source := {z | x < ↑z}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), x < ↑a → y - ↑a < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1 ∈
                  {z | x < ↑z}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | x < ↑z} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) })
                    ((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1) =
                  x_1) }.target
[PROOFSTEP]
apply Continuous.continuousOn
[GOAL]
case h
x y : ℝ
h : Fact (x < y)
⊢ Continuous
    { toFun := fun z => { val := fun x_1 => y - ↑z, property := (_ : 0 ≤ y - ↑z) },
        invFun := fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) },
        source := {z | x < ↑z}, target := {z | ↑z 0 < y - x},
        map_source' := (_ : ∀ (a : ↑(Icc x y)), x < ↑a → y - ↑a < y - x),
        map_target' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1 ∈
                  {z | x < ↑z}),
        left_inv' :=
          (_ :
            ∀ ⦃x_1 : ↑(Icc x y)⦄,
              x_1 ∈ {z | x < ↑z} →
                (fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) })
                    ((fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) }) x_1) =
                  x_1),
        right_inv' :=
          (_ :
            ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
              x_1 ∈ {z | ↑z 0 < y - x} →
                (fun z => { val := fun x_2 => y - ↑z, property := (_ : 0 ≤ y - ↑z) })
                    ((fun z => { val := max (y - ↑z 0) x, property := (_ : max (y - ↑z 0) x ∈ Icc x y) }) x_1) =
                  x_1) }.invFun
[PROOFSTEP]
apply Continuous.subtype_mk
[GOAL]
case h.h
x y : ℝ
h : Fact (x < y)
⊢ Continuous fun x_1 => max (y - ↑x_1 0) x
[PROOFSTEP]
have A : Continuous fun z : ℝ => max (y - z) x := (continuous_const.sub continuous_id).max continuous_const
[GOAL]
case h.h
x y : ℝ
h : Fact (x < y)
A : Continuous fun z => max (y - z) x
⊢ Continuous fun x_1 => max (y - ↑x_1 0) x
[PROOFSTEP]
have B : Continuous fun z : EuclideanSpace ℝ (Fin 1) => z 0 := continuous_apply 0
[GOAL]
case h.h
x y : ℝ
h : Fact (x < y)
A : Continuous fun z => max (y - z) x
B : Continuous fun z => z 0
⊢ Continuous fun x_1 => max (y - ↑x_1 0) x
[PROOFSTEP]
exact (A.comp B).comp continuous_subtype_val
[GOAL]
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
⊢ z ∈ ((fun z => if ↑z < y then IccLeftChart x y else IccRightChart x y) z).source
[PROOFSTEP]
by_cases h' : z.val < y
[GOAL]
case pos
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ↑z < y
⊢ z ∈ ((fun z => if ↑z < y then IccLeftChart x y else IccRightChart x y) z).source
[PROOFSTEP]
simp only [h', if_true]
[GOAL]
case pos
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ↑z < y
⊢ z ∈ (IccLeftChart x y).toLocalEquiv.source
[PROOFSTEP]
exact h'
[GOAL]
case neg
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ¬↑z < y
⊢ z ∈ ((fun z => if ↑z < y then IccLeftChart x y else IccRightChart x y) z).source
[PROOFSTEP]
simp only [h', if_false]
[GOAL]
case neg
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ¬↑z < y
⊢ z ∈ (IccRightChart x y).toLocalEquiv.source
[PROOFSTEP]
apply lt_of_lt_of_le h.out
[GOAL]
case neg
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ¬↑z < y
⊢ y ≤ ↑z
[PROOFSTEP]
simpa only [not_lt] using h'
[GOAL]
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
⊢ (fun z => if ↑z < y then IccLeftChart x y else IccRightChart x y) z ∈ {IccLeftChart x y, IccRightChart x y}
[PROOFSTEP]
by_cases h' : (z : ℝ) < y
[GOAL]
case pos
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ↑z < y
⊢ (fun z => if ↑z < y then IccLeftChart x y else IccRightChart x y) z ∈ {IccLeftChart x y, IccRightChart x y}
[PROOFSTEP]
simp [h']
[GOAL]
case neg
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ¬↑z < y
⊢ (fun z => if ↑z < y then IccLeftChart x y else IccRightChart x y) z ∈ {IccLeftChart x y, IccRightChart x y}
[PROOFSTEP]
simp [h']
[GOAL]
x y : ℝ
inst✝ : Fact (x < y)
⊢ SmoothManifoldWithCorners (modelWithCornersEuclideanHalfSpace 1) ↑(Icc x y)
[PROOFSTEP]
have M : ContDiff ℝ ∞ (show EuclideanSpace ℝ (Fin 1) → EuclideanSpace ℝ (Fin 1) from fun z i => -z i + (y - x)) :=
  contDiff_id.neg.add contDiff_const
[GOAL]
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
⊢ SmoothManifoldWithCorners (modelWithCornersEuclideanHalfSpace 1) ↑(Icc x y)
[PROOFSTEP]
apply smoothManifoldWithCorners_of_contDiffOn
[GOAL]
case h
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
⊢ ∀ (e e' : LocalHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)),
    e ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y) →
      e' ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y) →
        ContDiffOn ℝ ⊤
          (↑(modelWithCornersEuclideanHalfSpace 1) ∘
            ↑(LocalHomeomorph.symm e ≫ₕ e') ∘ ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
          (↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)) ⁻¹'
              (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source ∩
            range ↑(modelWithCornersEuclideanHalfSpace 1))
[PROOFSTEP]
intro e e' he he'
[GOAL]
case h
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
e e' : LocalHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)
he : e ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y)
he' : e' ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y)
⊢ ContDiffOn ℝ ⊤
    (↑(modelWithCornersEuclideanHalfSpace 1) ∘
      ↑(LocalHomeomorph.symm e ≫ₕ e') ∘ ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
    (↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)) ⁻¹'
        (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source ∩
      range ↑(modelWithCornersEuclideanHalfSpace 1))
[PROOFSTEP]
simp only [atlas, mem_singleton_iff, mem_insert_iff] at he he' 
[GOAL]
case h
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
e e' : LocalHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)
he : e ∈ ChartedSpace.atlas
he' : e' ∈ ChartedSpace.atlas
⊢ ContDiffOn ℝ ⊤
    (↑(modelWithCornersEuclideanHalfSpace 1) ∘
      ↑(LocalHomeomorph.symm e ≫ₕ e') ∘ ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
    (↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)) ⁻¹'
        (LocalHomeomorph.symm e ≫ₕ e').toLocalEquiv.source ∩
      range ↑(modelWithCornersEuclideanHalfSpace 1))
[PROOFSTEP]
rcases he with (rfl | rfl)
[GOAL]
case h.inl
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
e' : LocalHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)
he' : e' ∈ ChartedSpace.atlas
⊢ ContDiffOn ℝ ⊤
    (↑(modelWithCornersEuclideanHalfSpace 1) ∘
      ↑(LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ e') ∘
        ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
    (↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)) ⁻¹'
        (LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ e').toLocalEquiv.source ∩
      range ↑(modelWithCornersEuclideanHalfSpace 1))
[PROOFSTEP]
rcases he' with (rfl | rfl)
[GOAL]
case h.inr
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
e' : LocalHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)
he' : e' ∈ ChartedSpace.atlas
⊢ ContDiffOn ℝ ⊤
    (↑(modelWithCornersEuclideanHalfSpace 1) ∘
      ↑(LocalHomeomorph.symm (IccRightChart x y) ≫ₕ e') ∘
        ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
    (↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)) ⁻¹'
        (LocalHomeomorph.symm (IccRightChart x y) ≫ₕ e').toLocalEquiv.source ∩
      range ↑(modelWithCornersEuclideanHalfSpace 1))
[PROOFSTEP]
rcases he' with (rfl | rfl)
[GOAL]
case h.inl.inl
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
⊢ ContDiffOn ℝ ⊤
    (↑(modelWithCornersEuclideanHalfSpace 1) ∘
      ↑(LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ IccLeftChart x y) ∘
        ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
    (↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)) ⁻¹'
        (LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ IccLeftChart x y).toLocalEquiv.source ∩
      range ↑(modelWithCornersEuclideanHalfSpace 1))
[PROOFSTEP]
exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _ _ _)).1
[GOAL]
case h.inl.inr
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
⊢ ContDiffOn ℝ ⊤
    (↑(modelWithCornersEuclideanHalfSpace 1) ∘
      ↑(LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ IccRightChart x y) ∘
        ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
    (↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)) ⁻¹'
        (LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ IccRightChart x y).toLocalEquiv.source ∩
      range ↑(modelWithCornersEuclideanHalfSpace 1))
[PROOFSTEP]
apply M.contDiffOn.congr
[GOAL]
case h.inl.inr
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
⊢ ∀ (x_1 : EuclideanSpace ℝ (Fin 1)),
    x_1 ∈
        ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)) ⁻¹'
            (LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ IccRightChart x y).toLocalEquiv.source ∩
          range ↑(modelWithCornersEuclideanHalfSpace 1) →
      (↑(modelWithCornersEuclideanHalfSpace 1) ∘
            ↑(LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ IccRightChart x y) ∘
              ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
          x_1 =
        (fun this => this) (fun z i => -z i + (y - x)) x_1
[PROOFSTEP]
rintro _ ⟨⟨hz₁, hz₂⟩, ⟨⟨z, hz₀⟩, rfl⟩⟩
[GOAL]
case h.inl.inr.intro.intro.intro.mk
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ :
  ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) ∈
    (LocalHomeomorph.symm (LocalHomeomorph.symm (IccLeftChart x y))).toLocalEquiv.target
hz₂ :
  ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) ∈
    ↑(LocalHomeomorph.symm (LocalHomeomorph.symm (LocalHomeomorph.symm (IccLeftChart x y)))) ⁻¹'
      (IccRightChart x y).toLocalEquiv.source
⊢ (↑(modelWithCornersEuclideanHalfSpace 1) ∘
        ↑(LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ IccRightChart x y) ∘
          ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) =
    (fun this => this) (fun z i => -z i + (y - x))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ })
[PROOFSTEP]
simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, update_same, max_eq_left, hz₀,
  lt_sub_iff_add_lt, mfld_simps] at hz₁ hz₂ 
[GOAL]
case h.inl.inr.intro.intro.intro.mk
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : z 0 + x < y
hz₂ : x < min (z 0 + x) y
⊢ (↑(modelWithCornersEuclideanHalfSpace 1) ∘
        ↑(LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ IccRightChart x y) ∘
          ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) =
    (fun this => this) (fun z i => -z i + (y - x))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ })
[PROOFSTEP]
rw [min_eq_left hz₁.le, lt_add_iff_pos_left] at hz₂ 
[GOAL]
case h.inl.inr.intro.intro.intro.mk
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : z 0 + x < y
hz₂ : 0 < z 0
⊢ (↑(modelWithCornersEuclideanHalfSpace 1) ∘
        ↑(LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ IccRightChart x y) ∘
          ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) =
    (fun this => this) (fun z i => -z i + (y - x))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ })
[PROOFSTEP]
ext i
[GOAL]
case h.inl.inr.intro.intro.intro.mk.h
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : z 0 + x < y
hz₂ : 0 < z 0
i : Fin 1
⊢ (↑(modelWithCornersEuclideanHalfSpace 1) ∘
        ↑(LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ IccRightChart x y) ∘
          ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) i =
    (fun this => this) (fun z i => -z i + (y - x))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) i
[PROOFSTEP]
rw [Subsingleton.elim i 0]
[GOAL]
case h.inl.inr.intro.intro.intro.mk.h
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : z 0 + x < y
hz₂ : 0 < z 0
i : Fin 1
⊢ (↑(modelWithCornersEuclideanHalfSpace 1) ∘
        ↑(LocalHomeomorph.symm (IccLeftChart x y) ≫ₕ IccRightChart x y) ∘
          ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) 0 =
    (fun this => this) (fun z i => -z i + (y - x))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) 0
[PROOFSTEP]
simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, *, PiLp.add_apply, PiLp.neg_apply,
  max_eq_left, min_eq_left hz₁.le, update_same, mfld_simps]
[GOAL]
case h.inl.inr.intro.intro.intro.mk.h
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : z 0 + x < y
hz₂ : 0 < z 0
i : Fin 1
⊢ y - (z 0 + x) = -z 0 + (y - x)
[PROOFSTEP]
abel
[GOAL]
case h.inl.inr.intro.intro.intro.mk.h
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : z 0 + x < y
hz₂ : 0 < z 0
i : Fin 1
⊢ y - (z 0 + x) = -z 0 + (y - x)
[PROOFSTEP]
abel
[GOAL]
case h.inr.inl
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
⊢ ContDiffOn ℝ ⊤
    (↑(modelWithCornersEuclideanHalfSpace 1) ∘
      ↑(LocalHomeomorph.symm (IccRightChart x y) ≫ₕ IccLeftChart x y) ∘
        ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
    (↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)) ⁻¹'
        (LocalHomeomorph.symm (IccRightChart x y) ≫ₕ IccLeftChart x y).toLocalEquiv.source ∩
      range ↑(modelWithCornersEuclideanHalfSpace 1))
[PROOFSTEP]
apply M.contDiffOn.congr
[GOAL]
case h.inr.inl
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
⊢ ∀ (x_1 : EuclideanSpace ℝ (Fin 1)),
    x_1 ∈
        ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)) ⁻¹'
            (LocalHomeomorph.symm (IccRightChart x y) ≫ₕ IccLeftChart x y).toLocalEquiv.source ∩
          range ↑(modelWithCornersEuclideanHalfSpace 1) →
      (↑(modelWithCornersEuclideanHalfSpace 1) ∘
            ↑(LocalHomeomorph.symm (IccRightChart x y) ≫ₕ IccLeftChart x y) ∘
              ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
          x_1 =
        (fun this => this) (fun z i => -z i + (y - x)) x_1
[PROOFSTEP]
rintro _ ⟨⟨hz₁, hz₂⟩, ⟨z, hz₀⟩, rfl⟩
[GOAL]
case h.inr.inl.intro.intro.intro.mk
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ :
  ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) ∈
    (LocalHomeomorph.symm (LocalHomeomorph.symm (IccRightChart x y))).toLocalEquiv.target
hz₂ :
  ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) ∈
    ↑(LocalHomeomorph.symm (LocalHomeomorph.symm (LocalHomeomorph.symm (IccRightChart x y)))) ⁻¹'
      (IccLeftChart x y).toLocalEquiv.source
⊢ (↑(modelWithCornersEuclideanHalfSpace 1) ∘
        ↑(LocalHomeomorph.symm (IccRightChart x y) ≫ₕ IccLeftChart x y) ∘
          ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) =
    (fun this => this) (fun z i => -z i + (y - x))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ })
[PROOFSTEP]
simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, max_lt_iff, update_same, max_eq_left hz₀,
  mfld_simps] at hz₁ hz₂ 
[GOAL]
case h.inr.inl.intro.intro.intro.mk
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : z 0 < y - x
hz₂ : y - z 0 < y ∧ x < y
⊢ (↑(modelWithCornersEuclideanHalfSpace 1) ∘
        ↑(LocalHomeomorph.symm (IccRightChart x y) ≫ₕ IccLeftChart x y) ∘
          ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) =
    (fun this => this) (fun z i => -z i + (y - x))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ })
[PROOFSTEP]
rw [lt_sub_comm] at hz₁ 
[GOAL]
case h.inr.inl.intro.intro.intro.mk
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : x < y - z 0
hz₂ : y - z 0 < y ∧ x < y
⊢ (↑(modelWithCornersEuclideanHalfSpace 1) ∘
        ↑(LocalHomeomorph.symm (IccRightChart x y) ≫ₕ IccLeftChart x y) ∘
          ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) =
    (fun this => this) (fun z i => -z i + (y - x))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ })
[PROOFSTEP]
ext i
[GOAL]
case h.inr.inl.intro.intro.intro.mk.h
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : x < y - z 0
hz₂ : y - z 0 < y ∧ x < y
i : Fin 1
⊢ (↑(modelWithCornersEuclideanHalfSpace 1) ∘
        ↑(LocalHomeomorph.symm (IccRightChart x y) ≫ₕ IccLeftChart x y) ∘
          ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) i =
    (fun this => this) (fun z i => -z i + (y - x))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) i
[PROOFSTEP]
rw [Subsingleton.elim i 0]
[GOAL]
case h.inr.inl.intro.intro.intro.mk.h
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : x < y - z 0
hz₂ : y - z 0 < y ∧ x < y
i : Fin 1
⊢ (↑(modelWithCornersEuclideanHalfSpace 1) ∘
        ↑(LocalHomeomorph.symm (IccRightChart x y) ≫ₕ IccLeftChart x y) ∘
          ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) 0 =
    (fun this => this) (fun z i => -z i + (y - x))
      (↑(modelWithCornersEuclideanHalfSpace 1) { val := z, property := hz₀ }) 0
[PROOFSTEP]
simp only [modelWithCornersEuclideanHalfSpace, IccLeftChart, IccRightChart, PiLp.add_apply, PiLp.neg_apply, update_same,
  max_eq_left, hz₀, hz₁.le, mfld_simps]
[GOAL]
case h.inr.inl.intro.intro.intro.mk.h
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : x < y - z 0
hz₂ : y - z 0 < y ∧ x < y
i : Fin 1
⊢ y - z 0 - x = -z 0 + (y - x)
[PROOFSTEP]
abel
[GOAL]
case h.inr.inl.intro.intro.intro.mk.h
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z 0
hz₁ : x < y - z 0
hz₂ : y - z 0 < y ∧ x < y
i : Fin 1
⊢ y - z 0 - x = -z 0 + (y - x)
[PROOFSTEP]
abel
[GOAL]
case h.inr.inr
x y : ℝ
inst✝ : Fact (x < y)
M :
  ContDiff ℝ ⊤
    (let_fun this := fun z i => -z i + (y - x);
    this)
⊢ ContDiffOn ℝ ⊤
    (↑(modelWithCornersEuclideanHalfSpace 1) ∘
      ↑(LocalHomeomorph.symm (IccRightChart x y) ≫ₕ IccRightChart x y) ∘
        ↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)))
    (↑(ModelWithCorners.symm (modelWithCornersEuclideanHalfSpace 1)) ⁻¹'
        (LocalHomeomorph.symm (IccRightChart x y) ≫ₕ IccRightChart x y).toLocalEquiv.source ∩
      range ↑(modelWithCornersEuclideanHalfSpace 1))
[PROOFSTEP]
exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _ _ _)).1
[GOAL]
⊢ ChartedSpace (EuclideanHalfSpace 1) ↑(Icc 0 1)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ SmoothManifoldWithCorners (modelWithCornersEuclideanHalfSpace 1) ↑(Icc 0 1)
[PROOFSTEP]
infer_instance
