awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a b : E
rw : ‖a / b‖ ≠ 0 ↔ a ≠ b
⊢ 0 < ‖a / b‖ ↔ a ≠ b

Tactic:
rw [(norm_nonneg' _).lt_iff_ne, ne_comm]

Premises used: norm_nonneg', LE.le.lt_iff_ne, ne_comm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a b : E
⊢ ‖a / b‖ ≠ 0 ↔ a ≠ b

Tactic:
norm_div_eq_zero_iff.not

Premises used: Iff.not, norm_div_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a b : E
⊢ ‖a / b‖ ≠ 0 ↔ a ≠ b

Tactic:
exact norm_div_eq_zero_iff.not

Premises used: Iff.not, norm_div_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a b : E
h : ‖a / b‖ ≤ 0
rwa : a / b = 1
rwa₁ rwa₂ rwa₃ rwa₄ : ‖a / b‖ ≤ 0
⊢ a = b

Tactic:
rwa [← div_eq_one, ← norm_le_zero_iff']

Premises used: div_eq_one, norm_le_zero_iff'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a : E
⊢ a = 1 ∨ 0 < ‖a‖

Tactic:
simpa [eq_comm] using (norm_nonneg' a).eq_or_lt

Premises used: LE.le.eq_or_lt, norm_nonneg', eq_comm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a : E
⊢ a = 1 ∨ 0 < ‖a‖₊

Tactic:
eq_one_or_norm_pos a

Premises used: eq_one_or_norm_pos
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a : E
rw : (↑‖a‖₊ : ℝ) = 0 ↔ a = 1
rw₁ : ‖a‖ = 0 ↔ a = 1
rw₂ rw₃ : a = 1 ↔ a = 1
⊢ ‖a‖₊ = 0 ↔ a = 1

Tactic:
rw [← NNReal.coe_eq_zero, coe_nnnorm', norm_eq_zero']

Premises used: coe_nnnorm', NNReal.coe_eq_zero, norm_eq_zero'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a : E
⊢ ‖a‖₊ ≠ 0 ↔ a ≠ 1

Tactic:
nnnorm_eq_zero'.not

Premises used: Iff.not, nnnorm_eq_zero'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a : E
⊢ 0 < ‖a‖₊ ↔ a ≠ 1

Tactic:
pos_iff_ne_zero.trans nnnorm_ne_zero_iff'

Premises used: Iff.trans, nnnorm_ne_zero_iff', pos_iff_ne_zero
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
⊢ Eq (α := (a : E) → ℝ) (⇑(normGroupNorm E) : (a : E) → ℝ) norm

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
α : Type u_2
E : Type u_5
inst : NormedAddGroup E
inst_1 : TopologicalSpace α
f : α → E
⊢ (HasCompactSupport (β := ℝ) fun (x : α) ↦ ‖f x‖) ↔ HasCompactSupport f

Tactic:
hasCompactSupport_comp_left norm_eq_zero

Premises used: norm_eq_zero, hasCompactSupport_comp_left
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
⊢ comap norm atTop = cobounded E

Tactic:
simpa only [dist_one_right] using comap_dist_right_atTop (1 : E)

Premises used: Metric.comap_dist_right_atTop, OfNat.ofNat, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
ι : Sort u_5
p : ι → Prop
s : ι → Set ℝ
h : HasBasis atTop p s
⊢ (cobounded E).HasBasis p fun (i : ι) ↦ norm ⁻¹' s i

Tactic:
comap_norm_atTop' (E := E) ▸ h.comap _

Premises used: comap_norm_atTop', Eq.rec, Filter.HasBasis.comap
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
⊢ (cobounded E).HasBasis (fun (x : ℝ) ↦ True) fun (x : ℝ) ↦ {x_1 : E | x ≤ ‖x_1‖}

Tactic:
atTop_basis.cobounded_of_norm'

Premises used: Filter.atTop_basis, Set.Ici, Set.Mem, setOf, Filter.HasBasis.cobounded_of_norm', Set.preimage
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedGroup E
f : α → E
l : Filter α
rw : Tendsto (β := ℝ) (fun (x : α) ↦ ‖f x‖) l atTop ↔ Tendsto (norm ∘ f) l atTop
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖f x‖) l atTop ↔ Tendsto f l (cobounded E)

Tactic:
rw [← comap_norm_atTop', tendsto_comap_iff]

Premises used: comap_norm_atTop', Filter.tendsto_comap_iff
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖f x‖) l atTop ↔ Tendsto (norm ∘ f) l atTop

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
⊢ Tendsto norm (cobounded E) atTop

Tactic:
tendsto_norm_atTop_iff_cobounded'.2 tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, tendsto_norm_atTop_iff_cobounded'
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
a : ℝ
⊢ ∀ᶠ (x : E) in cobounded E, a ≤ ‖x‖

Tactic:
tendsto_norm_cobounded_atTop'.eventually_ge_atTop a

Premises used: tendsto_norm_cobounded_atTop', Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
inst_1 : ProperSpace E
⊢ Tendsto norm (cocompact E) atTop

Tactic:
cobounded_eq_cocompact (α := E) ▸ tendsto_norm_cobounded_atTop'

Premises used: Eq.rec, Metric.cobounded_eq_cocompact, tendsto_norm_cobounded_atTop'
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
⊢ (cobounded E)⁻¹ = cobounded E

Tactic:
simp only [← comap_norm_atTop', ← Filter.comap_inv, comap_comap, Function.comp_def, norm_inv']

Premises used: comap_norm_atTop', norm_inv', Function.comp_def, Filter.comap_inv, Filter.comap_comap
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
⊢ Tendsto Inv.inv (cobounded E) (cobounded E)

Tactic:
inv_cobounded.le

Premises used: Set.Mem, Eq.le, Filter.Tendsto, Filter.inv_cobounded
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

Tactic:
simpa only [Set.subset_def, mem_closedBall_one_iff] using isBounded_iff_subset_closedBall (1 : E)

Premises used: Set.subset_def, mem_closedBall_one_iff, OfNat.ofNat, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
s : Set E
hs : IsBounded s
R₀ : ℝ
hR₀ : ∀ x ∈ s, ‖x‖ ≤ R₀
⊢ max R₀ 1 > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
s : Set E
hs : IsBounded s
R : ℝ
hR₀ : R > 0
hR : ∀ x ∈ s, ‖x‖ ≤ R
⊢ R + 1 > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedGroup E
inst_1 : Nonempty α
inst_2 : SemilatticeSup α
u : α → E
⊢ CauchySeq u ↔ ∀ ε > 0, ∃ (N : α), ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖(u m)⁻¹ * u n‖ < ε

Tactic:
simp [Metric.cauchySeq_iff, dist_eq_norm_inv_mul]

Premises used: Metric.cauchySeq_iff, dist_eq_norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedGroup E
inst_1 : TopologicalSpace α
s : Set α
hs : IsCompact s
f : α → E
hf : ContinuousOn f s
⊢ ∃ (C : ℝ), ∀ x ∈ s, ‖f x‖ ≤ C

Tactic:
(isBounded_iff_forall_norm_le'.1 (hs.image_of_continuousOn hf).isBounded).imp fun _C hC _x hx =>
    hC _ <| Set.mem_image_of_mem _ hx

Premises used: isBounded_iff_forall_norm_le', IsCompact.isBounded, Exists.imp, IsCompact.image_of_continuousOn, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedGroup E
inst_1 : TopologicalSpace α
f : α → E
hf : HasCompactMulSupport f
h'f : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

Tactic:
simpa using (hf.isCompact_range h'f).isBounded.exists_norm_le'

Premises used: IsCompact.isBounded, Bornology.IsBounded.exists_norm_le', HasCompactMulSupport.isCompact_range
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
hg : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (Norm.norm ∘ g)
op : E → F → G
h_op : ∃ (A : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
obtain :
  ∀ (A : ℝ) (h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖),
    Tendsto.{u_1, u_4} (β := G) (fun (x : α) ↦ op (f x) (g x)) l (𝓝 1)
⊢ Tendsto.{u_1, u_4} (β := G) (fun (x : α) ↦ op (f x) (g x)) l (𝓝 1)

Tactic:
obtain ⟨A, h_op⟩ := h_op
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
hg : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (Norm.norm ∘ g)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
rcases :
  ∀ (C : ℝ) (hC : ∀ᶠ (x : ℝ) in map (Norm.norm ∘ g) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x C),
    Tendsto.{u_1, u_4} (β := G) (fun (x : α) ↦ op (f x) (g x)) l (𝓝 1)
⊢ Tendsto.{u_1, u_4} (β := G) (fun (x : α) ↦ op (f x) (g x)) l (𝓝 1)

Tactic:
rcases hg with ⟨C, hC⟩
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (x : ℝ) in map (Norm.norm ∘ g) l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x C
⊢ ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C

Tactic:
rw [eventually_map] at hC

Premises used: Filter.eventually_map
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
rw :
  ∀ (hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε) (op : E → F → G) (A : ℝ)
    (h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) (C : ℝ)
    (hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C),
    ∀ ε > 0, ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
⊢ Tendsto.{u_1, u_4} (β := G) (fun (x : α) ↦ op (f x) (g x)) l (𝓝 1)

Tactic:
rw [NormedGroup.tendsto_nhds_one] at hf ⊢

Premises used: NormedGroup.tendsto_nhds_one
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
rcases : ∀ (δ : ℝ) (δ₀ : 0 < δ) (hδ : A * C * δ < ε), ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε

Tactic:
rcases exists_pos_mul_lt ε₀ (A * C) with ⟨δ, δ₀, hδ⟩

Premises used: HMul.hMul, exists_pos_mul_lt
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
h : ∀ (i : α) (hf : ‖f i‖ < δ) (hg : (Norm.norm ∘ g) i ≤ C), ‖op (f i) (g i)‖ < ε
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε

Tactic:
filter_upwards [hf δ δ₀, hC] with i hf hg
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf_1 : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
⊢ ‖op (f i) (g i)‖ < ε

Tactic:
(h_op _ _).trans_lt ?_

Premises used: LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf_1 : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
h : A * ‖f i‖ * ‖g i‖ < ε
⊢ ‖op (f i) (g i)‖ < ε

Tactic:
refine (h_op _ _).trans_lt ?_

Premises used: LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf_1 : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
h : ∀ (hA : A ≤ 0), A * ‖f i‖ * ‖g i‖ < ε
h₁ : ∀ (hA : 0 ≤ A), A * ‖f i‖ * ‖g i‖ < ε
⊢ A * ‖f i‖ * ‖g i‖ < ε

Tactic:
rcases le_total A 0 with hA | hA

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf_1 : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : A ≤ 0
⊢ A * ‖f i‖ * ‖g i‖ < ε

Tactic:
(mul_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonpos_of_nonneg hA <| norm_nonneg' _) <|
      norm_nonneg' _).trans_lt ε₀

Premises used: mul_nonpos_of_nonpos_of_nonneg, norm_nonneg', LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf_1 : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : A ≤ 0
⊢ A * ‖f i‖ * ‖g i‖ < ε

Tactic:
exact (mul_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonpos_of_nonneg hA <| norm_nonneg' _) <|
      norm_nonneg' _).trans_lt ε₀

Premises used: mul_nonpos_of_nonpos_of_nonneg, norm_nonneg', LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf_1 : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
h₂ : ‖g i‖ ≤ C
⊢ A * ‖f i‖ * ‖g i‖ ≤ A * δ * C

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf_1 : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ ‖g i‖ ≤ C

Tactic:
hg
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf_1 : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ ‖g i‖ ≤ C

Tactic:
exact hg
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf_1 : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ A * δ * C = A * C * δ

Tactic:
mul_right_comm _ _ _

Premises used: mul_right_comm
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf_1 : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ A * C * δ < ε

Tactic:
hδ
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf_1 : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
A₁ : A * ‖f i‖ * ‖g i‖ ≤ A * δ * C
⊢ A * ‖f i‖ * ‖g i‖ < ε

Tactic:
calc
    A * ‖f i‖ * ‖g i‖ ≤ A * δ * C := by gcongr; exact hg
    _ = A * C * δ := mul_right_comm _ _ _
    _ < ε := hδ

Premises used: mul_right_comm
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
hg : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (Norm.norm ∘ g)
op : E → F → G
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖
⊢ Tendsto.{u_1, u_4} (β := G) (fun (x : α) ↦ op (f x) (g x)) l (𝓝 1)

Tactic:
hf.op_one_isBoundedUnder_le' hg op ⟨1, fun x y => (one_mul ‖x‖).symm ▸ h_op x y⟩

Premises used: Norm.norm, Eq.rec, Exists.intro, Filter.Tendsto.op_one_isBoundedUnder_le', OfNat.ofNat, Eq.symm, one_mul
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
X : Type u_5
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
inst_3 : ProperSpace E
e : X → E
he : Topology.IsClosedEmbedding e
rw : Tendsto (norm ∘ e) (cocompact X) atTop
⊢ Tendsto (norm ∘ e) Filter.cofinite atTop

Tactic:
rw [← Filter.cocompact_eq_cofinite X]

Premises used: Filter.cocompact_eq_cofinite
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
E : Type u_2
inst : SeminormedGroup E
X : Type u_5
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
inst_3 : ProperSpace E
e : X → E
he : Topology.IsClosedEmbedding e
⊢ Tendsto (norm ∘ e) (cocompact X) atTop

Tactic:
apply tendsto_norm_cocompact_atTop'.comp (Topology.IsClosedEmbedding.tendsto_cocompact he)

Premises used: Topology.IsClosedEmbedding.tendsto_cocompact, tendsto_norm_cocompact_atTop', Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddGroup E
inst_1 : TopologicalSpace α
f : α → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : HasCompactSupport f
⊢ ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

Tactic:
simpa [bddAbove_def] using hf.norm.bddAbove_range_of_hasCompactSupport h.norm

Premises used: Continuous.norm, HasCompactSupport.norm, bddAbove_def, Continuous.bddAbove_range_of_hasCompactSupport
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddGroup α
f : α → E
inst_1 : One E
hf : HasCompactMulSupport f
obtain : ∀ (K : Set α) (hK1 : IsCompact K) (hK2 : ∀ x ∉ K, f x = 1), ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
⊢ ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

Tactic:
obtain ⟨K, ⟨hK1, hK2⟩⟩ := exists_compact_iff_hasCompactMulSupport.mpr hf

Premises used: Iff.mpr, exists_compact_iff_hasCompactMulSupport
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddGroup α
f : α → E
inst_1 : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
obtain : ∀ (S : ℝ) (hS : S > 0) (hS' : ∀ x ∈ K, ‖x‖ ≤ S), ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
⊢ ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

Tactic:
obtain ⟨S, hS, hS'⟩ := hK1.isBounded.exists_pos_norm_le

Premises used: IsCompact.isBounded, Bornology.IsBounded.exists_pos_norm_le
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddGroup α
f : α → E
inst_1 : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
⊢ 0 < S + 1

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddGroup α
f : α → E
inst_1 : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
refine : ∀ (x : α) (hx : S + 1 ≤ ‖x‖), ¬‖x‖ ≤ S
⊢ ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

Tactic:
refine ⟨S + 1, by positivity, fun x hx => hK2 x ((mt <| hS' x) ?_)⟩
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddGroup α
f : α → E
inst_1 : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
x : α
hx : S + 1 ≤ ‖x‖
contrapose! : ∀ (hx : ‖x‖ ≤ S), ‖x‖ < S + 1
⊢ ¬‖x‖ ≤ S

Tactic:
contrapose! hx
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddGroup α
f : α → E
inst_1 : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
x : α
hx : ‖x‖ ≤ S
⊢ ‖x‖ < S + 1

Tactic:
lt_add_of_le_of_pos hx zero_lt_one

Premises used: zero_lt_one, lt_add_of_le_of_pos
-- Module: Mathlib.Analysis.Normed.Group.Bounded
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddGroup α
f : α → E
inst_1 : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
x : α
hx : ‖x‖ ≤ S
⊢ ‖x‖ < S + 1

Tactic:
exact lt_add_of_le_of_pos hx zero_lt_one

Premises used: zero_lt_one, lt_add_of_le_of_pos
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : 𝓕
inst_2 : ProperSpace F
inst_3 : FunLike 𝓕 E F
inst_4 : CocompactMapClass 𝓕 E F
ε : ℝ
⊢ Tendsto (⇑f : (a : E) → F) (cocompact E) (cocompact F)

Tactic:
have h := cocompact_tendsto f
-- Module: Mathlib.Analysis.Normed.Group.CocompactMap
Goal:
E : Type u_2
F : Type u_3
𝓕 : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : 𝓕
inst_2 : ProperSpace F
inst_3 : FunLike 𝓕 E F
inst_4 : CocompactMapClass 𝓕 E F
ε : ℝ
h : Tendsto (⇑f : (a : E) → F) (cocompact E) (cocompact F)
⊢ ∀ s ∈ cocompact F, (⇑f : (a : E) → F) ⁻¹' s ∈ cocompact E

Tactic:
rw [tendsto_def] at h

Premises used: Filter.tendsto_def