awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
rw : dist x y * (↑(Kf⁻¹ - Kg) : ℝ) ≤ dist (f x * g x) (f y * g y)
⊢ dist x y ≤ dist (f x * g x) (f y * g y) / (↑(Kf⁻¹ - Kg) : ℝ)

Tactic:
rw [le_div_iff₀ (NNReal.coe_pos.2 <| tsub_pos_iff_lt.2 hK)]

Premises used: Iff.mpr, tsub_pos_iff_lt, NNReal.coe_pos, le_div_iff₀
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
rw : (↑Kf⁻¹ : ℝ) * dist x y - (↑Kg : ℝ) * dist x y ≤ dist (f x * g x) (f y * g y)
⊢ dist x y * (↑(Kf⁻¹ - Kg) : ℝ) ≤ dist (f x * g x) (f y * g y)

Tactic:
rw [mul_comm, NNReal.coe_sub hK.le, sub_mul]

Premises used: LT.lt.le, sub_mul, mul_comm, NNReal.coe_sub
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
⊢ (↑Kf⁻¹ : ℝ) * dist x y - (↑Kg : ℝ) * dist x y ≤ dist (f x) (f y) - dist (g x) (g y)

Tactic:
sub_le_sub (hf.mul_le_dist x y) (hg.dist_le_mul x y)

Premises used: LipschitzWith.dist_le_mul, AntilipschitzWith.mul_le_dist, sub_le_sub
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
⊢ dist (f x) (f y) - dist (g x) (g y) ≤ dist (f x * g x) (f y * g y)

Tactic:
le_trans (le_abs_self _) (abs_dist_sub_le_dist_mul_mul _ _ _ _)

Premises used: le_abs_self, abs_dist_sub_le_dist_mul_mul, le_trans
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
⊢ (↑Kf⁻¹ : ℝ) * dist x y - (↑Kg : ℝ) * dist x y ≤ dist (f x * g x) (f y * g y)

Tactic:
calc
    ↑Kf⁻¹ * dist x y - Kg * dist x y ≤ dist (f x) (f y) - dist (g x) (g y) :=
      sub_le_sub (hf.mul_le_dist x y) (hg.dist_le_mul x y)
    _ ≤ _ := le_trans (le_abs_self _) (abs_dist_sub_le_dist_mul_mul _ _ _ _)

Premises used: LipschitzWith.dist_le_mul, le_abs_self, AntilipschitzWith.mul_le_dist, abs_dist_sub_le_dist_mul_mul, sub_le_sub, Dist.dist, le_trans
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg (g / f)
hK : Kg < Kf⁻¹
⊢ AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g

Tactic:
simpa only [Pi.div_apply, mul_div_cancel] using hf.mul_lipschitzWith hg hK

Premises used: AntilipschitzWith.mul_lipschitzWith, Pi.div_apply, mul_div_cancel
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
F : Type u_3
inst : SeminormedCommGroup F
E : Type u_5
inst_1 : SeminormedCommGroup E
K : ℝ≥0
f : E → F
hf : AntilipschitzWith K f
x y : E
⊢ ‖x⁻¹ * y‖ ≤ (↑K : ℝ) * ‖(f x)⁻¹ * f y‖

Tactic:
simp [← dist_eq_norm_inv_mul, hf.le_mul_dist x y]

Premises used: AntilipschitzWith.le_mul_dist, dist_eq_norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
a₁ a₂ b₁ b₂ : E
r₁ r₂ : ℝ
⊢ LipschitzMul E

Tactic:
⟨⟨1 + 1, LipschitzWith.prod_fst.mul LipschitzWith.prod_snd⟩⟩

Premises used: LipschitzWith.prod_snd, LipschitzWith.prod_fst, LipschitzMul.mk, HAdd.hAdd, LipschitzWith.mul, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
a₁ a₂ b₁ b₂ : E
r₁ r₂ : ℝ
⊢ IsUniformGroup E

Tactic:
⟨(LipschitzWith.prod_fst.div LipschitzWith.prod_snd).uniformContinuous⟩

Premises used: LipschitzWith.prod_snd, LipschitzWith.prod_fst, LipschitzWith.uniformContinuous, IsUniformGroup.mk, LipschitzWith.div
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
a₁ a₂ b₁ b₂ : E
r₁ r₂ : ℝ
⊢ IsTopologicalGroup E

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
p : E
⊢ norm (E := SeparationQuotient E) (mk p) = ‖p‖

Tactic:
rfl

Premises used: Quotient.liftOn', SeparationQuotient.lift, rfl
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
p : E
rw : Eq (α := SeparationQuotient E) (mk p) 1 ↔ norm (E := SeparationQuotient E) (mk p) = 0
rw₁ rw₂ : Eq (α := SeparationQuotient E) (mk p) 1 ↔ Eq (α := SeparationQuotient E) (mk p) 1
⊢ Eq (α := SeparationQuotient E) (mk p) 1 ↔ ‖p‖ = 0

Tactic:
rw [← norm_mk', norm_eq_zero']

Premises used: norm_eq_zero', SeparationQuotient.norm_mk'
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
p : E
⊢ nnnorm (E := SeparationQuotient E) (mk p) = ‖p‖₊

Tactic:
rfl

Premises used: Quotient.liftOn', SeparationQuotient.lift, rfl
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k / v k
h : ∀ (n : ℕ), ∏ k ∈ range (n + 1), u k = HMul.hMul (β := (n : ℕ) → E) d (fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k) n
⊢ (fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k) = d * fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k

Tactic:
ext n
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
⊢ ∏ k ∈ range (n + 1), u k = HMul.hMul (β := (n : ℕ) → E) d (fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k) n

Tactic:
simp [d]
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k / v k
rw : CauchySeq (d * fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k)
⊢ CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k

Tactic:
rw [show (fun n => ∏ k ∈ range (n + 1), u k) = d * fun n => ∏ k ∈ range (n + 1), v k
      by ext n; simp [d]]
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k / v k
suffices : ∀ n ≥ N, d n = d N
⊢ CauchySeq (d * fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k)

Tactic:
suffices ∀ n ≥ N, d n = d N from (tendsto_atTop_of_eventually_const this).cauchySeq.mul hv
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
dsimp : Eq.{u_2 + 1} (α := E) (∏ k ∈ range (n + 1), u k / v k) (∏ k ∈ range (N + 1), u k / v k)
⊢ d n = d N

Tactic:
dsimp [d]
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
⊢ N + 1 ≤ n + 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
rw : ∀ n ≥ N + 1, u n / v n = 1
⊢ Eq.{u_2 + 1} (α := E) (∏ k ∈ range (n + 1), u k / v k) (∏ k ∈ range (N + 1), u k / v k)

Tactic:
rw [eventually_constant_prod (N := N + 1) _ (by gcongr)]

Premises used: Finset.eventually_constant_prod
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
m : ℕ
hm : m ≥ N + 1
⊢ u m / v m = 1

Tactic:
simp [huv m (le_of_lt hm)]

Premises used: le_of_lt
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
obtain : ∀ (C : ℝ) (hC : ∀ (m n : ℕ), dist (u m) (u n) < C), BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ ‖u n‖)
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ ‖u n‖)

Tactic:
obtain ⟨C, -, hC⟩ := cauchySeq_bdd hu

Premises used: cauchySeq_bdd
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), dist (u m) (u n) < C
⊢ ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C

Tactic:
simp_rw [SeminormedGroup.dist_eq] at hC

Premises used: SeminormedGroup.dist_eq
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
n : ℕ
rw : ‖u n‖ ≤ ‖u 0‖ + C
⊢ ‖u n‖ ≤ C + ‖u 0‖

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
n : ℕ
⊢ ‖u n‖ ≤ ‖u 0‖ + C

Tactic:
(norm_le_norm_add_norm_inv_mul (u n) (u 0)).trans ?_

Premises used: norm_le_norm_add_norm_inv_mul, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
n : ℕ
refine : ‖u 0‖ + ‖(u n)⁻¹ * u 0‖ ≤ ‖u 0‖ + C
⊢ ‖u n‖ ≤ ‖u 0‖ + C

Tactic:
refine (norm_le_norm_add_norm_inv_mul (u n) (u 0)).trans ?_

Premises used: norm_le_norm_add_norm_inv_mul, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
n : ℕ
⊢ ‖u 0‖ + ‖(u n)⁻¹ * u 0‖ ≤ ‖u 0‖ + C

Tactic:
simp [(hC _ _).le]

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
⊢ ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖

Tactic:
have : ∀ n, ‖u n‖ ≤ C + ‖u 0‖ := by
    intro n
    rw [add_comm]
    refine (norm_le_norm_add_norm_inv_mul (u n) (u 0)).trans ?_
    simp [(hC _ _).le]
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ‖u n‖) y → y ≤ C + ‖u 0‖

Tactic:
simpa using this
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∃ (x : ℝ), ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ‖u n‖) y → y ≤ x

Tactic:
exact ⟨C + ‖u 0‖, by simpa using this⟩
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
f : E → F
C : ℝ≥0
s : Set E
⊢ LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ (↑C : ℝ) * ‖x / y‖

Tactic:
simpa [← norm_inv_mul] using lipschitzOnWith_iff_norm_inv_mul_le

Premises used: lipschitzOnWith_iff_norm_inv_mul_le, norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
f : E → F
C : ℝ≥0
s : Set E
a b : E
r : ℝ
h : LipschitzOnWith C f s
ha : a ∈ s
hb : b ∈ s
hr : ‖a / b‖ ≤ r
ha₁ : 0 ≤ (↑C : ℝ)
⊢ (↑C : ℝ) * ‖a / b‖ ≤ (↑C : ℝ) * r

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
f : E → F
C : ℝ≥0
⊢ LipschitzWith C f ↔ ∀ (x y : E), ‖f x / f y‖ ≤ (↑C : ℝ) * ‖x / y‖

Tactic:
simp only [lipschitzWith_iff_dist_le_mul, dist_eq_norm_div]

Premises used: lipschitzWith_iff_dist_le_mul, dist_eq_norm_div
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
f : E → F
C : ℝ≥0
a b : E
r : ℝ
h : LipschitzWith C f
hr : ‖a / b‖ ≤ r
ha : 0 ≤ (↑C : ℝ)
⊢ (↑C : ℝ) * ‖a / b‖ ≤ (↑C : ℝ) * r

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ : ∀ (x y : ℤ), dist (α := ℝ) (↑x : ℝ) (↑y : ℝ) = dist x y
⊢ ∀ (x y : ℤ), dist (α := ℝ) (↑x : ℝ) (↑y : ℝ) = dist x y

Tactic:
tauto
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
⊢ IsClosedEmbedding (Y := ℝ) Int.cast

Tactic:
isometry_intCast.isClosedEmbedding

Premises used: Real.isometry_intCast, Isometry.isClosedEmbedding
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
⊢ IsClosed (X := ℝ) (Set.range Int.cast)

Tactic:
isClosedEmbedding_intCast.isClosed_range

Premises used: Real.isClosedEmbedding_intCast, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
⊢ IsOpen (X := ℝ) (Set.range Int.cast)ᶜ

Tactic:
Real.isClosed_range_intCast.isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
⊢ Tendsto.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cocompact E) (𝓝 0)

Tactic:
have h := zero_at_infty f
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Tendsto.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cocompact E) (𝓝 0)
⊢ ∀ (s : Set ℝ),
    Membership.mem (γ := Filter ℝ) (𝓝 0) s →
      (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) ⁻¹' s ∈ cocompact E

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero, tendsto_def] at h

Premises used: Filter.tendsto_def, tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h :
  ∀ (s : Set ℝ),
    Membership.mem (γ := Filter ℝ) (𝓝 0) s →
      (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) ⁻¹' s ∈ cocompact E
⊢ Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E

Tactic:
specialize h (Metric.ball 0 ε) (Metric.ball_mem_nhds 0 hε)

Premises used: Metric.ball, Metric.ball_mem_nhds, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E
rcases :
  ∀ (r : ℝ)
    (hr :
      Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ
        (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε))),
    ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε
⊢ ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε

Tactic:
rcases Metric.closedBall_compl_subset_of_mem_cocompact h 0 with ⟨r, hr⟩

Premises used: Metric.closedBall_compl_subset_of_mem_cocompact, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E
r : ℝ
hr :
  Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε))
h₁ : ∀ (x : E) (_hx : r < ‖x‖), norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε
⊢ ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε

Tactic:
use r
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E
r : ℝ
hr :
  Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε))
x : E
hr' : r < ‖x‖
this :
  Membership.mem (γ := Set E)
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε)) x
⊢ norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε

Tactic:
simp_all
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E
r : ℝ
hr :
  Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε))
x : E
hr' : r < ‖x‖
h₁ :
  Membership.mem (γ := Set E)
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε)) x
⊢ norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε

Tactic:
suffices x ∈ (fun x ↦ ‖f x‖) ⁻¹' Metric.ball 0 ε by simp_all
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E
r : ℝ
hr :
  Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε))
x : E
hr' : r < ‖x‖
h₁ : Membership.mem (γ := Set E) (Metric.closedBall 0 r)ᶜ x
⊢ Membership.mem (γ := Set E)
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε)) x

Tactic:
apply hr
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E
r : ℝ
hr :
  Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε))
x : E
hr' : r < ‖x‖
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 r)ᶜ x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
rw : Tendsto (β := ℝ) (fun (x : E) ↦ ‖f x‖) (cocompact E) (𝓝 0)
⊢ Tendsto f (cocompact E) (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
s : Set ℝ
hs : Membership.mem (γ := Filter ℝ) (𝓝 0) s
rw : ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
⊢ Membership.mem (γ := Filter ℝ) (map (fun (x : E) ↦ ‖f x‖) (cocompact E)) s

Tactic:
rw [mem_map, Metric.mem_cocompact_iff_closedBall_compl_subset 0]

Premises used: Metric.mem_cocompact_iff_closedBall_compl_subset, OfNat.ofNat, Filter.mem_map
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
s : Set ℝ
hs : Membership.mem (γ := Filter ℝ) (𝓝 0) s
⊢ ∃ ε > 0, Metric.ball 0 ε ⊆ s

Tactic:
rw [Metric.mem_nhds_iff] at hs

Premises used: Metric.mem_nhds_iff
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
s : Set ℝ
hs : ∃ ε > 0, Metric.ball 0 ε ⊆ s
rcases :
  ∀ (ε : ℝ) (hε : ε > 0) (hs : Metric.ball 0 ε ⊆ s),
    ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
⊢ ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)

Tactic:
rcases hs with ⟨ε, hε, hs⟩
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
rcases :
  ∀ (r : ℝ) (hr : ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε),
    ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
⊢ ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)

Tactic:
rcases h ε hε with ⟨r, hr⟩
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
h₁ : Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
⊢ ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)

Tactic:
use r
-- Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
a : E
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 r)ᶜ a → Membership.mem (γ := Set E) ((fun (x : E) ↦ ‖f x‖) ⁻¹' s) a

Tactic:
aesop