[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c : R
⊢ ContinuousLinearMap.id R M = 1 • toContinuousLinearMap LinearIsometry.id
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c✝ : R
hf : IsConformalMap f
c : R
hc : c ≠ 0
⊢ IsConformalMap (c • f)
[PROOFSTEP]
rcases hf with ⟨c', hc', li, rfl⟩
[GOAL]
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
g : N →L[R] G
c✝ c : R
hc : c ≠ 0
c' : R
hc' : c' ≠ 0
li : M →ₗᵢ[R] N
⊢ IsConformalMap (c • c' • toContinuousLinearMap li)
[PROOFSTEP]
exact ⟨c * c', mul_ne_zero hc hc', li, smul_smul _ _ _⟩
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁹ : NormedField R
inst✝⁸ : SeminormedAddCommGroup M
inst✝⁷ : SeminormedAddCommGroup N
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : NormedSpace R M
inst✝⁴ : NormedSpace R N
inst✝³ : NormedSpace R G
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c : R
inst✝ : Subsingleton M
f' : M →L[R] N
x : M
⊢ ‖↑0 x‖ = ‖x‖
[PROOFSTEP]
simp [Subsingleton.elim x 0]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c : R
hg : IsConformalMap g
hf : IsConformalMap f
⊢ IsConformalMap (ContinuousLinearMap.comp g f)
[PROOFSTEP]
rcases hf with ⟨cf, hcf, lif, rfl⟩
[GOAL]
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
g : N →L[R] G
c : R
hg : IsConformalMap g
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
⊢ IsConformalMap (ContinuousLinearMap.comp g (cf • toContinuousLinearMap lif))
[PROOFSTEP]
rcases hg with ⟨cg, hcg, lig, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
c cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ IsConformalMap (ContinuousLinearMap.comp (cg • toContinuousLinearMap lig) (cf • toContinuousLinearMap lif))
[PROOFSTEP]
refine' ⟨cg * cf, mul_ne_zero hcg hcf, lig.comp lif, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
c cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ ContinuousLinearMap.comp (cg • toContinuousLinearMap lig) (cf • toContinuousLinearMap lif) =
    (cg * cf) • toContinuousLinearMap (LinearIsometry.comp lig lif)
[PROOFSTEP]
rw [smul_comp, comp_smul, mul_smul]
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
c cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ cg • cf • ContinuousLinearMap.comp (toContinuousLinearMap lig) (toContinuousLinearMap lif) =
    cg • cf • toContinuousLinearMap (LinearIsometry.comp lig lif)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
f✝ : M →L[R] N
g : N →L[R] G
c : R
f : M' →L[R] N
h : IsConformalMap f
⊢ Injective ↑f
[PROOFSTEP]
rcases h with ⟨c, hc, li, rfl⟩
[GOAL]
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c✝ c : R
hc : c ≠ 0
li : M' →ₗᵢ[R] N
⊢ Injective ↑(c • toContinuousLinearMap li)
[PROOFSTEP]
exact (smul_right_injective _ hc).comp li.injective
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁹ : NormedField R
inst✝⁸ : SeminormedAddCommGroup M
inst✝⁷ : SeminormedAddCommGroup N
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : NormedSpace R M
inst✝⁴ : NormedSpace R N
inst✝³ : NormedSpace R G
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c : R
inst✝ : Nontrivial M'
f' : M' →L[R] N
hf' : IsConformalMap f'
⊢ f' ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁹ : NormedField R
inst✝⁸ : SeminormedAddCommGroup M
inst✝⁷ : SeminormedAddCommGroup N
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : NormedSpace R M
inst✝⁴ : NormedSpace R N
inst✝³ : NormedSpace R G
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c : R
inst✝ : Nontrivial M'
hf' : IsConformalMap 0
⊢ False
[PROOFSTEP]
rcases exists_ne (0 : M') with ⟨a, ha⟩
[GOAL]
case intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
M' : Type u_5
inst✝⁹ : NormedField R
inst✝⁸ : SeminormedAddCommGroup M
inst✝⁷ : SeminormedAddCommGroup N
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : NormedSpace R M
inst✝⁴ : NormedSpace R N
inst✝³ : NormedSpace R G
inst✝² : NormedAddCommGroup M'
inst✝¹ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c : R
inst✝ : Nontrivial M'
hf' : IsConformalMap 0
a : M'
ha : a ≠ 0
⊢ False
[PROOFSTEP]
exact ha (hf'.injective rfl)


[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : NormedField α✝
inst✝² : SeminormedAddCommGroup β
α : Type u_5
inst✝¹ : NormedField α
inst✝ : NormedSpace α β
n : ℤ
x : β
⊢ ‖n • x‖ = ‖↑n‖ * ‖x‖
[PROOFSTEP]
rw [← norm_smul, ← Int.smul_one_eq_coe, smul_assoc, one_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : NormedField α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
x : β
⊢ ‖x‖⁻¹ • x ∈ closedBall 0 1
[PROOFSTEP]
simp only [mem_closedBall_zero_iff, norm_smul, norm_inv, norm_norm, ← _root_.div_eq_inv_mul, div_self_le_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : NormedField α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : NormedSpace ℝ β
t : ℝ
ht : 0 ≤ t
x : β
⊢ ‖t • x‖ = t * ‖x‖
[PROOFSTEP]
rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁵ : NormedField α
inst✝⁴ : SeminormedAddCommGroup β
E : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace α E
F : Type u_6
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace α F
c : α
x : E
ε : ℝ
h : 0 < ε
⊢ ‖c • (id x - x)‖ = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ closure (ball x r) = closedBall x r
[PROOFSTEP]
refine' Subset.antisymm closure_ball_subset_closedBall fun y hy => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
⊢ y ∈ closure (ball x r)
[PROOFSTEP]
have : ContinuousWithinAt (fun c : ℝ => c • (y - x) + x) (Ico 0 1) 1 :=
  ((continuous_id.smul continuous_const).add continuous_const).continuousWithinAt
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
⊢ y ∈ closure (ball x r)
[PROOFSTEP]
convert this.mem_closure _ _
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
⊢ y = 1 • (y - x) + x
[PROOFSTEP]
rw [one_smul, sub_add_cancel]
[GOAL]
case convert_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
⊢ 1 ∈ closure (Ico 0 1)
[PROOFSTEP]
simp [closure_Ico zero_ne_one, zero_le_one]
[GOAL]
case convert_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
⊢ MapsTo (fun c => c • (y - x) + x) (Ico 0 1) (ball x r)
[PROOFSTEP]
rintro c ⟨hc0, hc1⟩
[GOAL]
case convert_3.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ (fun c => c • (y - x) + x) c ∈ ball x r
[PROOFSTEP]
rw [mem_ball, dist_eq_norm, add_sub_cancel, norm_smul, Real.norm_eq_abs, abs_of_nonneg hc0, mul_comm, ← mul_one r]
[GOAL]
case convert_3.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖y - x‖ * c < r * 1
[PROOFSTEP]
rw [mem_closedBall, dist_eq_norm] at hy
[GOAL]
case convert_3.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖y - x‖ * c < r * 1
[PROOFSTEP]
replace hr : 0 < r := ((norm_nonneg _).trans hy).lt_of_ne hr.symm
[GOAL]
case convert_3.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ ‖y - x‖ * c < r * 1
[PROOFSTEP]
apply mul_lt_mul'
[GOAL]
case convert_3.intro.hac
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ ‖y - x‖ ≤ r
[PROOFSTEP]
assumption
[GOAL]
case convert_3.intro.hbd
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ c < 1
[PROOFSTEP]
assumption
[GOAL]
case convert_3.intro.hb
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ 0 ≤ c
[PROOFSTEP]
assumption
[GOAL]
case convert_3.intro.hc
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
y : E
hy : ‖y - x‖ ≤ r
this : ContinuousWithinAt (fun c => c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
hr : 0 < r
⊢ 0 < r
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (ball x r) = sphere x r
[PROOFSTEP]
rw [frontier, closure_ball x hr, isOpen_ball.interior_eq, closedBall_diff_ball]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r
[PROOFSTEP]
cases' hr.lt_or_lt with hr hr
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : r < 0
⊢ interior (closedBall x r) = ball x r
[PROOFSTEP]
rw [closedBall_eq_empty.2 hr, ball_eq_empty.2 hr.le, interior_empty]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) = ball x r
[PROOFSTEP]
refine' Subset.antisymm _ ball_subset_interior_closedBall
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) ⊆ ball x r
[PROOFSTEP]
intro y hy
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
⊢ y ∈ ball x r
[PROOFSTEP]
rcases(mem_closedBall.1 <| interior_subset hy).lt_or_eq with (hr | rfl)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝¹ : r ≠ 0
hr✝ : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
hr : dist y x < r
⊢ y ∈ ball x r
[PROOFSTEP]
exact hr
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
⊢ y ∈ ball x (dist y x)
[PROOFSTEP]
set f : ℝ → E := fun c : ℝ => c • (y - x) + x
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
⊢ y ∈ ball x (dist y x)
[PROOFSTEP]
suffices f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
  by
  have hfc : Continuous f := (continuous_id.smul continuous_const).add continuous_const
  have hf1 : (1 : ℝ) ∈ f ⁻¹' interior (closedBall x <| dist y x) := by simpa
  have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) :=
    interior_mono this (preimage_interior_subset_interior_preimage hfc hf1)
  contrapose h1
  simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
⊢ y ∈ ball x (dist y x)
[PROOFSTEP]
have hfc : Continuous f := (continuous_id.smul continuous_const).add continuous_const
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
⊢ y ∈ ball x (dist y x)
[PROOFSTEP]
have hf1 : (1 : ℝ) ∈ f ⁻¹' interior (closedBall x <| dist y x) := by simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
⊢ 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
hf1 : 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
⊢ y ∈ ball x (dist y x)
[PROOFSTEP]
have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) := interior_mono this (preimage_interior_subset_interior_preimage hfc hf1)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
hf1 : 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
h1 : 1 ∈ interior (Icc (-1) 1)
⊢ y ∈ ball x (dist y x)
[PROOFSTEP]
contrapose h1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
hf1 : 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
h1 : ¬y ∈ ball x (dist y x)
⊢ ¬1 ∈ interior (Icc (-1) 1)
[PROOFSTEP]
simp
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
⊢ f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
[PROOFSTEP]
intro c hc
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ c ∈ Icc (-1) 1
[PROOFSTEP]
rw [mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← mul_le_mul_right hr]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ ‖c‖ * dist y x ≤ 1 * dist y x
[PROOFSTEP]
simpa [dist_eq_norm, norm_smul] using hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (closedBall x r) = sphere x r
[PROOFSTEP]
rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (sphere x r) = ∅
[PROOFSTEP]
rw [← frontier_closedBall x hr, interior_frontier isClosed_ball]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_5
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type u_6
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (sphere x r) = sphere x r
[PROOFSTEP]
rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁷ : NormedField α
inst✝⁶ : SeminormedAddCommGroup β
E✝ : Type u_5
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : NormedSpace α E✝
F : Type u_6
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace α F
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples e }
[PROOFSTEP]
rcases eq_or_ne e 0 with (rfl | he)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁷ : NormedField α
inst✝⁶ : SeminormedAddCommGroup β
E✝ : Type u_5
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : NormedSpace α E✝
F : Type u_6
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace α F
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples 0 }
[PROOFSTEP]
rw [AddSubgroup.zmultiples_zero_eq_bot]
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁷ : NormedField α
inst✝⁶ : SeminormedAddCommGroup β
E✝ : Type u_5
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : NormedSpace α E✝
F : Type u_6
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace α F
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
⊢ DiscreteTopology { x // x ∈ ⊥ }
[PROOFSTEP]
refine Subsingleton.discreteTopology (α := ↑(⊥ : Subspace ℚ E))
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁷ : NormedField α
inst✝⁶ : SeminormedAddCommGroup β
E✝ : Type u_5
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : NormedSpace α E✝
F : Type u_6
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace α F
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
he : e ≠ 0
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples e }
[PROOFSTEP]
rw [discreteTopology_iff_open_singleton_zero, isOpen_induced_iff]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁷ : NormedField α
inst✝⁶ : SeminormedAddCommGroup β
E✝ : Type u_5
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : NormedSpace α E✝
F : Type u_6
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace α F
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
he : e ≠ 0
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = {0}
[PROOFSTEP]
refine' ⟨Metric.ball 0 ‖e‖, Metric.isOpen_ball, _⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁷ : NormedField α
inst✝⁶ : SeminormedAddCommGroup β
E✝ : Type u_5
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : NormedSpace α E✝
F : Type u_6
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace α F
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
he : e ≠ 0
⊢ Subtype.val ⁻¹' ball 0 ‖e‖ = {0}
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case inr.h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁷ : NormedField α
inst✝⁶ : SeminormedAddCommGroup β
E✝ : Type u_5
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : NormedSpace α E✝
F : Type u_6
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace α F
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
he : e ≠ 0
x : E
hx : x ∈ AddSubgroup.zmultiples e
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' ball 0 ‖e‖ ↔ { val := x, property := hx } ∈ {0}
[PROOFSTEP]
obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
[GOAL]
case inr.h.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁷ : NormedField α
inst✝⁶ : SeminormedAddCommGroup β
E✝ : Type u_5
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : NormedSpace α E✝
F : Type u_6
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace α F
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ { val := k • e, property := hx } ∈ Subtype.val ⁻¹' ball 0 ‖e‖ ↔ { val := k • e, property := hx } ∈ {0}
[PROOFSTEP]
rw [mem_preimage, mem_ball_zero_iff, AddSubgroup.coe_mk, mem_singleton_iff, Subtype.ext_iff, AddSubgroup.coe_mk,
  AddSubgroup.coe_zero, norm_zsmul ℚ k e, Int.norm_cast_rat, Int.norm_eq_abs,
  mul_lt_iff_lt_one_left (norm_pos_iff.mpr he), ← @Int.cast_one ℝ _, Int.cast_lt, Int.abs_lt_one_iff, smul_eq_zero,
  or_iff_left he]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁵ : NormedField α
inst✝⁴ : SeminormedAddCommGroup β
E : Type u_5
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace α E
F : Type u_6
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace α F
src✝¹ : SeminormedAddCommGroup (E × F) := seminormedAddCommGroup
src✝ : Module α (E × F) := instModule
s : α
x : E × F
⊢ ‖s • x‖ ≤ ‖s‖ * ‖x‖
[PROOFSTEP]
simp only [norm_smul, Prod.norm_def, Prod.smul_snd, Prod.smul_fst, mul_max_of_nonneg, norm_nonneg, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁸ : NormedField α
inst✝⁷ : SeminormedAddCommGroup β
E✝ : Type u_5
inst✝⁶ : SeminormedAddCommGroup E✝
inst✝⁵ : NormedSpace α E✝
F : Type u_6
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace α F
E : ι → Type u_7
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace α (E i)
a : α
f : (i : ι) → E i
⊢ ‖a • f‖ ≤ ‖a‖ * ‖f‖
[PROOFSTEP]
simp_rw [← coe_nnnorm, ← NNReal.coe_mul, NNReal.coe_le_coe, Pi.nnnorm_def, NNReal.mul_finset_sup]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁸ : NormedField α
inst✝⁷ : SeminormedAddCommGroup β
E✝ : Type u_5
inst✝⁶ : SeminormedAddCommGroup E✝
inst✝⁵ : NormedSpace α E✝
F : Type u_6
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace α F
E : ι → Type u_7
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace α (E i)
a : α
f : (i : ι) → E i
⊢ (Finset.sup Finset.univ fun b => ‖(a • f) b‖₊) ≤ Finset.sup Finset.univ fun a_1 => ‖a‖₊ * ‖f a_1‖₊
[PROOFSTEP]
exact Finset.sup_mono_fun fun _ _ => norm_smul_le a _
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
ι : Type u_4
F : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝⁵ : NormedField α
inst✝⁴ : AddCommGroup β
inst✝³ : Module α β
inst✝² : SeminormedAddCommGroup γ
inst✝¹ : NormedSpace α γ
inst✝ : LinearMapClass F α β γ
f : F
⊢ NormedSpace α β
[PROOFSTEP]
refine @NormedSpace.mk (α := α) (β := β) _ ?_ ?_ ?_
[GOAL]
case refine_1
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
ι : Type u_4
F : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝⁵ : NormedField α
inst✝⁴ : AddCommGroup β
inst✝³ : Module α β
inst✝² : SeminormedAddCommGroup γ
inst✝¹ : NormedSpace α γ
inst✝ : LinearMapClass F α β γ
f : F
⊢ Module α β
[PROOFSTEP]
infer_instance
[GOAL]
case refine_2
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
ι : Type u_4
F : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝⁵ : NormedField α
inst✝⁴ : AddCommGroup β
inst✝³ : Module α β
inst✝² : SeminormedAddCommGroup γ
inst✝¹ : NormedSpace α γ
inst✝ : LinearMapClass F α β γ
f : F
⊢ ∀ (a : α) (b : β), ‖a • b‖ ≤ ‖a‖ * ‖b‖
[PROOFSTEP]
intro a b
[GOAL]
case refine_2
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
ι : Type u_4
F : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝⁵ : NormedField α
inst✝⁴ : AddCommGroup β
inst✝³ : Module α β
inst✝² : SeminormedAddCommGroup γ
inst✝¹ : NormedSpace α γ
inst✝ : LinearMapClass F α β γ
f : F
a : α
b : β
⊢ ‖a • b‖ ≤ ‖a‖ * ‖b‖
[PROOFSTEP]
change ‖(⇑f) (a • b)‖ ≤ ‖a‖ * ‖(⇑f) b‖
[GOAL]
case refine_2
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
ι : Type u_4
F : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝⁵ : NormedField α
inst✝⁴ : AddCommGroup β
inst✝³ : Module α β
inst✝² : SeminormedAddCommGroup γ
inst✝¹ : NormedSpace α γ
inst✝ : LinearMapClass F α β γ
f : F
a : α
b : β
⊢ ‖↑f (a • b)‖ ≤ ‖a‖ * ‖↑f b‖
[PROOFSTEP]
exact (map_smul f a b).symm ▸ norm_smul_le a (f b)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type u_6
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
⊢ ∃ x, ‖x‖ = c
[PROOFSTEP]
rcases exists_ne (0 : E) with ⟨x, hx⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type u_6
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : x ≠ 0
⊢ ∃ x, ‖x‖ = c
[PROOFSTEP]
rw [← norm_ne_zero_iff] at hx
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type u_6
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ∃ x, ‖x‖ = c
[PROOFSTEP]
use c • ‖x‖⁻¹ • x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type u_6
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ‖c • ‖x‖⁻¹ • x‖ = c
[PROOFSTEP]
simp [norm_smul, Real.norm_of_nonneg hc, abs_of_nonneg hc, inv_mul_cancel hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type u_6
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (closedBall x r) = ball x r
[PROOFSTEP]
rcases eq_or_ne r 0 with (rfl | hr)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type u_6
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior (closedBall x 0) = ball x 0
[PROOFSTEP]
rw [closedBall_zero, ball_zero, interior_singleton]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type u_6
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r
[PROOFSTEP]
exact interior_closedBall x hr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type u_6
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ frontier (closedBall x r) = sphere x r
[PROOFSTEP]
rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_diff_ball]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type u_6
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (sphere x r) = ∅
[PROOFSTEP]
rw [← frontier_closedBall' x, interior_frontier isClosed_ball]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁶ : NormedField α
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace α E
F : Type u_6
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace α F
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ frontier (sphere x r) = sphere x r
[PROOFSTEP]
rw [isClosed_sphere.frontier_eq, interior_sphere' x, diff_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
⊢ ∃ x, c < ‖x‖
[PROOFSTEP]
rcases exists_ne (0 : E) with ⟨x, hx⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
⊢ ∃ x, c < ‖x‖
[PROOFSTEP]
rcases NormedField.exists_lt_norm 𝕜 (c / ‖x‖) with ⟨r, hr⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ ∃ x, c < ‖x‖
[PROOFSTEP]
use r • x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ c < ‖r • x‖
[PROOFSTEP]
rwa [norm_smul, ← _root_.div_lt_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ 0 < ‖x‖
[PROOFSTEP]
rwa [norm_pos_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
𝕜'✝ : Type u_6
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedRing 𝕜'✝
inst✝² : NormedAlgebra 𝕜 𝕜'✝
𝕜' : Type ?u.294395
inst✝¹ : NormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
⊢ NormedSpace 𝕜 𝕜'
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
𝕜' : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖↑(algebraMap 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
𝕜' : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖x • 1‖ = ‖x‖ * ‖1‖
[PROOFSTEP]
exact norm_smul _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
𝕜' : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x : 𝕜
⊢ ‖↑(algebraMap 𝕜 𝕜') x‖ = ‖x‖
[PROOFSTEP]
rw [norm_algebraMap, norm_one, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
𝕜' : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
⊢ Isometry ↑(algebraMap 𝕜 𝕜')
[PROOFSTEP]
refine' Isometry.of_dist_eq fun x y => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
𝕜' : Type u_6
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ dist (↑(algebraMap 𝕜 𝕜') x) (↑(algebraMap 𝕜 𝕜') y) = dist x y
[PROOFSTEP]
rw [dist_eq_norm, dist_eq_norm, ← RingHom.map_sub, norm_algebraMap']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜✝ : Type u_5
𝕜' : Type u_6
inst✝⁵ : NormedField 𝕜✝
inst✝⁴ : SeminormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜✝ 𝕜'
𝕜 : Type ?u.479633
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : NormedAlgebra ℝ 𝕜
q : ℚ
x : 𝕜
⊢ ‖q • x‖ ≤ ‖q‖ * ‖x‖
[PROOFSTEP]
rw [← smul_one_smul ℝ q x, Rat.smul_one_eq_coe, norm_smul, Rat.norm_cast_real]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
𝕜' : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
q : 𝕜
x✝ : PUnit
⊢ ‖q • x✝‖ ≤ ‖q‖ * ‖x✝‖
[PROOFSTEP]
simp only [norm_eq_zero, mul_zero, le_refl]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
ι : Type u_4
F : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝⁵ : NormedField α
inst✝⁴ : Ring β
inst✝³ : Algebra α β
inst✝² : SeminormedRing γ
inst✝¹ : NormedAlgebra α γ
inst✝ : NonUnitalAlgHomClass F α β γ
f : F
⊢ NormedAlgebra α β
[PROOFSTEP]
refine @NormedAlgebra.mk (𝕜 := α) (𝕜' := β) _ ?_ ?_ ?_
[GOAL]
case refine_1
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
ι : Type u_4
F : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝⁵ : NormedField α
inst✝⁴ : Ring β
inst✝³ : Algebra α β
inst✝² : SeminormedRing γ
inst✝¹ : NormedAlgebra α γ
inst✝ : NonUnitalAlgHomClass F α β γ
f : F
⊢ Algebra α β
[PROOFSTEP]
infer_instance
[GOAL]
case refine_2
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
ι : Type u_4
F : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝⁵ : NormedField α
inst✝⁴ : Ring β
inst✝³ : Algebra α β
inst✝² : SeminormedRing γ
inst✝¹ : NormedAlgebra α γ
inst✝ : NonUnitalAlgHomClass F α β γ
f : F
⊢ ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
[PROOFSTEP]
intro a b
[GOAL]
case refine_2
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
ι : Type u_4
F : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝⁵ : NormedField α
inst✝⁴ : Ring β
inst✝³ : Algebra α β
inst✝² : SeminormedRing γ
inst✝¹ : NormedAlgebra α γ
inst✝ : NonUnitalAlgHomClass F α β γ
f : F
a : α
b : β
⊢ ‖a • b‖ ≤ ‖a‖ * ‖b‖
[PROOFSTEP]
change ‖(⇑f) (a • b)‖ ≤ ‖a‖ * ‖(⇑f) b‖
[GOAL]
case refine_2
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
ι : Type u_4
F : Type u_5
α : Type u_6
β : Type u_7
γ : Type u_8
inst✝⁵ : NormedField α
inst✝⁴ : Ring β
inst✝³ : Algebra α β
inst✝² : SeminormedRing γ
inst✝¹ : NormedAlgebra α γ
inst✝ : NonUnitalAlgHomClass F α β γ
f : F
a : α
b : β
⊢ ‖↑f (a • b)‖ ≤ ‖a‖ * ‖↑f b‖
[PROOFSTEP]
exact (map_smul f a b).symm ▸ norm_smul_le a (f b)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
E : Type u_7
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜' E
src✝ : Module 𝕜 (RestrictScalars 𝕜 𝕜' E) := module 𝕜 𝕜' E
c : 𝕜
x : RestrictScalars 𝕜 𝕜' E
⊢ ‖↑(algebraMap 𝕜 𝕜') c‖ * ‖x‖ = ‖c‖ * ‖x‖
[PROOFSTEP]
rw [norm_algebraMap']


[GOAL]
𝕜 : 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_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F
x : E
⊢ ⊤ ≤ FormalMultilinearSeries.radius (fpowerSeries f x)
[PROOFSTEP]
simp
[GOAL]
𝕜 : 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_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F
x y✝ : E
x✝ : y✝ ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => ↑(fpowerSeries f x (n + 2)) fun x => y✝)
    (↑f (x + y✝) - ∑ i in Finset.range 2, ↑(fpowerSeries f x i) fun x => y✝)
[PROOFSTEP]
simp [Finset.sum_range_succ, ← sub_sub, hasSum_zero, fpowerSeries]
[GOAL]
𝕜 : 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_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E × F
⊢ ⊤ ≤ FormalMultilinearSeries.radius (fpowerSeriesBilinear f x)
[PROOFSTEP]
simp
[GOAL]
𝕜 : 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_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x y✝ : E × F
x✝ : y✝ ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => ↑(fpowerSeriesBilinear f x (n + 3)) fun x => y✝)
    (↑(↑f (x + y✝).fst) (x + y✝).snd - ∑ i in Finset.range 3, ↑(fpowerSeriesBilinear f x i) fun x => y✝)
[PROOFSTEP]
simp only [Finset.sum_range_succ, Finset.sum_range_one, Prod.fst_add, Prod.snd_add, f.map_add_add]
[GOAL]
𝕜 : 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_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x y✝ : E × F
x✝ : y✝ ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => ↑(fpowerSeriesBilinear f x (n + 3)) fun x => y✝)
    (↑(↑f x.fst) x.snd + ↑(↑(deriv₂ f) (x.fst, x.snd)) (y✝.fst, y✝.snd) + ↑(↑f y✝.fst) y✝.snd -
      ((((∑ x_1 in Finset.range 0, ↑(fpowerSeriesBilinear f x x_1) fun x => y✝) +
            ↑(fpowerSeriesBilinear f x 0) fun x => y✝) +
          ↑(fpowerSeriesBilinear f x 1) fun x => y✝) +
        ↑(fpowerSeriesBilinear f x 2) fun x => y✝))
[PROOFSTEP]
simp [fpowerSeriesBilinear, hasSum_zero]