𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
A : LocalEquiv E F := toLocalEquiv hf hc
⊢ ‖↑(LocalEquiv.symm A) x - ↑(LocalEquiv.symm A) y - ↑↑(ContinuousLinearEquiv.symm f') (x - y)‖ ≤
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
⊢ ‖↑(LocalEquiv.symm (toLocalEquiv hf hc)) x - ↑(LocalEquiv.symm (toLocalEquiv hf hc)) y -
        ↑↑(ContinuousLinearEquiv.symm f') (x - y)‖ ≤
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖
set A := hf.toLocalEquiv hc
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
⊢ ‖↑(LocalEquiv.symm A) x - ↑(LocalEquiv.symm A) y - ↑↑(ContinuousLinearEquiv.symm f') (x - y)‖ ≤
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
A : LocalEquiv E F := toLocalEquiv hf hc
⊢ ‖↑(LocalEquiv.symm A) x - ↑(LocalEquiv.symm A) y - ↑↑(ContinuousLinearEquiv.symm f') (x - y)‖ ≤
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖
have Af : ∀ z, A z = f z := fun z => rfl
case intro.intro
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
y : F
hy : y ∈ f '' s
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
⊢ ‖↑(LocalEquiv.symm A) (f x') - ↑(LocalEquiv.symm A) y - ↑↑(ContinuousLinearEquiv.symm f') (f x' - y)‖ ≤
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖f x' - y‖
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
⊢ ‖↑(LocalEquiv.symm A) x - ↑(LocalEquiv.symm A) y - ↑↑(ContinuousLinearEquiv.symm f') (x - y)‖ ≤
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖
rcases (mem_image _ _ _).1 hx with ⟨x', x's, rfl⟩
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖↑(LocalEquiv.symm A) (f x') - ↑(LocalEquiv.symm A) (f y') - ↑↑(ContinuousLinearEquiv.symm f') (f x' - f y')‖ ≤
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖f x' - f y'‖
case intro.intro
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
y : F
hy : y ∈ f '' s
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
⊢ ‖↑(LocalEquiv.symm A) (f x') - ↑(LocalEquiv.symm A) y - ↑↑(ContinuousLinearEquiv.symm f') (f x' - y)‖ ≤
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖f x' - y‖
rcases (mem_image _ _ _).1 hy with ⟨y', y's, rfl⟩
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖x' - y' - ↑↑(ContinuousLinearEquiv.symm f') (↑A x' - ↑A y')‖ ≤
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖↑A x' - ↑A y'‖
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖↑(LocalEquiv.symm A) (f x') - ↑(LocalEquiv.symm A) (f y') - ↑↑(ContinuousLinearEquiv.symm f') (f x' - f y')‖ ≤
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖f x' - f y'‖
rw [← Af x', ← Af y', A.left_inv x's, A.left_inv y's]
no goals
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖x' - y' - ↑↑(ContinuousLinearEquiv.symm f') (↑A x' - ↑A y')‖ ≤
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖↑A x' - ↑A y'‖
calc
  ‖x' - y' - f'.symm (A x' - A y')‖ ≤ N * ‖f' (x' - y' - f'.symm (A x' - A y'))‖ :=
    (f' : E →L[𝕜] F).bound_of_antilipschitz f'.antilipschitz _
  _ = N * ‖A y' - A x' - f' (y' - x')‖ := by
    congr 2
    simp only [ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearEquiv.map_sub]
    abel
  _ ≤ N * (c * ‖y' - x'‖) := (mul_le_mul_of_nonneg_left (hf _ y's _ x's) (NNReal.coe_nonneg _))
  _ ≤ N * (c * (((N⁻¹ - c)⁻¹ : ℝ≥0) * ‖A y' - A x'‖)) := by
    gcongr
    rw [← dist_eq_norm, ← dist_eq_norm]
    exact (hf.antilipschitz hc).le_mul_dist ⟨y', y's⟩ ⟨x', x's⟩
  _ = (N * (N⁻¹ - c)⁻¹ * c : ℝ≥0) * ‖A x' - A y'‖ := by
    simp only [norm_sub_rev, NNReal.coe_mul]; ring
case e_a.e_a
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑f' (x' - y' - ↑(ContinuousLinearEquiv.symm f') (↑A x' - ↑A y')) = ↑A y' - ↑A x' - ↑f' (y' - x')
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑(ContinuousLinearEquiv.symm f')‖₊ * ‖↑f' (x' - y' - ↑(ContinuousLinearEquiv.symm f') (↑A x' - ↑A y'))‖ =
    ↑‖↑(ContinuousLinearEquiv.symm f')‖₊ * ‖↑A y' - ↑A x' - ↑f' (y' - x')‖
congr 2
case e_a.e_a
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑f' x' - ↑f' y' - (↑(toLocalEquiv hf hc) x' - ↑(toLocalEquiv hf hc) y') =
    ↑(toLocalEquiv hf hc) y' - ↑(toLocalEquiv hf hc) x' - (↑f' y' - ↑f' x')
case e_a.e_a
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑f' (x' - y' - ↑(ContinuousLinearEquiv.symm f') (↑A x' - ↑A y')) = ↑A y' - ↑A x' - ↑f' (y' - x')
simp only [ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearEquiv.map_sub]
no goals
case e_a.e_a
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑f' x' - ↑f' y' - (↑(toLocalEquiv hf hc) x' - ↑(toLocalEquiv hf hc) y') =
    ↑(toLocalEquiv hf hc) y' - ↑(toLocalEquiv hf hc) x' - (↑f' y' - ↑f' x')
abel
case h.h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖y' - x'‖ ≤ ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * ‖↑A y' - ↑A x'‖
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑(ContinuousLinearEquiv.symm f')‖₊ * (↑c * ‖y' - x'‖) ≤
    ↑‖↑(ContinuousLinearEquiv.symm f')‖₊ * (↑c * (↑(‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * ‖↑A y' - ↑A x'‖))
gcongr
case h.h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ dist y' x' ≤ ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * dist (↑A y') (↑A x')
case h.h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖y' - x'‖ ≤ ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * ‖↑A y' - ↑A x'‖
rw [← dist_eq_norm, ← dist_eq_norm]
no goals
case h.h
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ dist y' x' ≤ ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * dist (↑A y') (↑A x')
exact (hf.antilipschitz hc).le_mul_dist ⟨y', y's⟩ ⟨x', x's⟩
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑(ContinuousLinearEquiv.symm f')‖₊ *
      (↑c * (↑(‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * ‖↑(toLocalEquiv hf hc) x' - ↑(toLocalEquiv hf hc) y'‖)) =
    ↑‖↑(ContinuousLinearEquiv.symm f')‖₊ * ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * ↑c *
      ‖↑(toLocalEquiv hf hc) x' - ↑(toLocalEquiv hf hc) y'‖
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑(ContinuousLinearEquiv.symm f')‖₊ * (↑c * (↑(‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * ‖↑A y' - ↑A x'‖)) =
    ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊ * (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * c) * ‖↑A x' - ↑A y'‖
simp only [norm_sub_rev, NNReal.coe_mul]
no goals
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.404204
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.404307
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
A : LocalEquiv E F := toLocalEquiv hf hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑(ContinuousLinearEquiv.symm f')‖₊ *
      (↑c * (↑(‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * ‖↑(toLocalEquiv hf hc) x' - ↑(toLocalEquiv hf hc) y'‖)) =
    ↑‖↑(ContinuousLinearEquiv.symm f')‖₊ * ↑(‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ * ↑c *
      ‖↑(toLocalEquiv hf hc) x' - ↑(toLocalEquiv hf hc) y'‖
ring