awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : SeminormedCommGroup E
u v : E
rw : ‖u * v‖ - ‖u / v‖ ≤ min (2 * ‖u‖) (2 * ‖v‖)
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * min ‖u‖ ‖v‖

Tactic:
rw [mul_min_of_nonneg _ _ (by positivity)]

Premises used: mul_min_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : SeminormedCommGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ min (2 * ‖u‖) (2 * ‖v‖)

Tactic:
le_min ?_ (norm_mul_sub_norm_div_le_two_mul u v)

Premises used: le_min, norm_mul_sub_norm_div_le_two_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : SeminormedCommGroup E
u v : E
refine : ‖u * v‖ - ‖u / v‖ ≤ 2 * ‖u‖
⊢ ‖u * v‖ - ‖u / v‖ ≤ min (2 * ‖u‖) (2 * ‖v‖)

Tactic:
refine le_min ?_ (norm_mul_sub_norm_div_le_two_mul u v)

Premises used: le_min, norm_mul_sub_norm_div_le_two_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : SeminormedCommGroup E
u v : E
rw : ‖v * u‖ - ‖v / u‖ ≤ 2 * ‖u‖
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * ‖u‖

Tactic:
rw [norm_div_rev, mul_comm]

Premises used: mul_comm, norm_div_rev
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : SeminormedCommGroup E
u v : E
⊢ ‖v * u‖ - ‖v / u‖ ≤ 2 * ‖u‖

Tactic:
norm_mul_sub_norm_div_le_two_mul _ _

Premises used: norm_mul_sub_norm_div_le_two_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : SeminormedCommGroup E
u v : E
⊢ ‖v * u‖ - ‖v / u‖ ≤ 2 * ‖u‖

Tactic:
exact norm_mul_sub_norm_div_le_two_mul _ _

Premises used: norm_mul_sub_norm_div_le_two_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ sphere a r ↔ ‖b⁻¹ * a‖ = r

Tactic:
simp [dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
r : ℝ
⊢ Membership.mem (γ := Set E) (sphere 1 r) a ↔ ‖a‖ = r

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
r : ℝ
x : (↑(sphere 1 r) : Type u_5)
⊢ ‖(↑x : E)‖ = r

Tactic:
mem_sphere_one_iff_norm.mp x.2

Premises used: mem_sphere_one_iff_norm, Iff.mp, Subtype.property
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
r : ℝ
hr : r ≠ 0
x : (↑(sphere 1 r) : Type u_5)
rwa rwa₁ rwa₂ rwa₃ : r ≠ 0
⊢ ‖(↑x : E)‖ ≠ 0

Tactic:
rwa [norm_eq_of_mem_sphere' x]

Premises used: norm_eq_of_mem_sphere'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x : (↑(sphere 1 1) : Type u_5)
⊢ (↑x : E) ≠ 1

Tactic:
ne_one_of_mem_sphere one_ne_zero _

Premises used: ne_one_of_mem_sphere, one_ne_zero
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ Eq (α := (a : E) → ℝ) (⇑(normGroupSeminorm E) : (a : E) → ℝ) norm

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
f : α → E
l : Filter α
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, dist (f x) 1 < ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε

Tactic:
simp only [dist_one_right]

Premises used: dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
f : E → F
x : E
y : F
simp_rw :
  (∀ ε > 0, ∃ δ > 0, ∀ ⦃x_1 : E⦄, dist x_1 x < δ → dist (f x_1) y < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x'⁻¹ * x‖ < δ → ‖(f x')⁻¹ * y‖ < ε
⊢ Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x'⁻¹ * x‖ < δ → ‖(f x')⁻¹ * y‖ < ε

Tactic:
simp_rw [Metric.tendsto_nhds_nhds, dist_eq_norm_inv_mul]

Premises used: Metric.tendsto_nhds_nhds, dist_eq_norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x : E
simp_rw : (𝓝 x).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ ball x ε
⊢ (𝓝 x).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {y : E | ‖y⁻¹ * x‖ < ε}

Tactic:
simp_rw [← ball_eq_norm_inv_mul_lt]

Premises used: ball_eq_norm_inv_mul_lt
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x : E
⊢ (𝓝 x).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ ball x ε

Tactic:
Metric.nhds_basis_ball

Premises used: Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x : E
⊢ (𝓝 x).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ ball x ε

Tactic:
exact Metric.nhds_basis_ball

Premises used: Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ HasBasis.{u_5, 1} (α := E) (𝓝 1) (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {y : E | ‖y⁻¹ * 1‖ < ε}

Tactic:
NormedGroup.nhds_basis_norm_lt (1 : E)

Premises used: OfNat.ofNat, NormedGroup.nhds_basis_norm_lt
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
h : Eq.{u_5 + 1} (α := ℝ → Set E) (fun (ε : ℝ) ↦ {y : E | ‖y‖ < ε}) fun (ε : ℝ) ↦ {y : E | ‖y⁻¹ * 1‖ < ε}
⊢ HasBasis.{u_5, 1} (α := E) (𝓝 1) (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {y : E | ‖y‖ < ε}

Tactic:
convert! NormedGroup.nhds_basis_norm_lt (1 : E) using 1

Premises used: OfNat.ofNat, NormedGroup.nhds_basis_norm_lt
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ Eq.{u_5 + 1} (α := ℝ → Set E) (fun (ε : ℝ) ↦ {y : E | ‖y‖ < ε}) fun (ε : ℝ) ↦ {y : E | ‖y⁻¹ * 1‖ < ε}

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ (𝓤 E).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {p : E × E | dist p.1 p.2 < ε}

Tactic:
Metric.uniformity_basis_dist (α := E)

Premises used: Metric.uniformity_basis_dist
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
h :
  Eq.{u_5 + 1} (α := ℝ → Set (E × E)) (fun (ε : ℝ) ↦ {p : E × E | ‖p.1⁻¹ * p.2‖ < ε}) fun (ε : ℝ) ↦
    {p : E × E | dist p.1 p.2 < ε}
⊢ (𝓤 E).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {p : E × E | ‖p.1⁻¹ * p.2‖ < ε}

Tactic:
convert! Metric.uniformity_basis_dist (α := E) using 1

Premises used: Metric.uniformity_basis_dist
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ Eq.{u_5 + 1} (α := ℝ → Set (E × E)) (fun (ε : ℝ) ↦ {p : E × E | ‖p.1⁻¹ * p.2‖ < ε}) fun (ε : ℝ) ↦
    {p : E × E | dist p.1 p.2 < ε}

Tactic:
simp [dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ (↑‖a‖₊ : ℝ) = ‖a‖

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ Eq.{u_5 + 1} (α := E → ℝ) (toReal ∘ nnnorm) norm

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ ‖a‖.toNNReal = ‖a‖₊

Tactic:
@Real.toNNReal_coe ‖a‖₊

Premises used: Real.toNNReal_coe, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x : E
⊢ ‖x‖ₑ.toReal = ‖x‖

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x : E
⊢ ENNReal.ofReal ‖x‖ = ‖x‖ₑ

Tactic:
ENNReal.ofReal_eq_coe_nnreal _

Premises used: ENNReal.ofReal_eq_coe_nnreal
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
simp : ENNReal.ofReal ‖x‖ = ENNReal.ofReal ‖y‖ ↔ ‖x‖ = ‖y‖
⊢ ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖

Tactic:
simp only [← ofReal_norm']

Premises used: ofReal_norm'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
h : ‖x‖ = ‖y‖
⊢ ENNReal.ofReal ‖x‖ = ENNReal.ofReal ‖y‖

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
refine : ∀ (h : ENNReal.ofReal ‖x‖ = ENNReal.ofReal ‖y‖), ‖x‖ = ‖y‖
⊢ ENNReal.ofReal ‖x‖ = ENNReal.ofReal ‖y‖ ↔ ‖x‖ = ‖y‖

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by congr⟩
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
h : ENNReal.ofReal ‖x‖ = ENNReal.ofReal ‖y‖
⊢ ‖x‖ = ‖y‖

Tactic:
(Real.toNNReal_eq_toNNReal_iff (norm_nonneg' _) (norm_nonneg' _)).mp (ENNReal.coe_inj.mp h)

Premises used: norm_nonneg', ENNReal.coe_inj, Iff.mp, Real.toNNReal_eq_toNNReal_iff
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
h : ENNReal.ofReal ‖x‖ = ENNReal.ofReal ‖y‖
⊢ ‖x‖ = ‖y‖

Tactic:
exact (Real.toNNReal_eq_toNNReal_iff (norm_nonneg' _) (norm_nonneg' _)).mp (ENNReal.coe_inj.mp h)

Premises used: norm_nonneg', ENNReal.coe_inj, Iff.mp, Real.toNNReal_eq_toNNReal_iff
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
simp : ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖ ↔ ‖x‖ ≤ ‖y‖
⊢ ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖

Tactic:
simp only [← ofReal_norm']

Premises used: ofReal_norm'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
h : ‖x‖ ≤ ‖y‖
⊢ ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
refine : ∀ (h : ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖), ‖x‖ ≤ ‖y‖
⊢ ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖ ↔ ‖x‖ ≤ ‖y‖

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by gcongr⟩
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
h : ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
rw [ENNReal.ofReal_le_ofReal_iff (norm_nonneg' _)] at h

Premises used: ENNReal.ofReal_le_ofReal_iff, norm_nonneg'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
h : ‖x‖ ≤ ‖y‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
h
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
F : Type u_6
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
h : ‖x‖ ≤ ‖y‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
exact h
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ nndist a b = ‖a⁻¹ * b‖₊

Tactic:
NNReal.eq <| dist_eq_norm_inv_mul _ _

Premises used: dist_eq_norm_inv_mul, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ ‖a⁻¹‖₊ = ‖a‖₊

Tactic:
NNReal.eq <| norm_inv' a

Premises used: NNReal.eq, norm_inv'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ nndist a 1 = ‖a‖₊

Tactic:
simp [nndist_eq_nnnorm_inv_mul]

Premises used: nndist_eq_nnnorm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ edist a 1 = ‖a‖ₑ

Tactic:
simp [edist_nndist, nndist_one_right, enorm]

Premises used: ENorm.enorm, edist_nndist, nndist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ nnnorm.{u_5} (E := E) 1 = 0

Tactic:
NNReal.eq norm_one'

Premises used: norm_one', NNReal.eq
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ nnnorm.{u_5} (E := E) 1 = 0

Tactic:
nnnorm_one'

Premises used: nnnorm_one'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ nnnorm.{u_5} (E := E) 1 = 0

Tactic:
exact nnnorm_one'

Premises used: nnnorm_one'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊

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

Premises used: Iff.mp, NNReal.coe_le_coe, norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ ‖HPow.hPow (β := ℕ) a 0‖ ≤ (↑0 : ℝ) * ‖a‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℕ
⊢ ‖a ^ (n + 1)‖ ≤ (↑(n + 1) : ℝ) * ‖a‖

Tactic:
simpa [pow_succ, add_mul] using norm_mul_le_of_le' norm_pow_le_mul_norm le_rfl

Premises used: add_mul, le_rfl, pow_succ, norm_mul_le_of_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℕ
⊢ ‖a ^ n‖₊ ≤ (↑n : ℝ≥0) * ‖a‖₊

Tactic:
simpa only [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_natCast] using norm_pow_le_mul_norm

Premises used: norm_pow_le_mul_norm, NNReal.coe_natCast, NNReal.coe_mul, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ |n|‖₊ = ‖a ^ n‖₊

Tactic:
NNReal.eq <| norm_zpow_abs a n

Premises used: norm_zpow_abs, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ n.natAbs‖₊ = ‖a ^ n‖₊

Tactic:
NNReal.eq <| norm_pow_natAbs a n

Premises used: norm_pow_natAbs, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
n : ℤ
hn : IsUnit n
⊢ ‖a ^ n‖₊ = ‖a‖₊

Tactic:
NNReal.eq <| norm_zpow_isUnit a hn

Premises used: norm_zpow_isUnit, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : SeminormedAddGroup E
n : ℤˣ
a : E
⊢ ‖n • a‖₊ = ‖a‖₊

Tactic:
NNReal.eq <| norm_isUnit_zsmul a n.isUnit

Premises used: NNReal.eq, norm_isUnit_zsmul, Units.isUnit
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ nndist 1 a = ‖a‖₊

Tactic:
simp [nndist_eq_nnnorm_inv_mul]

Premises used: nndist_eq_nnnorm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
rw : (↑(nndist 1 a) : ℝ≥0∞) = (↑‖a‖₊ : ℝ≥0∞)
rw₁ rw₂ : (↑‖a‖₊ : ℝ≥0∞) = (↑‖a‖₊ : ℝ≥0∞)
⊢ edist 1 a = (↑‖a‖₊ : ℝ≥0∞)

Tactic:
rw [edist_nndist, nndist_one_left]

Premises used: nndist_one_left, edist_nndist
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ nndist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖₊

Tactic:
NNReal.eq <| dist_mulIndicator s t f x

Premises used: NNReal.eq, dist_mulIndicator
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖a / b‖₊ ≤ ‖a‖₊ + ‖b‖₊

Tactic:
NNReal.coe_le_coe.1 <| norm_div_le _ _

Premises used: norm_div_le, Iff.mp, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖a / b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

Tactic:
simpa [enorm, ← ENNReal.coe_add] using nnnorm_div_le a b

Premises used: ENNReal.coe_add, ENorm.enorm, nnnorm_div_le
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ nndist ‖a‖₊ ‖b‖₊ ≤ ‖a⁻¹ * b‖₊

Tactic:
NNReal.coe_le_coe.1 <| dist_norm_norm_le_norm_inv_mul a b

Premises used: Iff.mp, dist_norm_norm_le_norm_inv_mul, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖b‖₊ ≤ ‖a‖₊ + ‖a / b‖₊

Tactic:
norm_le_norm_add_norm_div _ _

Premises used: norm_le_norm_add_norm_div
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖a‖₊ ≤ ‖b‖₊ + ‖a / b‖₊

Tactic:
norm_le_norm_add_norm_div' _ _

Premises used: norm_le_norm_add_norm_div'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖a‖₊ ≤ ‖a * b‖₊ + ‖b‖₊

Tactic:
norm_le_mul_norm_add _ _

Premises used: norm_le_mul_norm_add
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a b : E
⊢ ‖b‖₊ ≤ ‖a * b‖₊ + ‖a‖₊

Tactic:
norm_le_mul_norm_add' _ _

Premises used: norm_le_mul_norm_add'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖x‖₊ = 0
⊢ ‖x * y‖₊ = ‖y‖₊

Tactic:
NNReal.eq <| norm_mul_eq_norm_right _ <| congr_arg NNReal.toReal h

Premises used: norm_mul_eq_norm_right, NNReal.eq, congr_arg, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖y‖₊ = 0
⊢ ‖x * y‖₊ = ‖x‖₊

Tactic:
NNReal.eq <| norm_mul_eq_norm_left _ <| congr_arg NNReal.toReal h

Premises used: NNReal.eq, norm_mul_eq_norm_left, congr_arg, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖x‖₊ = 0
⊢ ‖x / y‖₊ = ‖y‖₊

Tactic:
NNReal.eq <| norm_div_eq_norm_right _ <| congr_arg NNReal.toReal h

Premises used: NNReal.eq, congr_arg, norm_div_eq_norm_right, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
x y : E
h : ‖y‖₊ = 0
⊢ ‖x / y‖₊ = ‖x‖₊

Tactic:
NNReal.eq <| norm_div_eq_norm_left _ <| congr_arg NNReal.toReal h

Premises used: norm_div_eq_norm_left, NNReal.eq, congr_arg, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ (↑‖a‖₊ : ℝ≥0∞).toReal = ‖a‖

Tactic:
rfl

Premises used: ENNReal.toReal, NNReal.toReal, rfl
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
α : Type u_2
E : Type u_5
inst : SeminormedGroup E
s t : Set α
f : α → E
x : α
rw : (↑(nndist (s.mulIndicator f x) (t.mulIndicator f x)) : ℝ≥0∞) = (↑‖(s ∆ t).mulIndicator f x‖₊ : ℝ≥0∞)
rw₁ rw₂ : (↑‖(s ∆ t).mulIndicator f x‖₊ : ℝ≥0∞) = (↑‖(s ∆ t).mulIndicator f x‖₊ : ℝ≥0∞)
⊢ edist (s.mulIndicator f x) (t.mulIndicator f x) = (↑‖(s ∆ t).mulIndicator f x‖₊ : ℝ≥0∞)

Tactic:
rw [edist_nndist, nndist_mulIndicator]

Premises used: nndist_mulIndicator, edist_nndist
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
simp_rw : (∃ (x : E) (y : E), ¬‖x⁻¹ * y‖₊ = 0) ↔ ∃ (x : E), ‖x‖₊ ≠ 0
⊢ NontrivialTopology E ↔ ∃ (x : E), ‖x‖₊ ≠ 0

Tactic:
simp_rw [TopologicalSpace.nontrivial_iff_exists_not_inseparable, Metric.inseparable_iff_nndist,
    nndist_eq_nnnorm_inv_mul]

Premises used: nndist_eq_nnnorm_inv_mul, TopologicalSpace.nontrivial_iff_exists_not_inseparable, Metric.inseparable_iff_nndist
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
h : ∃ (x : E), ‖x‖₊ ≠ 0
x : E
hx : ‖x‖₊ ≠ 0
⊢ ¬‖x⁻¹ * 1‖₊ = 0

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ (∃ (x : E) (y : E), ¬‖x⁻¹ * y‖₊ = 0) ↔ ∃ (x : E), ‖x‖₊ ≠ 0

Tactic:
exact ⟨fun ⟨x, y, hxy⟩ => ⟨_, hxy⟩, fun ⟨x, hx⟩ => ⟨x, 1, by simpa using hx⟩⟩
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0

Tactic:
simpa using nontrivialTopology_iff_exists_nnnorm_ne_zero' (E := E).not

Premises used: Iff.not, nontrivialTopology_iff_exists_nnnorm_ne_zero'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
inst_1 : NontrivialTopology E
⊢ ∃ (x : E), ‖x‖₊ ≠ 0

Tactic:
nontrivialTopology_iff_exists_nnnorm_ne_zero'.1 ‹_›

Premises used: nontrivialTopology_iff_exists_nnnorm_ne_zero', Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
inst_1 : IndiscreteTopology E
⊢ ∀ (x : E), ‖x‖₊ = 0

Tactic:
indiscreteTopology_iff_forall_nnnorm_eq_zero'.1 ‹_›

Premises used: indiscreteTopology_iff_forall_nnnorm_eq_zero', Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ NontrivialTopology E ↔ ∃ (x : E), ‖x‖ ≠ 0

Tactic:
simp [nontrivialTopology_iff_exists_nnnorm_ne_zero', ← NNReal.ne_iff]

Premises used: nontrivialTopology_iff_exists_nnnorm_ne_zero', NNReal.ne_iff
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
⊢ IndiscreteTopology E ↔ ∀ (x : E), ‖x‖ = 0

Tactic:
simpa using nontrivialTopology_iff_exists_norm_ne_zero' (E := E).not

Premises used: Iff.not, nontrivialTopology_iff_exists_norm_ne_zero'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
inst_1 : NontrivialTopology E
⊢ ∃ (x : E), ‖x‖ ≠ 0

Tactic:
nontrivialTopology_iff_exists_norm_ne_zero'.1 ‹_›

Premises used: nontrivialTopology_iff_exists_norm_ne_zero', Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
inst_1 : IndiscreteTopology E
⊢ ∀ (x : E), ‖x‖ = 0

Tactic:
indiscreteTopology_iff_forall_norm_eq_zero'.1 ‹_›

Premises used: indiscreteTopology_iff_forall_norm_eq_zero', Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : TopologicalSpace E
inst_1 : ESeminormedMonoid E
rw rw₁ : Eq (α := ℝ≥0∞) 0 0
⊢ enorm.{u_8} (E := E) 1 = 0

Tactic:
rw [ESeminormedMonoid.enorm_zero]

Premises used: ESeminormedMonoid.enorm_zero
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : TopologicalSpace E
inst_1 : ESeminormedMonoid E
hbot : NeBot (α := E) (𝓝[≠] 1)
c : ℝ≥0∞
hc : c ≠ 0
⊢ enorm.{u_8} (E := E) 1 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
⊢ ‖a⁻¹‖ₑ = ‖a‖ₑ

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup 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_inv_mul, ofReal_norm']

Premises used: ofReal_norm', dist_eq_norm_inv_mul, edist_dist
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : SeminormedGroup E
a b : E
rw : ‖(a / b)⁻¹‖ₑ = ‖b / a‖ₑ
rw₁ rw₂ : ‖b / a‖ₑ = ‖b / a‖ₑ
⊢ ‖a / b‖ₑ = ‖b / a‖ₑ

Tactic:
rw [← enorm_inv', inv_div]

Premises used: enorm_inv', inv_div
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_5
inst : SeminormedGroup E
a : E
r : ℝ≥0∞
rw : edist a 1 < r ↔ ‖a‖ₑ < r
rw₁ rw₂ : ‖a‖ₑ < r ↔ ‖a‖ₑ < r
⊢ Membership.mem (γ := Set E) (eball 1 r) a ↔ ‖a‖ₑ < r

Tactic:
rw [Metric.mem_eball, edist_one_right]

Premises used: edist_one_right, Metric.mem_eball
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : TopologicalSpace E
inst_1 : ESeminormedMonoid E
a b : E
⊢ ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

Tactic:
ESeminormedMonoid.enorm_mul_le a b

Premises used: ESeminormedMonoid.enorm_mul_le
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : TopologicalSpace E
inst_1 : ESeminormedMonoid E
r₁ r₂ : ℝ≥0∞
a₁ a₂ : E
h₁ : ‖a₁‖ₑ ≤ r₁
h₂ : ‖a₂‖ₑ ≤ r₂
⊢ ‖a₁ * a₂‖ₑ ≤ r₁ + r₂

Tactic:
(enorm_mul_le' a₁ a₂).trans <| add_le_add h₁ h₂

Premises used: add_le_add, LE.le.trans, enorm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : TopologicalSpace E
inst_1 : ESeminormedMonoid E
a b c : E
⊢ ‖a * b * c‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ

Tactic:
enorm_mul_le_of_le' (enorm_mul_le' _ _) le_rfl

Premises used: enorm_mul_le_of_le', le_rfl, enorm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : TopologicalSpace E
inst_1 : ESeminormedMonoid E
a b c d : E
⊢ ‖a * b * c * d‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ + ‖d‖ₑ

Tactic:
enorm_mul_le_of_le' enorm_mul₃_le' le_rfl

Premises used: enorm_mul_le_of_le', le_rfl, enorm_mul₃_le'
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : TopologicalSpace E
inst_1 : ENormedMonoid E
a : E
⊢ ‖a‖ₑ = 0 ↔ a = 1

Tactic:
simp [ENormedMonoid.enorm_eq_zero]

Premises used: ENormedMonoid.enorm_eq_zero
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : TopologicalSpace E
inst_1 : ENormedMonoid E
a : E
⊢ ‖a‖ₑ ≠ 0 ↔ a ≠ 1

Tactic:
enorm_eq_zero'.ne

Premises used: enorm_eq_zero', Iff.ne
-- Module: Mathlib.Analysis.Normed.Group.Basic
Goal:
E : Type u_8
inst : TopologicalSpace E
inst_1 : ENormedMonoid E
a : E
⊢ 0 < ‖a‖ₑ ↔ a ≠ 1

Tactic:
pos_iff_ne_zero.trans enorm_ne_zero'

Premises used: enorm_ne_zero', Iff.trans, pos_iff_ne_zero