awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x : E
f : Filter E
⊢ Disjoint (𝓝 x) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y⁻¹ * x‖

Tactic:
simp [NormedGroup.nhds_basis_norm_lt x |>.disjoint_iff_left, compl_setOf, eventually_iff]

Premises used: Filter.eventually_iff, Filter.HasBasis.disjoint_iff_left, Set.compl_setOf, NormedGroup.nhds_basis_norm_lt
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
f : Filter E
⊢ Disjoint (𝓝 1) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖

Tactic:
simpa using disjoint_nhds 1 f

Premises used: SeminormedGroup.disjoint_nhds, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : FunLike 𝓕 E F
inst_1 : Group E
inst_2 : SeminormedGroup F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
x y : E
simp : dist x y = dist.{u_6} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)
⊢ dist x y = norm.{u_6} (E := F) ((f : (a : E) → F) (x⁻¹ * y) : F)

Tactic:
simp only [map_mul, map_inv, ← dist_eq_norm_inv_mul]

Premises used: map_inv, dist_eq_norm_inv_mul, map_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : FunLike 𝓕 E F
inst_1 : Group E
inst_2 : SeminormedGroup F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
x y : E
⊢ dist x y = dist.{u_6} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
rw : ‖b⁻¹ * a‖ = ‖a / b‖
rw₁ rw₂ : ‖b⁻¹ * a‖ = ‖b⁻¹ * a‖
⊢ dist a b = ‖a / b‖

Tactic:
rw [dist_eq_norm_inv_mul', div_eq_inv_mul]

Premises used: dist_eq_norm_inv_mul', div_eq_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
rw : ‖a⁻¹ * b‖ = ‖b / a‖
rw₁ rw₂ : ‖a⁻¹ * b‖ = ‖a⁻¹ * b‖
⊢ dist a b = ‖b / a‖

Tactic:
rw [dist_eq_norm_inv_mul, div_eq_inv_mul]

Premises used: dist_eq_norm_inv_mul, div_eq_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
rw : dist a b = ‖a / b‖
rw₁ rw₂ : ‖a / b‖ = ‖a / b‖
⊢ ‖a⁻¹ * b‖ = ‖a / b‖

Tactic:
rw [← dist_eq_norm_inv_mul, dist_eq_norm_div]

Premises used: dist_eq_norm_inv_mul, dist_eq_norm_div
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
⊢ |‖a‖ - ‖b‖| ≤ ‖a / b‖

Tactic:
(abs_norm_sub_norm_le_norm_inv_mul a b).trans_eq (norm_inv_mul a b)

Premises used: LE.le.trans_eq, abs_norm_sub_norm_le_norm_inv_mul, norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
⊢ ‖a‖ - ‖b‖ ≤ ‖a / b‖

Tactic:
(le_abs_self _).trans (abs_norm_sub_norm_le' a b)

Premises used: le_abs_self, abs_norm_sub_norm_le', LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
⊢ dist ‖a‖ ‖b‖ ≤ ‖a / b‖

Tactic:
abs_norm_sub_norm_le' a b

Premises used: abs_norm_sub_norm_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
⊢ nndist ‖a‖₊ ‖b‖₊ ≤ ‖a / b‖₊

Tactic:
NNReal.coe_le_coe.1 <| dist_norm_norm_le' a b

Premises used: Iff.mp, dist_norm_norm_le', NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
⊢ nndist a b = ‖a / b‖₊

Tactic:
NNReal.eq <| dist_eq_norm_div _ _

Premises used: NNReal.eq, dist_eq_norm_div
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
rw : ENNReal.ofReal (dist a b) = ‖a / b‖ₑ
rw₁ : ENNReal.ofReal ‖a / b‖ = ‖a / b‖ₑ
rw₂ rw₃ : ‖a / b‖ₑ = ‖a / b‖ₑ
⊢ edist a b = ‖a / b‖ₑ

Tactic:
rw [edist_dist, dist_eq_norm_div, ofReal_norm']

Premises used: ofReal_norm', edist_dist, dist_eq_norm_div
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
x y : E
simp_rw : ‖x⁻¹⁻¹ * y‖ = ‖x⁻¹ * y⁻¹‖
simp_rw₁ : ‖x⁻¹⁻¹ * y‖ = ‖(x⁻¹ * y⁻¹)⁻¹‖
simp_rw₂ : ‖x⁻¹⁻¹ * y‖ = ‖x⁻¹⁻¹ * y⁻¹⁻¹‖
⊢ dist x⁻¹ y = dist x y⁻¹

Tactic:
simp_rw [dist_eq_norm_inv_mul, ← norm_inv' (x⁻¹ * y⁻¹), mul_inv, inv_inv]

Premises used: HMul.hMul, mul_inv, dist_eq_norm_inv_mul, norm_inv', Inv.inv, inv_inv
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_9
inst : SeminormedAddCommGroup E
m : Multiset E
⊢ ‖m.sum‖ ≤ Multiset.sum (Multiset.map (fun (x : E) ↦ ‖x‖) m)

Tactic:
m.le_sum_of_subadditive norm norm_zero.le norm_add_le

Premises used: Norm.norm, Multiset.le_sum_of_subadditive
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ε : Type u_9
inst : TopologicalSpace ε
inst_1 : ESeminormedAddCommMonoid ε
m : Multiset ε
⊢ ‖m.sum‖ₑ ≤ Multiset.sum (Multiset.map (fun (x : ε) ↦ ‖x‖ₑ) m)

Tactic:
m.le_sum_of_subadditive enorm enorm_zero.le enorm_add_le

Premises used: ENorm.enorm, Multiset.le_sum_of_subadditive
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
m : Multiset E
⊢ ‖m.prod‖ ≤ Multiset.sum (Multiset.map (fun (x : E) ↦ ‖x‖) m)

Tactic:
m.apply_prod_le_sum_map _ norm_one'.le norm_mul_le'

Premises used: norm_one', Eq.le, Multiset.apply_prod_le_sum_map, norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ε : Type u_9
inst : TopologicalSpace ε
inst_1 : ESeminormedCommMonoid ε
m : Multiset ε
⊢ ‖m.prod‖ₑ ≤ Multiset.sum (Multiset.map (fun (x : ε) ↦ ‖x‖ₑ) m)

Tactic:
m.apply_prod_le_sum_map _ enorm_one'.le enorm_mul_le'

Premises used: Eq.le, Multiset.apply_prod_le_sum_map, enorm_one', enorm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
ε : Type u_9
inst : TopologicalSpace ε
inst_1 : ESeminormedAddCommMonoid ε
s : Finset ι
f : ι → ε
⊢ enorm.{u_9} (E := ε) (∑ i ∈ s, f i) ≤ ∑ i ∈ s, ‖f i‖ₑ

Tactic:
s.le_sum_of_subadditive enorm enorm_zero.le enorm_add_le f

Premises used: Finset.le_sum_of_subadditive, ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_9
inst : SeminormedAddCommGroup E
s : Finset ι
f : ι → E
⊢ norm.{u_9} (E := E) (∑ i ∈ s, f i) ≤ ∑ i ∈ s, ‖f i‖

Tactic:
s.le_sum_of_subadditive norm norm_zero.le norm_add_le f

Premises used: Norm.norm, Finset.le_sum_of_subadditive
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedCommMonoid ε
s : Finset ι
f : ι → ε
⊢ enorm.{u_8} (E := ε) (∏ i ∈ s, f i) ≤ ∑ i ∈ s, ‖f i‖ₑ

Tactic:
s.apply_prod_le_sum_apply _ enorm_one'.le enorm_mul_le'

Premises used: Finset.apply_prod_le_sum_apply, Eq.le, enorm_one', enorm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ norm.{u_5} (E := E) (∏ i ∈ s, f i) ≤ ∑ i ∈ s, ‖f i‖

Tactic:
s.apply_prod_le_sum_apply _ norm_one'.le norm_mul_le'

Premises used: Finset.apply_prod_le_sum_apply, norm_one', Eq.le, norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedCommMonoid ε
s : Finset ι
f : ι → ε
n : ι → ℝ≥0∞
h : ∀ b ∈ s, ‖f b‖ₑ ≤ n b
⊢ enorm.{u_8} (E := ε) (∏ b ∈ s, f b) ≤ ∑ b ∈ s, n b

Tactic:
(enorm_prod_le s f).trans <| Finset.sum_le_sum h

Premises used: enorm_prod_le, Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f : ι → E
n : ι → ℝ
h : ∀ b ∈ s, ‖f b‖ ≤ n b
⊢ norm.{u_5} (E := E) (∏ b ∈ s, f b) ≤ ∑ b ∈ s, n b

Tactic:
(norm_prod_le s f).trans <| Finset.sum_le_sum h

Premises used: norm_prod_le, Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, dist (f b) (a b) ≤ d b
⊢ ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b

Tactic:
simp_rw [dist_eq_norm_inv_mul] at h

Premises used: dist_eq_norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b
rw : norm.{u_5} (E := E) (∏ x ∈ s, (f x)⁻¹ * a x) ≤ ∑ b ∈ s, d b
⊢ dist.{u_5} (α := E) (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b

Tactic:
rw [dist_eq_norm_inv_mul, ← Finset.prod_inv_distrib, ← Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, dist_eq_norm_inv_mul, Finset.prod_inv_distrib
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b
⊢ norm.{u_5} (E := E) (∏ x ∈ s, (f x)⁻¹ * a x) ≤ ∑ b ∈ s, d b

Tactic:
norm_prod_le_of_le s h

Premises used: norm_prod_le_of_le
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b
⊢ norm.{u_5} (E := E) (∏ x ∈ s, (f x)⁻¹ * a x) ≤ ∑ b ∈ s, d b

Tactic:
exact norm_prod_le_of_le s h

Premises used: norm_prod_le_of_le
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f a : ι → E
⊢ dist.{u_5} (α := E) (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b)

Tactic:
dist_prod_prod_le_of_le s fun _ _ => le_rfl

Premises used: le_rfl, dist_prod_prod_le_of_le
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
y : E
ε : ℝ
simp_rw : Eq.{u_5 + 1} (α := Set E) {x : E | ‖x⁻¹ * y‖ < ε} {x : E | ‖x / y‖ < ε}
⊢ ball y ε = {x : E | ‖x / y‖ < ε}

Tactic:
simp_rw [ball_eq_norm_inv_mul_lt, norm_inv_mul]

Premises used: ball_eq_norm_inv_mul_lt, norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
rw : dist b a < r ↔ ‖b / a‖ < r
rw₁ rw₂ : ‖b / a‖ < r ↔ ‖b / a‖ < r
⊢ b ∈ ball a r ↔ ‖b / a‖ < r

Tactic:
rw [mem_ball, dist_eq_norm_div]

Premises used: Metric.mem_ball, dist_eq_norm_div
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
rw : dist a b < r ↔ ‖a / b‖ < r
rw₁ rw₂ : ‖a / b‖ < r ↔ ‖a / b‖ < r
⊢ b ∈ ball a r ↔ ‖a / b‖ < r

Tactic:
rw [mem_ball', dist_eq_norm_div]

Premises used: dist_eq_norm_div, Metric.mem_ball'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
rw : dist b a ≤ r ↔ ‖b / a‖ ≤ r
rw₁ rw₂ : ‖b / a‖ ≤ r ↔ ‖b / a‖ ≤ r
⊢ b ∈ closedBall a r ↔ ‖b / a‖ ≤ r

Tactic:
rw [mem_closedBall, dist_eq_norm_div]

Premises used: dist_eq_norm_div, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
rw : dist a b ≤ r ↔ ‖a / b‖ ≤ r
rw₁ rw₂ : ‖a / b‖ ≤ r ↔ ‖a / b‖ ≤ r
⊢ b ∈ closedBall a r ↔ ‖a / b‖ ≤ r

Tactic:
rw [mem_closedBall', dist_eq_norm_div]

Premises used: Metric.mem_closedBall', dist_eq_norm_div
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ sphere a r ↔ ‖b / a‖ = r

Tactic:
simp [dist_eq_norm_div]

Premises used: dist_eq_norm_div
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
rw : ‖a * b / a‖ < r ↔ ‖b‖ < r
⊢ a * b ∈ ball a r ↔ ‖b‖ < r

Tactic:
rw [mem_ball_iff_norm'']

Premises used: mem_ball_iff_norm''
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ ‖a * b / a‖ < r ↔ ‖b‖ < r

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
rw : ‖a * b / a‖ ≤ r ↔ ‖b‖ ≤ r
⊢ a * b ∈ closedBall a r ↔ ‖b‖ ≤ r

Tactic:
rw [mem_closedBall_iff_norm'']

Premises used: mem_closedBall_iff_norm''
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
⊢ ‖a * b / a‖ ≤ r ↔ ‖b‖ ≤ r

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
h : ∀ (c : E), Membership.mem (γ := Set E) ((fun (x : E) ↦ b * x) ⁻¹' ball a r) c ↔ c ∈ ball (a / b) r
⊢ (fun (x : E) ↦ b * x) ⁻¹' ball a r = ball (a / b) r

Tactic:
ext c
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ b * x) ⁻¹' ball a r) c ↔ c ∈ ball (a / b) r

Tactic:
simp [dist_eq_norm_inv_mul, Set.mem_preimage, mem_ball, div_eq_mul_inv, mul_comm, mul_assoc]

Premises used: mul_assoc, dist_eq_norm_inv_mul, div_eq_mul_inv, Metric.mem_ball, mul_comm, Set.mem_preimage
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
h : ∀ (c : E), Membership.mem (γ := Set E) ((fun (x : E) ↦ b * x) ⁻¹' closedBall a r) c ↔ c ∈ closedBall (a / b) r
⊢ (fun (x : E) ↦ b * x) ⁻¹' closedBall a r = closedBall (a / b) r

Tactic:
ext c
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ b * x) ⁻¹' closedBall a r) c ↔ c ∈ closedBall (a / b) r

Tactic:
simp [dist_eq_norm_inv_mul, Set.mem_preimage, mem_closedBall, div_eq_mul_inv, mul_comm, mul_assoc]

Premises used: mul_assoc, dist_eq_norm_inv_mul, div_eq_mul_inv, mul_comm, Metric.mem_closedBall, Set.mem_preimage
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
h : ∀ (c : E), Membership.mem (γ := Set E) ((fun (x : E) ↦ b * x) ⁻¹' sphere a r) c ↔ c ∈ sphere (a / b) r
⊢ (fun (x : E) ↦ b * x) ⁻¹' sphere a r = sphere (a / b) r

Tactic:
ext c
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ b * x) ⁻¹' sphere a r) c ↔ c ∈ sphere (a / b) r

Tactic:
simp only [Set.mem_preimage, mem_sphere_iff_norm', div_div_eq_mul_div, mul_comm]

Premises used: mem_sphere_iff_norm', div_div_eq_mul_div, mul_comm, Set.mem_preimage
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : a ∈ closedBall b r
simp : ∀ (h : ‖a⁻¹ * b‖ ≤ r), ‖(a⁻¹ * b) ^ n‖ ≤ n • r
⊢ a ^ n ∈ closedBall (b ^ n) (n • r)

Tactic:
simp only [mem_closedBall, dist_eq_norm_inv_mul, ← inv_pow, ← mul_pow] at h ⊢

Premises used: dist_eq_norm_inv_mul, inv_pow, Metric.mem_closedBall, mul_pow
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ ≤ r
⊢ ‖(a⁻¹ * b) ^ n‖ ≤ n • r

Tactic:
norm_pow_le_mul_norm.trans ?_

Premises used: norm_pow_le_mul_norm, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ ≤ r
refine : (↑n : ℝ) * ‖a⁻¹ * b‖ ≤ n • r
⊢ ‖(a⁻¹ * b) ^ n‖ ≤ n • r

Tactic:
refine norm_pow_le_mul_norm.trans ?_

Premises used: norm_pow_le_mul_norm, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ ≤ r
⊢ (↑n : ℝ) * ‖a⁻¹ * b‖ ≤ n • r

Tactic:
simpa only [nsmul_eq_mul] using mul_le_mul_of_nonneg_left h n.cast_nonneg

Premises used: Nat.cast_nonneg, nsmul_eq_mul, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : a ∈ ball b r
simp : ∀ (h : ‖a⁻¹ * b‖ < r), ‖(a⁻¹ * b) ^ n‖ < n • r
⊢ a ^ n ∈ ball (b ^ n) (n • r)

Tactic:
simp only [mem_ball, dist_eq_norm_inv_mul, ← inv_pow, ← mul_pow] at h ⊢

Premises used: dist_eq_norm_inv_mul, inv_pow, Metric.mem_ball, mul_pow
-- Module: Mathlib.Analysis.Normed.Group.Basic
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

Tactic:
lt_of_le_of_lt norm_pow_le_mul_norm ?_

Premises used: lt_of_le_of_lt, norm_pow_le_mul_norm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a⁻¹ * b‖ < r
refine : (↑n : ℝ) * ‖a⁻¹ * b‖ < n • r
⊢ ‖(a⁻¹ * b) ^ n‖ < n • r

Tactic:
refine lt_of_le_of_lt norm_pow_le_mul_norm ?_

Premises used: lt_of_le_of_lt, norm_pow_le_mul_norm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a⁻¹ * b‖ < r
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < n
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
hn : 0 < n
h : ‖a⁻¹ * b‖ < r
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
replace hn : 0 < (n : ℝ) := by norm_cast
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ < r
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑n : ℝ) * ‖a⁻¹ * b‖ < (↑n : ℝ) * r
⊢ (↑n : ℝ) * ‖a⁻¹ * b‖ < n • r

Tactic:
rw [nsmul_eq_mul]

Premises used: nsmul_eq_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
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
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
⊢ (↑n : ℝ) * ‖a⁻¹ * b‖ < (↑n : ℝ) * r

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
c : E
simp : ‖b * c * (a * c)⁻¹‖ ≤ r ↔ ‖b * a⁻¹‖ ≤ r
⊢ a * c ∈ closedBall (b * c) r ↔ a ∈ closedBall b r

Tactic:
simp only [mem_closedBall, dist_eq_norm_inv_mul, mul_comm _ (b * c), mul_comm a⁻¹ b]

Premises used: HMul.hMul, dist_eq_norm_inv_mul, Inv.inv, mul_comm, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ ‖b * c * (a * c)⁻¹‖ ≤ r ↔ ‖b * a⁻¹‖ ≤ r

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
c : E
simp : ‖b * c * (a * c)⁻¹‖ < r ↔ ‖b * a⁻¹‖ < r
⊢ a * c ∈ ball (b * c) r ↔ a ∈ ball b r

Tactic:
simp only [mem_ball, dist_eq_norm_inv_mul, mul_comm _ (b * c), mul_comm a⁻¹ b]

Premises used: HMul.hMul, dist_eq_norm_inv_mul, Metric.mem_ball, Inv.inv, mul_comm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ ‖b * c * (a * c)⁻¹‖ < r ↔ ‖b * a⁻¹‖ < r

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
h : ∀ (x : E), x ∈ a • closedBall b r ↔ x ∈ closedBall (a • b) r
⊢ a • closedBall b r = closedBall (a • b) r

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
x : E
⊢ x ∈ a • closedBall b r ↔ x ∈ closedBall (a • b) r

Tactic:
simp [mem_closedBall, Set.mem_smul_set, dist_eq_norm_inv_mul, ← eq_inv_mul_iff_mul_eq, mul_assoc]

Premises used: mul_assoc, Set.mem_smul_set, dist_eq_norm_inv_mul, eq_inv_mul_iff_mul_eq, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
h : ∀ (x : E), x ∈ a • ball b r ↔ x ∈ ball (a • b) r
⊢ a • ball b r = ball (a • b) r

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
a b : E
r : ℝ
x : E
⊢ x ∈ a • ball b r ↔ x ∈ ball (a • b) r

Tactic:
simp [mem_ball, Set.mem_smul_set, dist_eq_norm_inv_mul, ← eq_inv_mul_iff_mul_eq, mul_assoc]

Premises used: mul_assoc, Set.mem_smul_set, dist_eq_norm_inv_mul, eq_inv_mul_iff_mul_eq, Metric.mem_ball
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
m : Multiset E
push_cast : ‖m.prod‖ ≤ (Multiset.map toReal (Multiset.map (fun (x : E) ↦ ‖x‖₊) m)).sum
⊢ (↑‖m.prod‖₊ : ℝ) ≤ (↑(Multiset.sum (Multiset.map (fun (x : E) ↦ ‖x‖₊) m)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
m : Multiset E
rw : ‖m.prod‖ ≤ (Multiset.map (toReal ∘ fun (x : E) ↦ ‖x‖₊) m).sum
⊢ ‖m.prod‖ ≤ (Multiset.map toReal (Multiset.map (fun (x : E) ↦ ‖x‖₊) m)).sum

Tactic:
rw [Multiset.map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
m : Multiset E
⊢ ‖m.prod‖ ≤ (Multiset.map (toReal ∘ fun (x : E) ↦ ‖x‖₊) m).sum

Tactic:
norm_multiset_prod_le _

Premises used: norm_multiset_prod_le, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
m : Multiset E
⊢ ‖m.prod‖ ≤ (Multiset.map (toReal ∘ fun (x : E) ↦ ‖x‖₊) m).sum

Tactic:
exact norm_multiset_prod_le _

Premises used: norm_multiset_prod_le
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f : ι → E
push_cast : norm.{u_5} (E := E) (∏ a ∈ s, f a) ≤ ∑ x ∈ s, ‖f x‖
⊢ (↑(nnnorm.{u_5} (E := E) (∏ a ∈ s, f a)) : ℝ) ≤ (↑(∑ a ∈ s, ‖f a‖₊) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ norm.{u_5} (E := E) (∏ a ∈ s, f a) ≤ ∑ x ∈ s, ‖f x‖

Tactic:
norm_prod_le _ _

Premises used: norm_prod_le
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ norm.{u_5} (E := E) (∏ a ∈ s, f a) ≤ ∑ x ∈ s, ‖f x‖

Tactic:
exact norm_prod_le _ _

Premises used: norm_prod_le
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
ι : Type u_3
E : Type u_5
inst : SeminormedCommGroup E
s : Finset ι
f : ι → E
n : ι → ℝ≥0
h : ∀ b ∈ s, ‖f b‖₊ ≤ n b
⊢ nnnorm.{u_5} (E := E) (∏ b ∈ s, f b) ≤ ∑ b ∈ s, n b

Tactic:
(norm_prod_le_of_le s h).trans_eq (NNReal.coe_sum ..).symm

Premises used: norm_prod_le_of_le, LE.le.trans_eq, NNReal.coe_sum, Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
f : E → F
x : E
y : F
⊢ Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε

Tactic:
simpa [norm_inv_mul] using NormedGroup.tendsto_nhds_nhds (f := f) (x := x) (y := y)

Premises used: NormedGroup.tendsto_nhds_nhds, norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
x : E
⊢ (𝓝 x).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {y : E | ‖y / x‖ < ε}

Tactic:
simpa [norm_inv_mul] using NormedGroup.nhds_basis_norm_lt x

Premises used: norm_inv_mul, NormedGroup.nhds_basis_norm_lt
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedCommGroup E
⊢ (𝓤 E).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {p : E × E | ‖p.1 / p.2‖ < ε}

Tactic:
simpa [norm_inv_mul] using NormedGroup.uniformity_basis_dist (E := E)

Premises used: NormedGroup.uniformity_basis_dist, norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a : E
rw : dist a 1 ≤ 0 ↔ a = 1
rw₁ rw₂ : a = 1 ↔ a = 1
⊢ ‖a‖ ≤ 0 ↔ a = 1

Tactic:
rw [← dist_one_right, dist_le_zero]

Premises used: dist_le_zero, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a : E
rw : ¬‖a‖ ≤ 0 ↔ a ≠ 1
rw₁ rw₂ : ¬a = 1 ↔ a ≠ 1
⊢ 0 < ‖a‖ ↔ a ≠ 1

Tactic:
rw [← not_le, norm_le_zero_iff']

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

Tactic:
(norm_nonneg' a).ge_iff_eq'.symm.trans norm_le_zero_iff'

Premises used: norm_nonneg', LE.le.ge_iff_eq', Iff.trans, norm_le_zero_iff', Iff.symm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a : E
⊢ ‖a‖ ≠ 0 ↔ a ≠ 1

Tactic:
norm_eq_zero'.not

Premises used: norm_eq_zero', Iff.not
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : NormedGroup E
a b : E
rw : a / b = 1 ↔ a = b
rw₁ rw₂ : a = b ↔ a = b
⊢ ‖a / b‖ = 0 ↔ a = b

Tactic:
rw [norm_eq_zero', div_eq_one]

Premises used: norm_eq_zero', div_eq_one