[GOAL]
𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
E : Type u_3
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
F : Type u_4
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace 𝕜 F
J : ModelWithCorners 𝕜 F F
G : Type u_5
inst✝¹³ : TopologicalSpace G
inst✝¹² : ChartedSpace H G
inst✝¹¹ : Group G
inst✝¹⁰ : LieGroup I G
E' : Type u_6
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H' M
E'' : Type u_9
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_10
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M' : Type u_11
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H'' M'
n : ℕ∞
f g : M → G
s : Set M
x₀ : M
hf : ContMDiffWithinAt I' I n f s x₀
hg : ContMDiffWithinAt I' I n g s x₀
⊢ ContMDiffWithinAt I' I n (fun x => f x / g x) s x₀
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
E : Type u_3
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
F : Type u_4
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace 𝕜 F
J : ModelWithCorners 𝕜 F F
G : Type u_5
inst✝¹³ : TopologicalSpace G
inst✝¹² : ChartedSpace H G
inst✝¹¹ : Group G
inst✝¹⁰ : LieGroup I G
E' : Type u_6
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H' M
E'' : Type u_9
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_10
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M' : Type u_11
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H'' M'
n : ℕ∞
f g : M → G
s : Set M
x₀ : M
hf : ContMDiffWithinAt I' I n f s x₀
hg : ContMDiffWithinAt I' I n g s x₀
⊢ ContMDiffWithinAt I' I n (fun x => f x * (g x)⁻¹) s x₀
[PROOFSTEP]
exact hf.mul hg.inv
[GOAL]
𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
E : Type u_3
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
F : Type u_4
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace 𝕜 F
J : ModelWithCorners 𝕜 F F
G : Type u_5
inst✝¹³ : TopologicalSpace G
inst✝¹² : ChartedSpace H G
inst✝¹¹ : Group G
inst✝¹⁰ : LieGroup I G
E' : Type u_6
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H' M
E'' : Type u_9
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_10
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M' : Type u_11
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H'' M'
n : ℕ∞
f g : M → G
x₀ : M
hf : ContMDiffAt I' I n f x₀
hg : ContMDiffAt I' I n g x₀
⊢ ContMDiffAt I' I n (fun x => f x / g x) x₀
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
E : Type u_3
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
F : Type u_4
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace 𝕜 F
J : ModelWithCorners 𝕜 F F
G : Type u_5
inst✝¹³ : TopologicalSpace G
inst✝¹² : ChartedSpace H G
inst✝¹¹ : Group G
inst✝¹⁰ : LieGroup I G
E' : Type u_6
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H' M
E'' : Type u_9
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_10
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M' : Type u_11
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H'' M'
n : ℕ∞
f g : M → G
x₀ : M
hf : ContMDiffAt I' I n f x₀
hg : ContMDiffAt I' I n g x₀
⊢ ContMDiffAt I' I n (fun x => f x * (g x)⁻¹) x₀
[PROOFSTEP]
exact hf.mul hg.inv
[GOAL]
𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
E : Type u_3
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
F : Type u_4
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace 𝕜 F
J : ModelWithCorners 𝕜 F F
G : Type u_5
inst✝¹³ : TopologicalSpace G
inst✝¹² : ChartedSpace H G
inst✝¹¹ : Group G
inst✝¹⁰ : LieGroup I G
E' : Type u_6
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H' M
E'' : Type u_9
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_10
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M' : Type u_11
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H'' M'
n : ℕ∞
f g : M → G
s : Set M
hf : ContMDiffOn I' I n f s
hg : ContMDiffOn I' I n g s
⊢ ContMDiffOn I' I n (fun x => f x / g x) s
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
E : Type u_3
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
F : Type u_4
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace 𝕜 F
J : ModelWithCorners 𝕜 F F
G : Type u_5
inst✝¹³ : TopologicalSpace G
inst✝¹² : ChartedSpace H G
inst✝¹¹ : Group G
inst✝¹⁰ : LieGroup I G
E' : Type u_6
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H' M
E'' : Type u_9
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_10
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M' : Type u_11
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H'' M'
n : ℕ∞
f g : M → G
s : Set M
hf : ContMDiffOn I' I n f s
hg : ContMDiffOn I' I n g s
⊢ ContMDiffOn I' I n (fun x => f x * (g x)⁻¹) s
[PROOFSTEP]
exact hf.mul hg.inv
[GOAL]
𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
E : Type u_3
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
F : Type u_4
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace 𝕜 F
J : ModelWithCorners 𝕜 F F
G : Type u_5
inst✝¹³ : TopologicalSpace G
inst✝¹² : ChartedSpace H G
inst✝¹¹ : Group G
inst✝¹⁰ : LieGroup I G
E' : Type u_6
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H' M
E'' : Type u_9
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_10
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M' : Type u_11
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H'' M'
n : ℕ∞
f g : M → G
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
⊢ ContMDiff I' I n fun x => f x / g x
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
𝕜 : Type u_1
inst✝¹⁹ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
E : Type u_3
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
F : Type u_4
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace 𝕜 F
J : ModelWithCorners 𝕜 F F
G : Type u_5
inst✝¹³ : TopologicalSpace G
inst✝¹² : ChartedSpace H G
inst✝¹¹ : Group G
inst✝¹⁰ : LieGroup I G
E' : Type u_6
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H' M
E'' : Type u_9
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_10
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M' : Type u_11
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H'' M'
n : ℕ∞
f g : M → G
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
⊢ ContMDiff I' I n fun x => f x * (g x)⁻¹
[PROOFSTEP]
exact hf.mul hg.inv
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
⊢ ∀ ⦃x : 𝕜⦄, x ≠ 0 → SmoothAt 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜) (fun y => y⁻¹) x
[PROOFSTEP]
intro x hx
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
hx : x ≠ 0
⊢ SmoothAt 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜) (fun y => y⁻¹) x
[PROOFSTEP]
change ContMDiffAt 𝓘(𝕜) 𝓘(𝕜) ⊤ Inv.inv x
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
hx : x ≠ 0
⊢ ContMDiffAt 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜) ⊤ Inv.inv x
[PROOFSTEP]
rw [contMDiffAt_iff_contDiffAt]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
x : 𝕜
hx : x ≠ 0
⊢ ContDiffAt 𝕜 ⊤ Inv.inv x
[PROOFSTEP]
exact contDiffAt_inv 𝕜 hx
[GOAL]
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : GroupWithZero G
inst✝⁶ : SmoothInv₀ I G
inst✝⁵ : SmoothMul I G
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f g : M → G
n : ℕ∞
s : Set M
a : M
hf : ContMDiffWithinAt I' I n f s a
hg : ContMDiffWithinAt I' I n g s a
h₀ : g a ≠ 0
⊢ ContMDiffWithinAt I' I n (f / g) s a
[PROOFSTEP]
simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
[GOAL]
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : GroupWithZero G
inst✝⁶ : SmoothInv₀ I G
inst✝⁵ : SmoothMul I G
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f g : M → G
n : ℕ∞
s : Set M
hf : ContMDiffOn I' I n f s
hg : ContMDiffOn I' I n g s
h₀ : ∀ (x : M), x ∈ s → g x ≠ 0
⊢ ContMDiffOn I' I n (f / g) s
[PROOFSTEP]
simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
[GOAL]
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : GroupWithZero G
inst✝⁶ : SmoothInv₀ I G
inst✝⁵ : SmoothMul I G
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f g : M → G
n : ℕ∞
a : M
hf : ContMDiffAt I' I n f a
hg : ContMDiffAt I' I n g a
h₀ : g a ≠ 0
⊢ ContMDiffAt I' I n (f / g) a
[PROOFSTEP]
simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
[GOAL]
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : GroupWithZero G
inst✝⁶ : SmoothInv₀ I G
inst✝⁵ : SmoothMul I G
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f g : M → G
n : ℕ∞
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
h₀ : ∀ (x : M), g x ≠ 0
⊢ ContMDiff I' I n (f / g)
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)


[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


[GOAL]
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (E x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : TopologicalSpace (TotalSpace F E)
inst✝¹⁵ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
⊢ ∀ (e e' : Trivialization F TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'],
    SmoothOn IB' 𝓘(𝕜, F →L[𝕜] F) (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)
[PROOFSTEP]
rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩
[GOAL]
case mk.intro.intro.mk.intro.intro
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (E x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : TopologicalSpace (TotalSpace F E)
inst✝¹⁵ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
⊢ SmoothOn IB' 𝓘(𝕜, F →L[𝕜] F)
    (fun b => ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b))
    ((Trivialization.pullback e f).baseSet ∩ (Trivialization.pullback e' f).baseSet)
[PROOFSTEP]
skip
[GOAL]
case mk.intro.intro.mk.intro.intro
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (E x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : TopologicalSpace (TotalSpace F E)
inst✝¹⁵ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
⊢ SmoothOn IB' 𝓘(𝕜, F →L[𝕜] F)
    (fun b => ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b))
    ((Trivialization.pullback e f).baseSet ∩ (Trivialization.pullback e' f).baseSet)
[PROOFSTEP]
refine' ((smoothOn_coordChangeL _ e e').comp f.smooth.smoothOn fun b hb => hb).congr _
[GOAL]
case mk.intro.intro.mk.intro.intro
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (E x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : TopologicalSpace (TotalSpace F E)
inst✝¹⁵ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
⊢ ∀ (y : B'),
    y ∈ ↑f ⁻¹' (e.baseSet ∩ e'.baseSet) →
      ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) y) =
        ((fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ↑f) y
[PROOFSTEP]
rintro b (hb : f b ∈ e.baseSet ∩ e'.baseSet)
[GOAL]
case mk.intro.intro.mk.intro.intro
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (E x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : TopologicalSpace (TotalSpace F E)
inst✝¹⁵ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
⊢ ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b) =
    ((fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ↑f) b
[PROOFSTEP]
ext v
[GOAL]
case mk.intro.intro.mk.intro.intro.h
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (E x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : TopologicalSpace (TotalSpace F E)
inst✝¹⁵ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ↑↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b) v =
    ↑(((fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ↑f) b) v
[PROOFSTEP]
show ((e.pullback f).coordChangeL 𝕜 (e'.pullback f) b) v = (e.coordChangeL 𝕜 e' (f b)) v
[GOAL]
case mk.intro.intro.mk.intro.intro.h
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (E x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : TopologicalSpace (TotalSpace F E)
inst✝¹⁵ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b) v =
    ↑(Trivialization.coordChangeL 𝕜 e e' (↑f b)) v
[PROOFSTEP]
rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]
[GOAL]
case mk.intro.intro.mk.intro.intro.h
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (E x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : TopologicalSpace (TotalSpace F E)
inst✝¹⁵ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (↑(Trivialization.pullback e' f)
        (↑(LocalHomeomorph.symm (Trivialization.pullback e f).toLocalHomeomorph) (b, v))).snd =
    (↑e' { proj := ↑f b, snd := Trivialization.symm e (↑f b) v }).snd
case mk.intro.intro.mk.intro.intro.h.hb
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
M : Type u_4
F : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : (x : B) → AddCommMonoid (E x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : TopologicalSpace (TotalSpace F E)
inst✝¹⁵ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : SmoothManifoldWithCorners IB B
EB' : Type u_9
inst✝⁸ : NormedAddCommGroup EB'
inst✝⁷ : NormedSpace 𝕜 EB'
HB' : Type u_10
inst✝⁶ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : ChartedSpace HB' B'
inst✝³ : SmoothManifoldWithCorners IB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : SmoothVectorBundle F E IB
f : SmoothMap IB' IB B' B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ b ∈ (Trivialization.pullback e f).baseSet ∩ (Trivialization.pullback e' f).baseSet
[PROOFSTEP]
exacts [rfl, hb]