[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x : Unitization 𝕜 A
⊢ (fst x + 0, ↑↑(↑lift (NonUnitalAlgHom.Lmul 𝕜 A)) x) =
    (fst x, ↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x))
[PROOFSTEP]
rw [add_zero]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x : Unitization 𝕜 A
⊢ (fst x, ↑↑(↑lift (NonUnitalAlgHom.Lmul 𝕜 A)) x) = (fst x, ↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x))
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
⊢ Function.Injective ↑(splitMul 𝕜 A)
[PROOFSTEP]
rw [injective_iff_map_eq_zero]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
⊢ ∀ (a : Unitization 𝕜 A), ↑(splitMul 𝕜 A) a = 0 → a = 0
[PROOFSTEP]
intro x hx
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
x : Unitization 𝕜 A
hx : ↑(splitMul 𝕜 A) x = 0
⊢ x = 0
[PROOFSTEP]
induction x using Unitization.ind
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : ↑(splitMul 𝕜 A) (inl r✝ + ↑a✝) = 0
⊢ inl r✝ + ↑a✝ = 0
[PROOFSTEP]
rw [map_add] at hx
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : ↑(splitMul 𝕜 A) (inl r✝) + ↑(splitMul 𝕜 A) ↑a✝ = 0
⊢ inl r✝ + ↑a✝ = 0
[PROOFSTEP]
simp only [splitMul_apply, fst_inl, snd_inl, map_zero, add_zero, fst_inr, snd_inr, zero_add, Prod.mk_add_mk,
  Prod.mk_eq_zero] at hx
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : r✝ = 0 ∧ ↑(algebraMap 𝕜 (A →L[𝕜] A)) r✝ + ↑(mul 𝕜 A) a✝ = 0
⊢ inl r✝ + ↑a✝ = 0
[PROOFSTEP]
obtain ⟨rfl, hx⟩ := hx
[GOAL]
case h.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
a✝ : A
hx : ↑(algebraMap 𝕜 (A →L[𝕜] A)) 0 + ↑(mul 𝕜 A) a✝ = 0
⊢ inl 0 + ↑a✝ = 0
[PROOFSTEP]
simp only [map_zero, zero_add, inl_zero] at hx ⊢
[GOAL]
case h.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
a✝ : A
hx : ↑(mul 𝕜 A) a✝ = 0
⊢ ↑a✝ = 0
[PROOFSTEP]
rw [← map_zero (mul 𝕜 A)] at hx
[GOAL]
case h.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
a✝ : A
hx : ↑(mul 𝕜 A) a✝ = ↑(mul 𝕜 A) 0
⊢ ↑a✝ = 0
[PROOFSTEP]
rw [h hx, inr_zero]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖x‖ = ‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖
[PROOFSTEP]
rw [norm_def, splitMul_apply, Prod.norm_def, sup_eq_max]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ LipschitzWith 2 ↑(addEquiv 𝕜 A)
[PROOFSTEP]
rw [← Real.toNNReal_ofNat]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ LipschitzWith (Real.toNNReal 2) ↑(addEquiv 𝕜 A)
[PROOFSTEP]
refine AddMonoidHomClass.lipschitz_of_bound (Unitization.addEquiv 𝕜 A) 2 fun x => ?_
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖↑(addEquiv 𝕜 A) x‖ ≤ 2 * ‖x‖
[PROOFSTEP]
rw [norm_eq_sup, Prod.norm_def]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ max ‖(↑(addEquiv 𝕜 A) x).fst‖ ‖(↑(addEquiv 𝕜 A) x).snd‖ ≤
    2 * (‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖)
[PROOFSTEP]
refine' max_le ?_ ?_
[GOAL]
case refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖(↑(addEquiv 𝕜 A) x).fst‖ ≤ 2 * (‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖)
[PROOFSTEP]
rw [sup_eq_max, mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
[GOAL]
case refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖(↑(addEquiv 𝕜 A) x).fst‖ ≤ max (2 * ‖fst x‖) (2 * ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖)
[PROOFSTEP]
exact le_max_of_le_left ((le_add_of_nonneg_left (norm_nonneg _)).trans_eq (two_mul _).symm)
[GOAL]
case refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖(↑(addEquiv 𝕜 A) x).snd‖ ≤ 2 * (‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖)
[PROOFSTEP]
nontriviality A
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
✝ : Nontrivial A
⊢ ‖(↑(addEquiv 𝕜 A) x).snd‖ ≤ 2 * (‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖)
[PROOFSTEP]
rw [two_mul]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
✝ : Nontrivial A
⊢ ‖(↑(addEquiv 𝕜 A) x).snd‖ ≤
    ‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖ +
      ‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖
[PROOFSTEP]
calc
  ‖x.snd‖ = ‖mul 𝕜 A x.snd‖ := .symm <| (isometry_mul 𝕜 A).norm_map_of_map_zero (map_zero _) _
  _ ≤ ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ + ‖x.fst‖ := by
    simpa only [add_comm _ (mul 𝕜 A x.snd), norm_algebraMap'] using
      norm_le_add_norm_add (mul 𝕜 A x.snd) (algebraMap 𝕜 _ x.fst)
  _ ≤ _ := add_le_add le_sup_right le_sup_left
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
✝ : Nontrivial A
⊢ ‖↑(mul 𝕜 A) (snd x)‖ ≤ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖ + ‖fst x‖
[PROOFSTEP]
simpa only [add_comm _ (mul 𝕜 A x.snd), norm_algebraMap'] using
  norm_le_add_norm_add (mul 𝕜 A x.snd) (algebraMap 𝕜 _ x.fst)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ AntilipschitzWith 2 ↑(addEquiv 𝕜 A)
[PROOFSTEP]
refine AddMonoidHomClass.antilipschitz_of_bound (addEquiv 𝕜 A) fun x => ?_
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖x‖ ≤ ↑2 * ‖↑(addEquiv 𝕜 A) x‖
[PROOFSTEP]
rw [norm_eq_sup, Prod.norm_def, NNReal.coe_two]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖ ≤
    2 * max ‖(↑(addEquiv 𝕜 A) x).fst‖ ‖(↑(addEquiv 𝕜 A) x).snd‖
[PROOFSTEP]
refine max_le ?_ ?_
[GOAL]
case refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖fst x‖ ≤ 2 * max ‖(↑(addEquiv 𝕜 A) x).fst‖ ‖(↑(addEquiv 𝕜 A) x).snd‖
[PROOFSTEP]
rw [mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
[GOAL]
case refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖fst x‖ ≤ max (2 * ‖(↑(addEquiv 𝕜 A) x).fst‖) (2 * ‖(↑(addEquiv 𝕜 A) x).snd‖)
[PROOFSTEP]
exact le_max_of_le_left ((le_add_of_nonneg_left (norm_nonneg _)).trans_eq (two_mul _).symm)
[GOAL]
case refine_2
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖ ≤
    2 * max ‖(↑(addEquiv 𝕜 A) x).fst‖ ‖(↑(addEquiv 𝕜 A) x).snd‖
[PROOFSTEP]
nontriviality A
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
✝ : Nontrivial A
⊢ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖ ≤
    2 * max ‖(↑(addEquiv 𝕜 A) x).fst‖ ‖(↑(addEquiv 𝕜 A) x).snd‖
[PROOFSTEP]
calc
  ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ ≤ ‖algebraMap 𝕜 _ x.fst‖ + ‖mul 𝕜 A x.snd‖ := norm_add_le _ _
  _ = ‖x.fst‖ + ‖x.snd‖ := by
    rw [norm_algebraMap', (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 A)).mp (isometry_mul 𝕜 A)]
  _ ≤ _ := (add_le_add (le_max_left _ _) (le_max_right _ _)).trans_eq (two_mul _).symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
✝ : Nontrivial A
⊢ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x)‖ + ‖↑(mul 𝕜 A) (snd x)‖ = ‖fst x‖ + ‖snd x‖
[PROOFSTEP]
rw [norm_algebraMap', (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 A)).mp (isometry_mul 𝕜 A)]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ 𝓤 (Unitization 𝕜 A) = 𝓤 (Unitization 𝕜 A)
[PROOFSTEP]
have key : UniformInducing (addEquiv 𝕜 A) :=
  antilipschitzWith_addEquiv.uniformInducing lipschitzWith_addEquiv.uniformContinuous
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
key : UniformInducing ↑(addEquiv 𝕜 A)
⊢ 𝓤 (Unitization 𝕜 A) = 𝓤 (Unitization 𝕜 A)
[PROOFSTEP]
rw [← key.comap_uniformity]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
key : UniformInducing ↑(addEquiv 𝕜 A)
⊢ 𝓤 (Unitization 𝕜 A) = comap (fun x => (↑(addEquiv 𝕜 A) x.fst, ↑(addEquiv 𝕜 A) x.snd)) (𝓤 (𝕜 × A))
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
k : 𝕜
x : Unitization 𝕜 A
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖
[PROOFSTEP]
rw [norm_def, map_smul, norm_smul, ← norm_def]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ ‖1‖ = 1
[PROOFSTEP]
simpa only [norm_eq_sup, fst_one, norm_one, snd_one, map_one, map_zero, add_zero, ge_iff_le, sup_eq_left] using
  op_norm_le_bound _ zero_le_one fun x => by simp
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : A
⊢ ‖↑1 x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
a : A
⊢ ‖↑a‖ = ‖a‖
[PROOFSTEP]
simp [norm_eq_sup]


[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
⊢ (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1
[PROOFSTEP]
have : 0 < 1 + ‖x‖ ^ 2 := by positivity
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
⊢ 0 < 1 + ‖x‖ ^ 2
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
this : 0 < 1 + ‖x‖ ^ 2
⊢ (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1
[PROOFSTEP]
rw [mem_ball_zero_iff, norm_smul, Real.norm_eq_abs, abs_inv, ← _root_.div_eq_inv_mul,
  div_lt_one (abs_pos.mpr <| Real.sqrt_ne_zero'.mpr this), ← abs_norm x, ← sq_lt_sq, abs_norm, Real.sq_sqrt this.le]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
this : 0 < 1 + ‖x‖ ^ 2
⊢ ‖x‖ ^ 2 < 1 + ‖x‖ ^ 2
[PROOFSTEP]
exact lt_one_add _
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
⊢ (fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y) ((fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x) = x
[PROOFSTEP]
field_simp [norm_smul, smul_smul, (zero_lt_one_add_norm_sq x).ne', sq_abs, Real.sq_sqrt (zero_lt_one_add_norm_sq x).le,
  ← Real.sqrt_div (zero_lt_one_add_norm_sq x).le]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) ((fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y) y) = y
[PROOFSTEP]
have : 0 < 1 - ‖y‖ ^ 2 := by nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ 0 < 1 - ‖y‖ ^ 2
[PROOFSTEP]
nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
this : 0 < 1 - ‖y‖ ^ 2
⊢ (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) ((fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y) y) = y
[PROOFSTEP]
field_simp [norm_smul, smul_smul, this.ne', sq_abs, Real.sq_sqrt this.le, ← Real.sqrt_div this.le]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ContinuousOn
    ↑{ toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y = y) }
    { toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y =
                  y) }.source
[PROOFSTEP]
suffices Continuous fun (x : E) => (1 + ‖x‖ ^ 2).sqrt⁻¹ from (this.smul continuous_id).continuousOn
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Continuous fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹
[PROOFSTEP]
refine' Continuous.inv₀ _ fun x => Real.sqrt_ne_zero'.mpr (by positivity)
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ 0 < 1 + ‖x‖ ^ 2
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Continuous fun x => Real.sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
continuity
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ContinuousOn
    { toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y =
                  y) }.invFun
    { toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y =
                  y) }.target
[PROOFSTEP]
have : ∀ y ∈ ball (0 : E) 1, (1 - ‖(y : E)‖ ^ 2).sqrt ≠ 0 := fun y hy ↦
  by
  rw [Real.sqrt_ne_zero']
  nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ Real.sqrt (1 - ‖y‖ ^ 2) ≠ 0
[PROOFSTEP]
rw [Real.sqrt_ne_zero']
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ 0 < 1 - ‖y‖ ^ 2
[PROOFSTEP]
nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
this : ∀ (y : E), y ∈ ball 0 1 → Real.sqrt (1 - ‖y‖ ^ 2) ≠ 0
⊢ ContinuousOn
    { toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y =
                  y) }.invFun
    { toFun := fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y,
        source := univ, target := ball 0 1,
        map_source' := (_ : ∀ (x : E), x ∈ univ → (fun x => (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1),
        map_target' := (_ : ∀ (x : E), x ∈ ball 0 1 → True),
        left_inv' :=
          (_ :
            ∀ (x : E),
              x ∈ univ →
                (Real.sqrt (1 - ‖(Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (Real.sqrt (1 + ‖x‖ ^ 2))⁻¹ • x = x),
        right_inv' :=
          (_ :
            ∀ (y : E),
              y ∈ ball 0 1 →
                (Real.sqrt (1 + ‖(Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (Real.sqrt (1 - ‖y‖ ^ 2))⁻¹ • y =
                  y) }.target
[PROOFSTEP]
exact
  ContinuousOn.smul (ContinuousOn.inv₀ (continuousOn_const.sub (continuous_norm.continuousOn.pow _)).sqrt this)
    continuousOn_id
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ↑univUnitBall 0 = 0
[PROOFSTEP]
simp [LocalHomeomorph.univUnitBall_apply]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ↑(LocalHomeomorph.symm univUnitBall) 0 = 0
[PROOFSTEP]
simp [LocalHomeomorph.univUnitBall_symm_apply]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ↑(Homeomorph.trans (Homeomorph.smulOfNeZero r (_ : r ≠ 0))
          (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) ''
      ball 0 1 =
    ball c r
[PROOFSTEP]
change (IsometryEquiv.vaddConst c) ∘ (r • ·) '' ball (0 : E) 1 = ball c r
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (↑(IsometryEquiv.vaddConst c) ∘ fun x => r • x) '' ball 0 1 = ball c r
[PROOFSTEP]
rw [image_comp, image_smul, smul_unitBall hr.ne', IsometryEquiv.image_ball]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ball (↑(IsometryEquiv.vaddConst c) 0) ‖r‖ = ball c r
[PROOFSTEP]
simp [abs_of_pos hr]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (univBall c r).toLocalEquiv.source = univ
[PROOFSTEP]
unfold univBall
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (if h : 0 < r then
          LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
            (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)
        else
          Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))).toLocalEquiv.source =
    univ
[PROOFSTEP]
split_ifs
[GOAL]
case pos
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
h✝ : 0 < r
⊢ (LocalHomeomorph.trans' univUnitBall (unitBallBall c r h✝)
          (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)).toLocalEquiv.source =
    univ
[PROOFSTEP]
rfl
[GOAL]
case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
h✝ : ¬0 < r
⊢ (Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))).toLocalEquiv.source = univ
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (univBall c r).toLocalEquiv.target = ball c r
[PROOFSTEP]
rw [univBall, dif_pos hr]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (LocalHomeomorph.trans' univUnitBall (unitBallBall c r hr)
          (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)).toLocalEquiv.target =
    ball c r
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ball c r ⊆ (univBall c r).toLocalEquiv.target
[PROOFSTEP]
by_cases hr : 0 < r
[GOAL]
case pos
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ball c r ⊆ (univBall c r).toLocalEquiv.target
[PROOFSTEP]
rw [univBall_target c hr]
[GOAL]
case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆ (univBall c r).toLocalEquiv.target
[PROOFSTEP]
rw [univBall, dif_neg hr]
[GOAL]
case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆ (Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))).toLocalEquiv.target
[PROOFSTEP]
exact subset_univ _
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(univBall c r) 0 = c
[PROOFSTEP]
unfold univBall
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(if h : 0 < r then
          LocalHomeomorph.trans' univUnitBall (unitBallBall c r h)
            (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target)
        else Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))
      0 =
    c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
h✝ : 0 < r
⊢ ↑(LocalHomeomorph.trans' univUnitBall (unitBallBall c r h✝)
          (_ : univUnitBall.toLocalEquiv.target = univUnitBall.toLocalEquiv.target))
      0 =
    c
[PROOFSTEP]
simp
[GOAL]
case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
h✝ : ¬0 < r
⊢ ↑(Homeomorph.toLocalHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) 0 = c
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(LocalHomeomorph.symm (univBall c r)) c = 0
[PROOFSTEP]
have : 0 ∈ (univBall c r).source := by simp
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ 0 ∈ (univBall c r).toLocalEquiv.source
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
this : 0 ∈ (univBall c r).toLocalEquiv.source
⊢ ↑(LocalHomeomorph.symm (univBall c r)) c = 0
[PROOFSTEP]
simpa only [univBall_apply_zero] using (univBall c r).left_inv this
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ Continuous ↑(univBall c r)
[PROOFSTEP]
simpa [continuous_iff_continuousOn_univ] using (univBall c r).continuousOn