awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : a ∈ closedBall b r
⊢ a ^ n ∈ closedBall (b ^ n) (n • r)
have simp : ∀ (h : ‖a⁻¹ * b‖ ≤ r), ‖(a⁻¹ * b) ^ n‖ ≤ n • r
Tactic: simp only [mem_closedBall, dist_eq_norm_inv_mul, ← inv_pow, ← mul_pow] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ ≤ r
⊢ ‖(a⁻¹ * b) ^ n‖ ≤ n • r
have refine : (↑n : ℝ) * ‖a⁻¹ * b‖ ≤ n • r
Tactic: refine norm_pow_le_mul_norm.trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : a ∈ ball b r
⊢ a ^ n ∈ ball (b ^ n) (n • r)
have simp : ∀ (h : ‖a⁻¹ * b‖ < r), ‖(a⁻¹ * b) ^ n‖ < n • r
Tactic: simp only [mem_ball, dist_eq_norm_inv_mul, ← inv_pow, ← mul_pow] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a⁻¹ * b‖ < r
⊢ ‖(a⁻¹ * b) ^ n‖ < n • r
have refine : (↑n : ℝ) * ‖a⁻¹ * b‖ < n • r
Tactic: refine lt_of_le_of_lt norm_pow_le_mul_norm ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (hypothesis)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a⁻¹ * b‖ < r
⊢ (↑n : ℝ) * ‖a⁻¹ * b‖ < n • r
have hn₁ : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: replace hn : 0 < (n : ℝ) := by norm_cast
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ < r
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ (↑n : ℝ) * ‖a⁻¹ * b‖ < n • r
have rw : (↑n : ℝ) * ‖a⁻¹ * b‖ < (↑n : ℝ) * r
Tactic: rw [nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ < r
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ (↑n : ℝ) * ‖a⁻¹ * b‖ < (↑n : ℝ) * r
have nlinarith : (↑n : ℝ) * r ≤ (↑n : ℝ) * ‖a⁻¹ * b‖ → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ < r
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
nlinarith nlinarith₁ : (↑n : ℝ) * r ≤ (↑n : ℝ) * ‖a⁻¹ * b‖ → HMul.hMul (α := ℝ) 1 1 = 1
⊢ (↑n : ℝ) * ‖a⁻¹ * b‖ < (↑n : ℝ) * r
have nlinarith₂ : (↑n : ℝ) * r ≤ (↑n : ℝ) * ‖a⁻¹ * b‖ →
  HMul.hMul (α := ℝ) 1 (↑n : ℝ) * (1 * r) - HMul.hMul (α := ℝ) 1 (↑n : ℝ) * (1 * ‖a⁻¹ * b‖) +
      (0 - (1 * ‖a⁻¹ * b‖ - 1 * r) * HSub.hSub (α := ℝ) 0 (↑n : ℝ)) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ a * c ∈ closedBall (b * c) r ↔ a ∈ closedBall b r
have simp : ‖b * c * (a * c)⁻¹‖ ≤ r ↔ ‖b * a⁻¹‖ ≤ r
Tactic: simp only [mem_closedBall, dist_eq_norm_inv_mul, mul_comm _ (b * c), mul_comm a⁻¹ b]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ a * c ∈ ball (b * c) r ↔ a ∈ ball b r
have simp : ‖b * c * (a * c)⁻¹‖ < r ↔ ‖b * a⁻¹‖ < r
Tactic: simp only [mem_ball, dist_eq_norm_inv_mul, mul_comm _ (b * c), mul_comm a⁻¹ b]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a • closedBall b r = closedBall (a • b) r
have h : ∀ (x : E), x ∈ a • closedBall b r ↔ x ∈ closedBall (a • b) r
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a • ball b r = ball (a • b) r
have h : ∀ (x : E), x ∈ a • ball b r ↔ x ∈ ball (a • b) r
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
m : Multiset E
⊢ (↑‖m.prod‖₊ : ℝ) ≤ (↑(Multiset.sum (Multiset.map (fun (x : E) ↦ ‖x‖₊) m)) : ℝ)
have push_cast : ‖m.prod‖ ≤ (Multiset.map toReal (Multiset.map (fun (x : E) ↦ ‖x‖₊) m)).sum
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : SeminormedCommGroup E
m : Multiset E
⊢ ‖m.prod‖ ≤ (Multiset.map toReal (Multiset.map (fun (x : E) ↦ ‖x‖₊) m)).sum
have rw : ‖m.prod‖ ≤ (Multiset.map (toReal ∘ fun (x : E) ↦ ‖x‖₊) m).sum
Tactic: rw [Multiset.map_map]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ (↑(nnnorm.{u_5} (E := E) (∏ a ∈ s, f a)) : ℝ) ≤ (↑(∑ a ∈ s, ‖f a‖₊) : ℝ)
have push_cast : norm.{u_5} (E := E) (∏ a ∈ s, f a) ≤ ∑ x ∈ s, ‖f x‖
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : NormedGroup E
a : E
⊢ ‖a‖ ≤ 0 ↔ a = 1
have rw : dist a 1 ≤ 0 ↔ a = 1
Tactic: rw [← dist_one_right, dist_le_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : NormedGroup E
a : E
rw : dist a 1 ≤ 0 ↔ a = 1
⊢ ‖a‖ ≤ 0 ↔ a = 1
have rw₁ : a = 1 ↔ a = 1
Tactic: rw [← dist_one_right, dist_le_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : NormedGroup E
a : E
⊢ 0 < ‖a‖ ↔ a ≠ 1
have rw : ¬‖a‖ ≤ 0 ↔ a ≠ 1
Tactic: rw [← not_le, norm_le_zero_iff']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : NormedGroup E
a : E
rw : ¬‖a‖ ≤ 0 ↔ a ≠ 1
⊢ 0 < ‖a‖ ↔ a ≠ 1
have rw₁ : ¬a = 1 ↔ a ≠ 1
Tactic: rw [← not_le, norm_le_zero_iff']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : NormedGroup E
a b : E
⊢ ‖a / b‖ = 0 ↔ a = b
have rw : a / b = 1 ↔ a = b
Tactic: rw [norm_eq_zero', div_eq_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : NormedGroup E
a b : E
rw : a / b = 1 ↔ a = b
⊢ ‖a / b‖ = 0 ↔ a = b
have rw₁ : a = b ↔ a = b
Tactic: rw [norm_eq_zero', div_eq_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : NormedGroup E
a b : E
⊢ 0 < ‖a / b‖ ↔ a ≠ b
have rw : ‖a / b‖ ≠ 0 ↔ a ≠ b
Tactic: rw [(norm_nonneg' _).lt_iff_ne, ne_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : NormedGroup E
a b : E
h : ‖a / b‖ ≤ 0
⊢ a = b
have rwa : a / b = 1
Tactic: rwa [← div_eq_one, ← norm_le_zero_iff']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : NormedGroup E
a : E
⊢ ‖a‖₊ = 0 ↔ a = 1
have rw : (↑‖a‖₊ : ℝ) = 0 ↔ a = 1
Tactic: rw [← NNReal.coe_eq_zero, coe_nnnorm', norm_eq_zero']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : NormedGroup E
a : E
rw : (↑‖a‖₊ : ℝ) = 0 ↔ a = 1
⊢ ‖a‖₊ = 0 ↔ a = 1
have rw₁ : ‖a‖ = 0 ↔ a = 1
Tactic: rw [← NNReal.coe_eq_zero, coe_nnnorm', norm_eq_zero']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Basic (goal)
Goal:
E : Type u_5
inst : NormedGroup E
a : E
rw : (↑‖a‖₊ : ℝ) = 0 ↔ a = 1
rw₁ : ‖a‖ = 0 ↔ a = 1
⊢ ‖a‖₊ = 0 ↔ a = 1
have rw₂ : a = 1 ↔ a = 1
Tactic: rw [← NNReal.coe_eq_zero, coe_nnnorm', norm_eq_zero']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖f x‖) l atTop ↔ Tendsto f l (cobounded E)
have rw : Tendsto (β := ℝ) (fun (x : α) ↦ ‖f x‖) l atTop ↔ Tendsto (norm ∘ f) l atTop
Tactic: rw [← comap_norm_atTop', tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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‖
⊢ Tendsto.{u_1, u_4} (β := G) (fun (x : α) ↦ op (f x) (g x)) l (𝓝 1)
have 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)
Tactic: obtain ⟨A, h_op⟩ := h_op
Cleared hypotheses: h_op
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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‖
⊢ Tendsto.{u_1, u_4} (β := G) (fun (x : α) ↦ op (f x) (g x)) l (𝓝 1)
have 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)
Tactic: rcases hg with ⟨C, hC⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (hypothesis)
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
⊢ Tendsto.{u_1, u_4} (β := G) (fun (x : α) ↦ op (f x) (g x)) l (𝓝 1)
have hC₁ : ∀ᶠ (a : α) in l, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
Tactic: rw [eventually_map] at hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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
⊢ Tendsto.{u_1, u_4} (β := G) (fun (x : α) ↦ op (f x) (g x)) l (𝓝 1)
have 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)‖ < ε
Tactic: rw [NormedGroup.tendsto_nhds_one] at hf ⊢
Cleared hypotheses: hf, op, A, h_op, C, hC
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
have rcases : ∀ (δ : ℝ) (δ₀ : 0 < δ) (hδ : A * C * δ < ε), ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
Tactic: rcases exists_pos_mul_lt ε₀ (A * C) with ⟨δ, δ₀, hδ⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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 * δ < ε
⊢ ∀ᶠ (x : α) in l, ‖op (f x) (g x)‖ < ε
have h : ∀ (i : α) (hf : ‖f i‖ < δ) (hg : (Norm.norm ∘ g) i ≤ C), ‖op (f i) (g i)‖ < ε
Tactic: filter_upwards [hf δ δ₀, hC] with i hf hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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)‖ < ε
have h : A * ‖f i‖ * ‖g i‖ < ε
Tactic: refine (h_op _ _).trans_lt ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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
⊢ A * ‖f i‖ * ‖g i‖ < ε
have h : ∀ (hA : A ≤ 0), A * ‖f i‖ * ‖g i‖ < ε
Tactic: rcases le_total A 0 with hA | hA
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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‖ < ε
⊢ A * ‖f i‖ * ‖g i‖ < ε
have h₁ : ∀ (hA : 0 ≤ A), A * ‖f i‖ * ‖g i‖ < ε
Tactic: rcases le_total A 0 with hA | hA
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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 * ‖f i‖ * ‖g i‖ ≤ A * δ * C
have h₂ : ‖g i‖ ≤ C
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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 * ‖f i‖ * ‖g i‖ < ε
have A₁ : A * ‖f i‖ * ‖g i‖ ≤ A * δ * C
Tactic: calc
    A * ‖f i‖ * ‖g i‖ ≤ A * δ * C := by gcongr; exact hg
    _ = A * C * δ := mul_right_comm _ _ _
    _ < ε := hδ
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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) Filter.cofinite atTop
have rw : Tendsto (norm ∘ e) (cocompact X) atTop
Tactic: rw [← Filter.cocompact_eq_cofinite X]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddGroup α
f : α → E
inst_1 : One E
hf : HasCompactMulSupport f
⊢ ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
have obtain : ∀ (K : Set α) (hK1 : IsCompact K) (hK2 : ∀ x ∉ K, f x = 1), ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
Tactic: obtain ⟨K, ⟨hK1, hK2⟩⟩ := exists_compact_iff_hasCompactMulSupport.mpr hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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
⊢ ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
have obtain : ∀ (S : ℝ) (hS : S > 0) (hS' : ∀ x ∈ K, ‖x‖ ≤ S), ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
Tactic: obtain ⟨S, hS, hS'⟩ := hK1.isBounded.exists_pos_norm_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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
⊢ ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
have refine : ∀ (x : α) (hx : S + 1 ≤ ‖x‖), ¬‖x‖ ≤ S
Tactic: refine ⟨S + 1, by positivity, fun x hx => hK2 x ((mt <| hS' x) ?_)⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Bounded (goal)
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‖
⊢ ¬‖x‖ ≤ S
have contrapose! : ∀ (hx : ‖x‖ ≤ S), ‖x‖ < S + 1
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (hypothesis)
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
ε : ℝ
⊢ ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have h : Tendsto (⇑f : (a : E) → F) (cocompact E) (cocompact F)
Tactic: have h := cocompact_tendsto f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (hypothesis)
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)
⊢ ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have h₁ : ∀ s ∈ cocompact F, (⇑f : (a : E) → F) ⁻¹' s ∈ cocompact E
Tactic: rw [tendsto_def] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (hypothesis)
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 : ∀ s ∈ cocompact F, (⇑f : (a : E) → F) ⁻¹' s ∈ cocompact E
⊢ ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have h₁ : Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E
Tactic: specialize h (Metric.closedBall 0 ε)ᶜ (mem_cocompact_of_closedBall_compl_subset 0 ⟨ε, rfl.subset⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (goal)
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 : Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E
⊢ ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have rcases : ∀ (r : ℝ)
  (hr :
    Subset.{u_2} (α := Set E) (closedBall 0 r)ᶜ
      (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ)),
  ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
Tactic: rcases closedBall_compl_subset_of_mem_cocompact h 0 with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (goal)
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 : Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : Subset.{u_2} (α := Set E) (closedBall 0 r)ᶜ (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ)
⊢ ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have h₁ : ∀ (x : E), r < ‖x‖ → ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
Tactic: use r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (goal)
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 : Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : Subset.{u_2} (α := Set E) (closedBall 0 r)ᶜ (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ)
x : E
hx : r < ‖x‖
⊢ ε < norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have h₁ : Membership.mem (γ := Set E) (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ) x
Tactic: suffices x ∈ f ⁻¹' (Metric.closedBall 0 ε)ᶜ by simp_all
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (goal)
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 : Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ ∈ cocompact E
r : ℝ
hr : Subset.{u_2} (α := Set E) (closedBall 0 r)ᶜ (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ)
x : E
hx : r < ‖x‖
⊢ Membership.mem (γ := Set E) (Set.preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) (closedBall 0 ε)ᶜ) x
have h₁ : Membership.mem (γ := Set E) (closedBall 0 r)ᶜ x
Tactic: apply hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
⊢ f ⁻¹' s ∈ cocompact E
have rcases : ∀ (ε : ℝ) (hε : (closedBall 0 ε)ᶜ ⊆ s), f ⁻¹' s ∈ cocompact E
Tactic: rcases closedBall_compl_subset_of_mem_cocompact hs 0 with ⟨ε, hε⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
⊢ f ⁻¹' s ∈ cocompact E
have rcases : ∀ (r : ℝ) (hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖), f ⁻¹' s ∈ cocompact E
Tactic: rcases h ε with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
⊢ f ⁻¹' s ∈ cocompact E
have apply : ∃ (r : ℝ), (closedBall 0 r)ᶜ ⊆ f ⁻¹' s
Tactic: apply mem_cocompact_of_closedBall_compl_subset 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
⊢ ∃ (r : ℝ), (closedBall 0 r)ᶜ ⊆ f ⁻¹' s
have h₁ : (closedBall 0 r)ᶜ ⊆ f ⁻¹' s
Tactic: use r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (hypothesis)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 r)ᶜ x
⊢ x ∈ f ⁻¹' s
have hx₁ : r < ‖x‖
Tactic: simp only [Set.mem_compl_iff, Metric.mem_closedBall, dist_zero_right, not_le] at hx
Cleared hypotheses: hx