[GOAL]
α : Type u_1
inst✝² : NormedAddCommGroup α
inst✝¹ : Lattice α
inst✝ : HasSolidNorm α
x✝² x✝¹ : ℚ
x✝ : |x✝²| ≤ |x✝¹|
⊢ ‖x✝²‖ ≤ ‖x✝¹‖
[PROOFSTEP]
simpa only [norm, ← Rat.cast_abs, Rat.cast_le]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ ‖a‖ ≤ ‖b‖
[PROOFSTEP]
apply solid
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ |a| ≤ |b|
[PROOFSTEP]
rw [abs_eq_sup_neg]
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ a ⊔ -a ≤ |b|
[PROOFSTEP]
nth_rw 1 [← neg_neg a]
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ - -a ⊔ -a ≤ |b|
[PROOFSTEP]
rw [← neg_inf_eq_sup_neg]
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ |b|
[PROOFSTEP]
rw [abs_eq_sup_neg]
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ b ⊔ -b
[PROOFSTEP]
nth_rw 1 [← neg_neg b]
[GOAL]
case a
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ - -b ⊔ -b
[PROOFSTEP]
rwa [← neg_inf_eq_sup_neg, neg_le_neg_iff, @inf_comm _ _ _ b, @inf_comm _ _ _ a]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖
[PROOFSTEP]
rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊓ b - c ⊓ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
[PROOFSTEP]
refine' le_trans (solid _) (norm_add_le |a - c| |b - d|)
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ ||a - c| + |b - d||
[PROOFSTEP]
rw [abs_of_nonneg (|a - c| + |b - d|) (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
[PROOFSTEP]
calc
  |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)| := by rw [sub_add_sub_cancel]
  _ ≤ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| := (abs_add_le _ _)
  _ ≤ |a - c| + |b - d| := by
    apply add_le_add
    · exact abs_inf_sub_inf_le_abs _ _ _
    · rw [@inf_comm _ _ c, @inf_comm _ _ c]
      exact abs_inf_sub_inf_le_abs _ _ _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)|
[PROOFSTEP]
rw [sub_add_sub_cancel]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|
[PROOFSTEP]
apply add_le_add
[GOAL]
case h₁
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊓ b - c ⊓ b| ≤ |a - c|
[PROOFSTEP]
exact abs_inf_sub_inf_le_abs _ _ _
[GOAL]
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |c ⊓ b - c ⊓ d| ≤ |b - d|
[PROOFSTEP]
rw [@inf_comm _ _ c, @inf_comm _ _ c]
[GOAL]
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |b ⊓ c - d ⊓ c| ≤ |b - d|
[PROOFSTEP]
exact abs_inf_sub_inf_le_abs _ _ _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖
[PROOFSTEP]
rw [← norm_abs_eq_norm (a - c), ← norm_abs_eq_norm (b - d)]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ ‖a ⊔ b - c ⊔ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
[PROOFSTEP]
refine' le_trans (solid _) (norm_add_le |a - c| |b - d|)
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ ||a - c| + |b - d||
[PROOFSTEP]
rw [abs_of_nonneg (|a - c| + |b - d|) (add_nonneg (abs_nonneg (a - c)) (abs_nonneg (b - d)))]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
[PROOFSTEP]
calc
  |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)| := by rw [sub_add_sub_cancel]
  _ ≤ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| := (abs_add_le _ _)
  _ ≤ |a - c| + |b - d| := by
    apply add_le_add
    · exact abs_sup_sub_sup_le_abs _ _ _
    · rw [@sup_comm _ _ c, @sup_comm _ _ c]
      exact abs_sup_sub_sup_le_abs _ _ _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ d| = |a ⊔ b - c ⊔ b + (c ⊔ b - c ⊔ d)|
[PROOFSTEP]
rw [sub_add_sub_cancel]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| + |c ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
[PROOFSTEP]
apply add_le_add
[GOAL]
case h₁
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| ≤ |a - c|
[PROOFSTEP]
exact abs_sup_sub_sup_le_abs _ _ _
[GOAL]
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |c ⊔ b - c ⊔ d| ≤ |b - d|
[PROOFSTEP]
rw [@sup_comm _ _ c, @sup_comm _ _ c]
[GOAL]
case h₂
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
a b c d : α
⊢ |b ⊔ c - d ⊔ c| ≤ |b - d|
[PROOFSTEP]
exact abs_sup_sub_sup_le_abs _ _ _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
[PROOFSTEP]
have h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖ := norm_inf_sub_inf_le_add_norm x y 0 0
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
[PROOFSTEP]
simpa only [inf_idem, sub_zero] using h
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
[PROOFSTEP]
have h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖ := norm_sup_sub_sup_le_add_norm x y 0 0
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
[PROOFSTEP]
simpa only [sup_idem, sub_zero] using h
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
⊢ ContinuousInf α
[PROOFSTEP]
refine' ⟨continuous_iff_continuousAt.2 fun q => tendsto_iff_norm_tendsto_zero.2 <| _⟩
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
q : α × α
⊢ Filter.Tendsto (fun e => ‖e.fst ⊓ e.snd - (fun p => p.fst ⊓ p.snd) q‖) (nhds q) (nhds 0)
[PROOFSTEP]
have : ∀ p : α × α, ‖p.1 ⊓ p.2 - q.1 ⊓ q.2‖ ≤ ‖p.1 - q.1‖ + ‖p.2 - q.2‖ := fun _ => norm_inf_sub_inf_le_add_norm _ _ _ _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
q : α × α
this : ∀ (p : α × α), ‖p.fst ⊓ p.snd - q.fst ⊓ q.snd‖ ≤ ‖p.fst - q.fst‖ + ‖p.snd - q.snd‖
⊢ Filter.Tendsto (fun e => ‖e.fst ⊓ e.snd - (fun p => p.fst ⊓ p.snd) q‖) (nhds q) (nhds 0)
[PROOFSTEP]
refine' squeeze_zero (fun e => norm_nonneg _) this _
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
q : α × α
this : ∀ (p : α × α), ‖p.fst ⊓ p.snd - q.fst ⊓ q.snd‖ ≤ ‖p.fst - q.fst‖ + ‖p.snd - q.snd‖
⊢ Filter.Tendsto (fun t => ‖t.fst - q.fst‖ + ‖t.snd - q.snd‖) (nhds q) (nhds 0)
[PROOFSTEP]
convert
  ((continuous_fst.tendsto q).sub <| tendsto_const_nhds).norm.add
    ((continuous_snd.tendsto q).sub <| tendsto_const_nhds).norm
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
q : α × α
this : ∀ (p : α × α), ‖p.fst ⊓ p.snd - q.fst ⊓ q.snd‖ ≤ ‖p.fst - q.fst‖ + ‖p.snd - q.snd‖
⊢ 0 = ‖q.fst - q.fst‖ + ‖q.snd - q.snd‖
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
z x y : α
⊢ dist (x ⊔ z) (y ⊔ z) ≤ ↑1 * dist x y
[PROOFSTEP]
rw [NNReal.coe_one, one_mul, dist_eq_norm, dist_eq_norm]
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
z x y : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
[PROOFSTEP]
exact norm_sup_sub_sup_le_norm x y z
[GOAL]
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
⊢ Continuous NegPart.neg
[PROOFSTEP]
refine continuous_pos.comp <| @continuous_neg _ _ _ TopologicalAddGroup.toContinuousNeg
[GOAL]
α : Type u_1
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_2
inst✝ : NormedLatticeAddCommGroup E
⊢ IsClosed {x | 0 ≤ x}
[PROOFSTEP]
suffices {x : E | 0 ≤ x} = NegPart.neg ⁻¹' {(0 : E)} by
  rw [this]
  exact IsClosed.preimage continuous_neg' isClosed_singleton
[GOAL]
α : Type u_1
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_2
inst✝ : NormedLatticeAddCommGroup E
this : {x | 0 ≤ x} = NegPart.neg ⁻¹' {0}
⊢ IsClosed {x | 0 ≤ x}
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_2
inst✝ : NormedLatticeAddCommGroup E
this : {x | 0 ≤ x} = NegPart.neg ⁻¹' {0}
⊢ IsClosed (NegPart.neg ⁻¹' {0})
[PROOFSTEP]
exact IsClosed.preimage continuous_neg' isClosed_singleton
[GOAL]
α : Type u_1
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_2
inst✝ : NormedLatticeAddCommGroup E
⊢ {x | 0 ≤ x} = NegPart.neg ⁻¹' {0}
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
inst✝¹ : NormedLatticeAddCommGroup α
E : Type u_2
inst✝ : NormedLatticeAddCommGroup E
x : E
⊢ x ∈ {x | 0 ≤ x} ↔ x ∈ NegPart.neg ⁻¹' {0}
[PROOFSTEP]
simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_setOf_eq,
  @neg_eq_zero_iff E _ _ (OrderedAddCommGroup.to_covariantClass_left_le E)]
  -- porting note: I'm not sure why Lean couldn't synthesize this instance because it works with
    -- `have : CovariantClass E E (· + ·) (· ≤ ·) := inferInstance`
[GOAL]
α : Type u_1
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
⊢ IsClosed {p | p.fst ≤ p.snd}
[PROOFSTEP]
have : {p : G × G | p.fst ≤ p.snd} = (fun p : G × G => p.snd - p.fst) ⁻¹' {x : G | 0 ≤ x} := by ext1 p;
  simp only [sub_nonneg, Set.preimage_setOf_eq]
[GOAL]
α : Type u_1
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
⊢ {p | p.fst ≤ p.snd} = (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
[PROOFSTEP]
ext1 p
[GOAL]
case h
α : Type u_1
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
p : G × G
⊢ p ∈ {p | p.fst ≤ p.snd} ↔ p ∈ (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
[PROOFSTEP]
simp only [sub_nonneg, Set.preimage_setOf_eq]
[GOAL]
α : Type u_1
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.fst ≤ p.snd} = (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed {p | p.fst ≤ p.snd}
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
inst✝³ : NormedLatticeAddCommGroup α
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.fst ≤ p.snd} = (fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed ((fun p => p.snd - p.fst) ⁻¹' {x | 0 ≤ x})
[PROOFSTEP]
exact IsClosed.preimage (continuous_snd.sub continuous_fst) h


[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
⊢ (CauchySeq fun s => ∑ i in s, f i) ↔ ∀ (ε : ℝ), ε > 0 → ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
[PROOFSTEP]
rw [cauchySeq_finset_iff_vanishing, nhds_basis_ball.forall_iff]
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
⊢ (∀ (i : ℝ), 0 < i → ∃ s, ∀ (t : Finset ι), Disjoint t s → ∑ b in t, f b ∈ ball 0 i) ↔
    ∀ (ε : ℝ), ε > 0 → ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
[PROOFSTEP]
simp only [ball_zero_eq, Set.mem_setOf_eq]
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
⊢ ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      (∃ s_1, ∀ (t : Finset ι), Disjoint t s_1 → ∑ b in t, f b ∈ s) →
        ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b in t_1, f b ∈ t
[PROOFSTEP]
rintro s t hst ⟨s', hs'⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
s t : Set E
hst : s ⊆ t
s' : Finset ι
hs' : ∀ (t : Finset ι), Disjoint t s' → ∑ b in t, f b ∈ s
⊢ ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b in t_1, f b ∈ t
[PROOFSTEP]
exact ⟨s', fun t' ht' => hst <| hs' _ ht'⟩
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝² : SeminormedAddCommGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : CompleteSpace E
f : ι → E
⊢ Summable f ↔ ∀ (ε : ℝ), ε > 0 → ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
[PROOFSTEP]
rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_vanishing_norm]
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
⊢ CauchySeq fun s => ∑ i in s, f i
[PROOFSTEP]
refine' cauchySeq_finset_iff_vanishing_norm.2 fun ε hε => _
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
[PROOFSTEP]
rcases summable_iff_vanishing_norm.1 hg ε hε with ⟨s, hs⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
[PROOFSTEP]
refine' ⟨s ∪ h.toFinset, fun t ht => _⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
⊢ ‖∑ i in t, f i‖ < ε
[PROOFSTEP]
have : ∀ i ∈ t, ‖f i‖ ≤ g i := by
  intro i hi
  simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff, Classical.not_not] at ht
  exact (ht hi).2
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
⊢ ∀ (i : ι), i ∈ t → ‖f i‖ ≤ g i
[PROOFSTEP]
intro i hi
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
i : ι
hi : i ∈ t
⊢ ‖f i‖ ≤ g i
[PROOFSTEP]
simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff, Classical.not_not] at ht
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
i : ι
hi : i ∈ t
ht : ∀ ⦃a : ι⦄, a ∈ t → ¬a ∈ s ∧ a ∈ {x | ‖f x‖ ≤ g x}
⊢ ‖f i‖ ≤ g i
[PROOFSTEP]
exact (ht hi).2
[GOAL]
case intro
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
this : ∀ (i : ι), i ∈ t → ‖f i‖ ≤ g i
⊢ ‖∑ i in t, f i‖ < ε
[PROOFSTEP]
calc
  ‖∑ i in t, f i‖ ≤ ∑ i in t, g i := norm_sum_le_of_le _ this
  _ ≤ ‖∑ i in t, g i‖ := (le_abs_self _)
  _ < ε := hs _ (ht.mono_right le_sup_left)
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
⊢ CauchySeq fun n => ∑ i in range n, f i
[PROOFSTEP]
refine' Metric.cauchySeq_iff'.2 fun ε hε => _
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (∑ i in range n, f i) (∑ i in range N, f i) < ε
[PROOFSTEP]
refine' (Metric.cauchySeq_iff'.1 hg ε hε).imp fun N hg n hn => _
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N : ℕ
hg : ∀ (n : ℕ), n ≥ N → dist (∑ i in range n, g i) (∑ i in range N, g i) < ε
n : ℕ
hn : n ≥ N
⊢ dist (∑ i in range n, f i) (∑ i in range N, f i) < ε
[PROOFSTEP]
specialize hg n hn
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hg : dist (∑ i in range n, g i) (∑ i in range N, g i) < ε
⊢ dist (∑ i in range n, f i) (∑ i in range N, f i) < ε
[PROOFSTEP]
rw [dist_eq_norm, ← sum_Ico_eq_sub _ hn] at hg ⊢
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n => ∑ i in range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hg : ‖∑ k in Ico N n, g k‖ < ε
⊢ ‖∑ k in Ico N n, f k‖ < ε
[PROOFSTEP]
calc
  ‖∑ k in Ico N n, f k‖ ≤ ∑ k in _, ‖f k‖ := norm_sum_le _ _
  _ ≤ ∑ k in _, g k := (sum_le_sum fun x _ => hf x)
  _ ≤ ‖∑ k in _, g k‖ := (le_abs_self _)
  _ < ε := hg
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝² : SeminormedAddCommGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ Summable f
[PROOFSTEP]
rw [summable_iff_cauchySeq_finset]
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝² : SeminormedAddCommGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ CauchySeq fun s => ∑ b in s, f b
[PROOFSTEP]
exact cauchySeq_finset_of_norm_bounded g hg h
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ ‖∑' (i : ι), f i‖ ≤ a
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : Summable f
⊢ ‖∑' (i : ι), f i‖ ≤ a
[PROOFSTEP]
exact hf.hasSum.norm_le_of_bounded hg h
[GOAL]
case neg
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ ‖∑' (i : ι), f i‖ ≤ a
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, norm_zero]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ 0 ≤ a
[PROOFSTEP]
exact ge_of_tendsto' hg fun s => sum_nonneg fun i _hi => (norm_nonneg _).trans (h i)
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖₊ ≤ g i
⊢ ‖∑' (i : ι), f i‖₊ ≤ a
[PROOFSTEP]
simp only [← NNReal.coe_le_coe, ← NNReal.hasSum_coe, coe_nnnorm] at *
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum (fun a => ↑(g a)) ↑a
h : ∀ (i : ι), ‖f i‖ ≤ ↑(g i)
⊢ ‖∑' (i : ι), f i‖ ≤ ↑a
[PROOFSTEP]
exact tsum_of_norm_bounded hg h
[GOAL]
ι : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
inst✝² : SeminormedAddCommGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ≥0
hg : Summable g
h : ∀ (i : ι), ‖f i‖₊ ≤ g i
i : ι
⊢ ‖f i‖ ≤ (fun i => ↑(g i)) i
[PROOFSTEP]
exact_mod_cast h i


[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
c : V
x y : P
⊢ dist (c +ᵥ x) (c +ᵥ y) = dist x y
[PROOFSTEP]
rw [NormedAddTorsor.dist_eq_norm', NormedAddTorsor.dist_eq_norm', vadd_vsub_vadd_cancel_left]
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
v₁ v₂ : V
x : P
⊢ dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂
[PROOFSTEP]
rw [dist_eq_norm_vsub V, dist_eq_norm, vadd_vsub_vadd_cancel_right]
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
v : V
x : P
⊢ dist (v +ᵥ x) x = ‖v‖
[PROOFSTEP]
rw [dist_eq_norm_vsub V _ x, vadd_vsub]
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
v : V
x : P
⊢ dist x (v +ᵥ x) = ‖v‖
[PROOFSTEP]
rw [dist_comm, dist_vadd_left]
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
x y z : P
⊢ dist (x -ᵥ y) (x -ᵥ z) = dist y z
[PROOFSTEP]
rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
v v' : V
p p' : P
⊢ dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p'
[PROOFSTEP]
simpa [(dist_vadd_cancel_right)] using dist_triangle (v +ᵥ p) (v' +ᵥ p) (v' +ᵥ p')
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
p₁ p₂ p₃ p₄ : P
⊢ dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄
[PROOFSTEP]
rw [dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub V, dist_eq_norm_vsub V]
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)‖ ≤ ‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖
[PROOFSTEP]
exact norm_sub_le _ _
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
p₁ p₂ p₃ p₄ : P
⊢ nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄
[PROOFSTEP]
simp only [← NNReal.coe_le_coe, NNReal.coe_add, ← dist_nndist, (dist_vsub_vsub_le)]
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
v v' : V
p p' : P
⊢ edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'
[PROOFSTEP]
simp only [edist_nndist]
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
v v' : V
p p' : P
⊢ ↑(nndist (v +ᵥ p) (v' +ᵥ p')) ≤ ↑(nndist v v') + ↑(nndist p p')
[PROOFSTEP]
norm_cast
  -- porting note: was apply_mod_cast
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
v v' : V
p p' : P
⊢ nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'
[PROOFSTEP]
apply dist_vadd_vadd_le
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
p₁ p₂ p₃ p₄ : P
⊢ edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄
[PROOFSTEP]
simp only [edist_nndist]
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
p₁ p₂ p₃ p₄ : P
⊢ ↑(nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄)) ≤ ↑(nndist p₁ p₃) + ↑(nndist p₂ p₄)
[PROOFSTEP]
norm_cast
  -- porting note: was apply_mod_cast
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
p₁ p₂ p₃ p₄ : P
⊢ nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄
[PROOFSTEP]
apply dist_vsub_vsub_le
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : SeminormedAddCommGroup V
inst✝ : AddTorsor V P
x : P
⊢ dist x x = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : SeminormedAddCommGroup V
inst✝ : AddTorsor V P
x y : P
⊢ dist x y = dist y x
[PROOFSTEP]
simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : SeminormedAddCommGroup V
inst✝ : AddTorsor V P
x y z : P
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
change ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : SeminormedAddCommGroup V
inst✝ : AddTorsor V P
x y z : P
⊢ ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
[PROOFSTEP]
rw [← vsub_add_vsub_cancel]
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : SeminormedAddCommGroup V
inst✝ : AddTorsor V P
x y z : P
⊢ ‖x -ᵥ ?p2 + (?p2 -ᵥ z)‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
case p2
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : SeminormedAddCommGroup V
inst✝ : AddTorsor V P
x y z : P
⊢ P
[PROOFSTEP]
apply norm_add_le
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : SeminormedAddCommGroup V
inst✝ : AddTorsor V P
x✝¹ x✝ : P
⊢ (fun x y => ↑{ val := ‖x -ᵥ y‖, property := (_ : 0 ≤ ‖x -ᵥ y‖) }) x✝¹ x✝ = ENNReal.ofReal (dist x✝¹ x✝)
[PROOFSTEP]
simp only [← ENNReal.ofReal_eq_coe_nnreal]
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : NormedAddCommGroup V
inst✝ : AddTorsor V P
x : P
⊢ dist x x = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : NormedAddCommGroup V
inst✝ : AddTorsor V P
x y : P
⊢ dist x y = dist y x
[PROOFSTEP]
simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : NormedAddCommGroup V
inst✝ : AddTorsor V P
x y z : P
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
change ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : NormedAddCommGroup V
inst✝ : AddTorsor V P
x y z : P
⊢ ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
[PROOFSTEP]
rw [← vsub_add_vsub_cancel]
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : NormedAddCommGroup V
inst✝ : AddTorsor V P
x y z : P
⊢ ‖x -ᵥ ?p2 + (?p2 -ᵥ z)‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
case p2
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : NormedAddCommGroup V
inst✝ : AddTorsor V P
x y z : P
⊢ P
[PROOFSTEP]
apply norm_add_le
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : NormedAddCommGroup V
inst✝ : AddTorsor V P
x✝¹ x✝ : P
⊢ (fun x y => ↑{ val := ‖x -ᵥ y‖, property := (_ : 0 ≤ ‖x -ᵥ y‖) }) x✝¹ x✝ = ENNReal.ofReal (dist x✝¹ x✝)
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : NormedAddCommGroup V
inst✝ : AddTorsor V P
x✝¹ x✝ : P
⊢ ↑{ val := ‖x✝¹ -ᵥ x✝‖, property := (_ : 0 ≤ ‖x✝¹ -ᵥ x✝‖) } = ENNReal.ofReal ‖x✝¹ -ᵥ x✝‖
[PROOFSTEP]
rw [ENNReal.ofReal_eq_coe_nnreal]
[GOAL]
α : Type u_1
V✝ : Type u_2
P✝ : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁷ : SeminormedAddCommGroup V✝
inst✝⁶ : PseudoMetricSpace P✝
inst✝⁵ : NormedAddTorsor V✝ P✝
inst✝⁴ : NormedAddCommGroup W
inst✝³ : MetricSpace Q
inst✝² : NormedAddTorsor W Q
V : Type u_6
P : Type u_7
inst✝¹ : NormedAddCommGroup V
inst✝ : AddTorsor V P
x✝ y✝ : P
h : dist x✝ y✝ = 0
⊢ x✝ = y✝
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
⊢ IsClosed (s +ᵥ t)
[PROOFSTEP]
refine IsSeqClosed.isClosed (fun u p husv hup ↦ ?_)
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
husv : ∀ (n : ℕ), u n ∈ s +ᵥ t
hup : Tendsto u atTop (𝓝 p)
⊢ p ∈ s +ᵥ t
[PROOFSTEP]
choose! a v hav using husv
[GOAL]
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
v : ℕ → P
hav : ∀ (n : ℕ), a n ∈ s ∧ v n ∈ t ∧ (fun x x_1 => x +ᵥ x_1) (a n) (v n) = u n
⊢ p ∈ s +ᵥ t
[PROOFSTEP]
rcases ht.isSeqCompact fun n ↦ (hav n).2.1 with ⟨q, hqt, φ, φ_mono, hφq⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
v : ℕ → P
hav : ∀ (n : ℕ), a n ∈ s ∧ v n ∈ t ∧ (fun x x_1 => x +ᵥ x_1) (a n) (v n) = u n
q : P
hqt : q ∈ t
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφq : Tendsto ((fun n => v n) ∘ φ) atTop (𝓝 q)
⊢ p ∈ s +ᵥ t
[PROOFSTEP]
refine
  ⟨p -ᵥ q, q, hs.mem_of_tendsto ((hup.comp φ_mono.tendsto_atTop).vsub hφq) (eventually_of_forall fun n ↦ ?_), hqt,
    vsub_vadd _ _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
v : ℕ → P
hav : ∀ (n : ℕ), a n ∈ s ∧ v n ∈ t ∧ (fun x x_1 => x +ᵥ x_1) (a n) (v n) = u n
q : P
hqt : q ∈ t
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφq : Tendsto ((fun n => v n) ∘ φ) atTop (𝓝 q)
n : ℕ
⊢ (u ∘ φ -ᵥ (fun n => v n) ∘ φ) n ∈ s
[PROOFSTEP]
convert (hav (φ n)).1 using 1
[GOAL]
case h.e'_4
α : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
inst✝² : NormedAddCommGroup W
inst✝¹ : MetricSpace Q
inst✝ : NormedAddTorsor W Q
s : Set V
t : Set P
hs : IsClosed s
ht : IsCompact t
u : ℕ → P
p : P
hup : Tendsto u atTop (𝓝 p)
a : ℕ → V
v : ℕ → P
hav : ∀ (n : ℕ), a n ∈ s ∧ v n ∈ t ∧ (fun x x_1 => x +ᵥ x_1) (a n) (v n) = u n
q : P
hqt : q ∈ t
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφq : Tendsto ((fun n => v n) ∘ φ) atTop (𝓝 q)
n : ℕ
⊢ (u ∘ φ -ᵥ (fun n => v n) ∘ φ) n = a (φ n)
[PROOFSTEP]
exact (eq_vadd_iff_vsub_eq _ _ _).mp (hav (φ n)).2.2.symm


[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
⊢ completion (id G) = id (Completion G)
[PROOFSTEP]
ext x
[GOAL]
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
x : Completion G
⊢ ↑(completion (id G)) x = ↑(id (Completion G)) x
[PROOFSTEP]
rw [NormedAddGroupHom.completion_def, NormedAddGroupHom.coe_id, Completion.map_id]
[GOAL]
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
x : Completion G
⊢ _root_.id x = ↑(id (Completion G)) x
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
⊢ NormedAddGroupHom.comp (completion g) (completion f) = completion (NormedAddGroupHom.comp g f)
[PROOFSTEP]
ext x
[GOAL]
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ ↑(NormedAddGroupHom.comp (completion g) (completion f)) x = ↑(completion (NormedAddGroupHom.comp g f)) x
[PROOFSTEP]
rw [NormedAddGroupHom.coe_comp, NormedAddGroupHom.completion_def, NormedAddGroupHom.completion_coe_to_fun,
  NormedAddGroupHom.completion_coe_to_fun, Completion.map_comp g.uniformContinuous f.uniformContinuous]
[GOAL]
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ Completion.map (↑g ∘ ↑f) x = Completion.map (↑(NormedAddGroupHom.comp g f)) x
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
⊢ ∀ (v : G), ‖↑G v‖ ≤ 1 * ‖v‖
[PROOFSTEP]
simp [le_refl]
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
⊢ NormedAddGroupHom.comp (completion f) toCompl = NormedAddGroupHom.comp toCompl f
[PROOFSTEP]
ext x
[GOAL]
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
x : G
⊢ ↑(NormedAddGroupHom.comp (completion f) toCompl) x = ↑(NormedAddGroupHom.comp toCompl f) x
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
x : G
⊢ ‖↑f x‖ ≤ ‖completion f‖ * ‖x‖
[PROOFSTEP]
simpa using f.completion.le_opNorm x
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
⊢ range (NormedAddGroupHom.comp toCompl (incl (ker f))) ≤ ker (completion f)
[PROOFSTEP]
rintro _ ⟨⟨g, h₀ : f g = 0⟩, rfl⟩
[GOAL]
case intro.mk
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : G
h₀ : ↑f g = 0
⊢ ↑(toAddMonoidHom (NormedAddGroupHom.comp toCompl (incl (ker f)))) { val := g, property := h₀ } ∈ ker (completion f)
[PROOFSTEP]
simp [h₀, mem_ker, Completion.coe_zero]
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
⊢ ↑(ker (completion f)) = closure ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f))))
[PROOFSTEP]
refine le_antisymm ?_ (closure_minimal f.ker_le_ker_completion f.completion.isClosed_ker)
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
⊢ ↑(ker (completion f)) ≤ closure ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f))))
[PROOFSTEP]
rintro hatg (hatg_in : f.completion hatg = 0)
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
⊢ hatg ∈ closure ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f))))
[PROOFSTEP]
rw [SeminormedAddCommGroup.mem_closure_iff]
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
⊢ ∀ (ε : ℝ), 0 < ε → ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
intro ε ε_pos
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
rcases h.exists_pos with ⟨C', C'_pos, hC'⟩
[GOAL]
case intro.intro
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
rcases exists_pos_mul_lt ε_pos (1 + C' * ‖f‖) with ⟨δ, δ_pos, hδ⟩
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
obtain ⟨_, ⟨g : G, rfl⟩, hg : ‖hatg - g‖ < δ⟩ :=
  SeminormedAddCommGroup.mem_closure_iff.mp (Completion.denseInducing_coe.dense hatg) δ δ_pos
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
obtain ⟨g' : G, hgg' : f g' = f g, hfg : ‖g'‖ ≤ C' * ‖f g‖⟩ := hC' (f g) (mem_range_self _ g)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
have mem_ker : g - g' ∈ f.ker := by rw [f.mem_ker, map_sub, sub_eq_zero.mpr hgg'.symm]
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
⊢ g - g' ∈ ker f
[PROOFSTEP]
rw [f.mem_ker, map_sub, sub_eq_zero.mpr hgg'.symm]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
refine ⟨_, ⟨⟨g - g', mem_ker⟩, rfl⟩, ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
⊢ ‖hatg - ↑(toAddMonoidHom (NormedAddGroupHom.comp toCompl (incl (ker f)))) { val := g - g', property := mem_ker }‖ < ε
[PROOFSTEP]
have : ‖f g‖ ≤ ‖f‖ * δ
[GOAL]
case this
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
⊢ ‖↑f g‖ ≤ ‖f‖ * δ
case intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ ‖hatg - ↑(toAddMonoidHom (NormedAddGroupHom.comp toCompl (incl (ker f)))) { val := g - g', property := mem_ker }‖ < ε
[PROOFSTEP]
calc
  ‖f g‖ ≤ ‖f‖ * ‖hatg - g‖ := by simpa [hatg_in] using f.completion.le_opNorm (hatg - g)
  _ ≤ ‖f‖ * δ := by gcongr
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
⊢ ‖↑f g‖ ≤ ‖f‖ * ‖hatg - ↑G g‖
[PROOFSTEP]
simpa [hatg_in] using f.completion.le_opNorm (hatg - g)
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
⊢ ‖f‖ * ‖hatg - ↑G g‖ ≤ ‖f‖ * δ
[PROOFSTEP]
gcongr
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ ‖hatg - ↑(toAddMonoidHom (NormedAddGroupHom.comp toCompl (incl (ker f)))) { val := g - g', property := mem_ker }‖ < ε
[PROOFSTEP]
calc
  ‖hatg - ↑(g - g')‖ = ‖hatg - g + g'‖ := by rw [Completion.coe_sub, sub_add]
  _ ≤ ‖hatg - g‖ + ‖(g' : Completion G)‖ := (norm_add_le _ _)
  _ = ‖hatg - g‖ + ‖g'‖ := by rw [Completion.norm_coe]
  _ < δ + C' * ‖f g‖ := (add_lt_add_of_lt_of_le hg hfg)
  _ ≤ δ + C' * (‖f‖ * δ) := by gcongr
  _ < ε := by simpa only [add_mul, one_mul, mul_assoc] using hδ
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ ‖hatg - ↑G (g - g')‖ = ‖hatg - ↑G g + ↑G g'‖
[PROOFSTEP]
rw [Completion.coe_sub, sub_add]
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ ‖hatg - ↑G g‖ + ‖↑G g'‖ = ‖hatg - ↑G g‖ + ‖g'‖
[PROOFSTEP]
rw [Completion.norm_coe]
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ δ + C' * ‖↑f g‖ ≤ δ + C' * (‖f‖ * δ)
[PROOFSTEP]
gcongr
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ δ + C' * (‖f‖ * δ) < ε
[PROOFSTEP]
simpa only [add_mul, one_mul, mul_assoc] using hδ
[GOAL]
G : Type u_1
inst✝³ : SeminormedAddCommGroup G
H : Type u_2
inst✝² : SeminormedAddCommGroup H
inst✝¹ : SeparatedSpace H
inst✝ : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom (Completion G) H
hg : ∀ (v : G), ↑f v = ↑g (↑G v)
⊢ extension f = g
[PROOFSTEP]
ext v
[GOAL]
case H
G : Type u_1
inst✝³ : SeminormedAddCommGroup G
H : Type u_2
inst✝² : SeminormedAddCommGroup H
inst✝¹ : SeparatedSpace H
inst✝ : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom (Completion G) H
hg : ∀ (v : G), ↑f v = ↑g (↑G v)
v : Completion G
⊢ ↑(extension f) v = ↑g v
[PROOFSTEP]
rw [NormedAddGroupHom.extension_coe_to_fun,
  Completion.extension_unique f.uniformContinuous g.uniformContinuous fun a => hg a]


[GOAL]
E : Type u_1
inst✝ : SeminormedAddCommGroup E
x y : Completion E
⊢ dist x y = ‖x - y‖
[PROOFSTEP]
induction x, y using Completion.induction_on₂
[GOAL]
case hp
E : Type u_1
inst✝ : SeminormedAddCommGroup E
⊢ IsClosed {x | dist x.fst x.snd = ‖x.fst - x.snd‖}
[PROOFSTEP]
refine' isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous _
[GOAL]
case hp
E : Type u_1
inst✝ : SeminormedAddCommGroup E
⊢ Continuous fun x => ‖x.fst - x.snd‖
[PROOFSTEP]
exact Continuous.comp Completion.continuous_extension continuous_sub
[GOAL]
case ih
E : Type u_1
inst✝ : SeminormedAddCommGroup E
a✝ b✝ : E
⊢ dist (↑E a✝) (↑E b✝) = ‖↑E a✝ - ↑E b✝‖
[PROOFSTEP]
rw [← Completion.coe_sub, norm_coe, Completion.dist_eq, dist_eq_norm]


[GOAL]
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
⊢ Bounded (s * t)
[PROOFSTEP]
obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le'
[GOAL]
case intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
⊢ Bounded (s * t)
[PROOFSTEP]
obtain ⟨Rt, hRt⟩ : ∃ R, ∀ x ∈ t, ‖x‖ ≤ R := ht.exists_norm_le'
[GOAL]
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
⊢ Bounded (s * t)
[PROOFSTEP]
refine' bounded_iff_forall_norm_le'.2 ⟨Rs + Rt, _⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
⊢ ∀ (x : E), x ∈ s * t → ‖x‖ ≤ Rs + Rt
[PROOFSTEP]
rintro z ⟨x, y, hx, hy, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x✝ y✝ : E
hs : Bounded s
ht : Bounded t
Rs : ℝ
hRs : ∀ (x : E), x ∈ s → ‖x‖ ≤ Rs
Rt : ℝ
hRt : ∀ (x : E), x ∈ t → ‖x‖ ≤ Rt
x y : E
hx : x ∈ s
hy : y ∈ t
⊢ ‖(fun x x_1 => x * x_1) x y‖ ≤ Rs + Rt
[PROOFSTEP]
exact norm_mul_le_of_le (hRs x hx) (hRt y hy)
[GOAL]
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ Bounded s → Bounded s⁻¹
[PROOFSTEP]
simp_rw [bounded_iff_forall_norm_le', ← image_inv, ball_image_iff, norm_inv']
[GOAL]
E : Type u_1
inst✝ : SeminormedGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ (∃ C, ∀ (x : E), x ∈ s → ‖x‖ ≤ C) → ∃ C, ∀ (x : E), x ∈ s → ‖x‖ ≤ C
[PROOFSTEP]
exact id
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s✝ t : Set E
x✝ y x : E
s : Set E
⊢ infEdist x⁻¹ s⁻¹ = infEdist x s
[PROOFSTEP]
rw [← image_inv, infEdist_image isometry_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s✝ t : Set E
x✝ y x : E
s : Set E
⊢ infEdist x⁻¹ s = infEdist x s⁻¹
[PROOFSTEP]
rw [← infEdist_inv_inv, inv_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ (thickening δ s)⁻¹ = thickening δ s⁻¹
[PROOFSTEP]
simp_rw [thickening, ← infEdist_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x | EMetric.infEdist x s < ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s < ENNReal.ofReal δ}
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ (cthickening δ s)⁻¹ = cthickening δ s⁻¹
[PROOFSTEP]
simp_rw [cthickening, ← infEdist_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x | EMetric.infEdist x s ≤ ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s ≤ ENNReal.ofReal δ}
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} * ball y δ = ball (x * y) δ
[PROOFSTEP]
simp only [preimage_mul_ball, image_mul_left, singleton_mul, div_inv_eq_mul, mul_comm y x]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} / ball y δ = ball (x / y) δ
[PROOFSTEP]
simp_rw [div_eq_mul_inv, inv_ball, singleton_mul_ball]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball x δ * {y} = ball (x * y) δ
[PROOFSTEP]
rw [mul_comm, singleton_mul_ball, mul_comm y]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball x δ / {y} = ball (x / y) δ
[PROOFSTEP]
simp_rw [div_eq_mul_inv, inv_singleton, ball_mul_singleton]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} * ball 1 δ = ball x δ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} / ball 1 δ = ball x δ
[PROOFSTEP]
rw [singleton_div_ball, div_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball 1 δ * {x} = ball x δ
[PROOFSTEP]
simp [ball_mul_singleton]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball 1 δ / {x} = ball x⁻¹ δ
[PROOFSTEP]
rw [ball_div_singleton, one_div]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ x • ball 1 δ = ball x δ
[PROOFSTEP]
rw [smul_ball, smul_eq_mul, mul_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} * closedBall y δ = closedBall (x * y) δ
[PROOFSTEP]
simp_rw [singleton_mul, ← smul_eq_mul, image_smul, smul_closedBall]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} / closedBall y δ = closedBall (x / y) δ
[PROOFSTEP]
simp_rw [div_eq_mul_inv, inv_closedBall, singleton_mul_closedBall]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ closedBall x δ * {y} = closedBall (x * y) δ
[PROOFSTEP]
simp [mul_comm _ { y }, mul_comm y]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ closedBall x δ / {y} = closedBall (x / y) δ
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} * closedBall 1 δ = closedBall x δ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} / closedBall 1 δ = closedBall x δ
[PROOFSTEP]
rw [singleton_div_closedBall, div_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ closedBall 1 δ * {x} = closedBall x δ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ closedBall 1 δ / {x} = closedBall x⁻¹ δ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ x • closedBall 1 δ = closedBall x δ
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s * ball 1 δ = thickening δ s
[PROOFSTEP]
rw [thickening_eq_biUnion_ball]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s * ball 1 δ = ⋃ (x : E) (_ : x ∈ s), ball x δ
[PROOFSTEP]
convert iUnion₂_mul (fun x (_ : x ∈ s) => { x }) (ball (1 : E) δ)
[GOAL]
case h.e'_2.h.e'_5
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s = ⋃ (i : E) (_ : i ∈ s), {i}
case h.e'_3.h.e'_3.h.f
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ
[PROOFSTEP]
exact s.biUnion_of_singleton.symm
[GOAL]
case h.e'_3.h.e'_3.h.f
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h.e'_3.h.f.h
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝² y x✝¹ : E
x✝ : x✝¹ ∈ s
x : E
⊢ x ∈ ball x✝¹ δ ↔ x ∈ {x✝¹} * ball 1 δ
[PROOFSTEP]
simp_rw [singleton_mul_ball, mul_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s / ball 1 δ = thickening δ s
[PROOFSTEP]
simp [div_eq_mul_inv, mul_ball_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball 1 δ * s = thickening δ s
[PROOFSTEP]
rw [mul_comm, mul_ball_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball 1 δ / s = thickening δ s⁻¹
[PROOFSTEP]
simp [div_eq_mul_inv, ball_mul_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s * ball x δ = x • thickening δ s
[PROOFSTEP]
rw [← smul_ball_one, mul_smul_comm, mul_ball_one]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s / ball x δ = x⁻¹ • thickening δ s
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball x δ * s = x • thickening δ s
[PROOFSTEP]
rw [mul_comm, mul_ball]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ ball x δ / s = x • thickening δ s⁻¹
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = cthickening δ s
[PROOFSTEP]
rw [hs.cthickening_eq_biUnion_closedBall hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = ⋃ (x : E) (_ : x ∈ s), closedBall x δ
[PROOFSTEP]
ext x
[GOAL]
case h
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ x ∈ s * closedBall 1 δ ↔ x ∈ ⋃ (x : E) (_ : x ∈ s), closedBall x δ
[PROOFSTEP]
simp only [mem_mul, dist_eq_norm_div, exists_prop, mem_iUnion, mem_closedBall, exists_and_left, mem_closedBall_one_iff,
  ← eq_div_iff_mul_eq'', div_one, exists_eq_right]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s / closedBall 1 δ = cthickening δ s
[PROOFSTEP]
simp [div_eq_mul_inv, hs.mul_closedBall_one hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ closedBall 1 δ * s = cthickening δ s
[PROOFSTEP]
rw [mul_comm, hs.mul_closedBall_one hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ closedBall 1 δ / s = cthickening δ s⁻¹
[PROOFSTEP]
simp [div_eq_mul_inv, mul_comm, hs.inv.mul_closedBall_one hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ s * closedBall x δ = x • cthickening δ s
[PROOFSTEP]
rw [← smul_closedBall_one, mul_smul_comm, hs.mul_closedBall_one hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ s / closedBall x δ = x⁻¹ • cthickening δ s
[PROOFSTEP]
simp [div_eq_mul_inv, mul_comm, hs.mul_closedBall hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ closedBall x δ * s = x • cthickening δ s
[PROOFSTEP]
rw [mul_comm, hs.mul_closedBall hδ]
[GOAL]
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝ y : E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ closedBall x δ * s = x • cthickening δ s
[PROOFSTEP]
simp [div_eq_mul_inv, hs.closedBall_mul hδ]