mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x / y‖ = ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
y : E
ε : ℝ
a : E
⊢ a ∈ ball y ε ↔ a ∈ {x | ‖x⁻¹ * y‖ < ε}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
a : E
⊢ a ∈ ball 1 r ↔ a ∈ {x | ‖x‖ < r}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
⊢ b ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖b⁻¹ * a‖ < r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖a⁻¹ * b‖ < r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
⊢ IsClosed[inst✝²] (s ∩ Icc a y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ
⊢ a ∈ ball 1 r ↔ ‖a‖ < r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖b⁻¹ * a‖ ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
⊢ Icc a b ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this : toDual a ∈ ⇑ofDual ⁻¹' s
⊢ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ
⊢ a ∈ closedBall 1 r ↔ ‖a‖ ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖a⁻¹ * b‖ ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
h : b ∈ closedBall a r
⊢ ‖a‖ + ‖b⁻¹ * a‖ ≤ ‖a‖ + r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
h : b ∈ ball a r
⊢ ‖a‖ + ‖b⁻¹ * a‖ < ‖a‖ + r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this : IsClosed[instTopologicalSpace] (⇑ofDual ⁻¹' s ∩ Icc (toDual b) (toDual a))
⊢ toDual b ∈ ⇑ofDual ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v w : E
⊢ ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this : IsClosed[instTopologicalSpace] (⇑ofDual ⁻¹' s ∩ Icc (toDual b) (toDual a))
⊢ toDual b ≤ toDual a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * ‖v‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedCommGroup E
u v : E
⊢ 0 ≤ 2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedCommGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * min ‖u‖ ‖v‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ sphere a r ↔ ‖b⁻¹ * a‖ = r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ
⊢ a ∈ sphere 1 r ↔ ‖a‖ = r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
⊢ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
hr : r ≠ 0
x : ↑(sphere 1 r)
⊢ ‖↑x‖ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
y : α
hy : y ∈ Icc a b
⊢ IsClosed[inst✝²] (s ∩ Icc y b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
⊢ Icc a b ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
⊢ ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
x : E
y : F
⊢ Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x'⁻¹ * x‖ < δ → ‖(f x')⁻¹ * y‖ < ε

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
⊢ ∃ f, StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ (𝓝 x).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {y | ‖y⁻¹ * x‖ < ε}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
⊢ Icc a a ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ (𝓝 1).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {y | ‖y‖ < ε}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s : Set X
inst✝ : PseudoEMetricSpace X
d : ℝ≥0∞
⊢ ediam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝ : PseudoEMetricSpace X
d : ℝ≥0∞
f : α → X
s : Set α
⊢ ediam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
inst✝ : PseudoEMetricSpace X
ι : Type u_3
o : Option ι
s : ι → Set X
⊢ ediam (⋃ i ∈ o, s i) = ⨆ i ∈ o, ediam (s i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s : Set X
x : X
inst✝ : PseudoEMetricSpace X
d : ℝ≥0∞
⊢ ediam (insert x s) ≤ d ↔ max (⨆ y ∈ s, edist x y) (ediam s) ≤ d

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
x y : X
inst✝ : PseudoEMetricSpace X
⊢ ediam {x, y} = edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ (𝓤 E).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {p | ‖p.1⁻¹ * p.2‖ < ε}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ ‖x‖ₑ.toReal = ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
x y z : X
inst✝ : PseudoEMetricSpace X
⊢ ediam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
a : X
ha : a ∈ s
b : X
hb : b ∈ t
⊢ edist a x + edist x y + edist y b ≤ ediam s + edist x y + ediam t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
h : ‖x‖ = ‖y‖
⊢ ENNReal.ofReal ‖x‖ = ENNReal.ofReal ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
⊢ ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
h : ‖x‖ ≤ ‖y‖
⊢ ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
⊢ ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ nndist a 1 = ‖a‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ edist a 1 = ‖a‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ a = 1 → ‖a‖₊ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖a ^ 0‖ ≤ ↑0 * ‖a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℕ
⊢ ‖a ^ (n + 1)‖ ≤ ↑(n + 1) * ‖a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℕ
⊢ ‖a ^ n‖₊ ≤ ↑n * ‖a‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ nndist 1 a = ‖a‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ edist 1 a = ↑‖a‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht : t₁ ∈ Icc a t₁
⊢ closure[inst✝³] A ⊆ s ∩ Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ edist (s.mulIndicator f x) (t.mulIndicator f x) = ↑‖(s ∆ t).mulIndicator f x‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x✝ : ∃ x, ‖x‖₊ ≠ 0
x : E
hx : ‖x‖₊ ≠ 0
⊢ ¬‖x⁻¹ * 1‖₊ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ NontrivialTopology E ↔ ∃ x, ‖x‖₊ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ NontrivialTopology E ↔ ∃ x, ‖x‖ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ IndiscreteTopology E ↔ ∀ (x : E), ‖x‖ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ESeminormedMonoid E
⊢ ‖1‖ₑ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ESeminormedMonoid E
hbot : (𝓝[≠] 1).NeBot
c : ℝ≥0∞
hc : c ≠ 0
⊢ ‖1‖ₑ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖a⁻¹‖ₑ = ‖a‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
⊢ ediam (s ∪ t) ≤ ediam s + edist x y + ediam t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ edist a b = ‖a⁻¹ * b‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s t : Set X
inst✝ : PseudoEMetricSpace X
h : (s ∩ t).Nonempty
⊢ ediam (s ∪ t) ≤ ediam s + ediam t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
⊢ t₁ ∈ A

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖ₑ = ‖b / a‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ≥0∞
⊢ a ∈ eball 1 r ↔ ‖a‖ₑ < r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ENormedMonoid E
a : E
⊢ ‖a‖ₑ = 0 ↔ a = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
⊢ ediam (univ.pi s) ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x : E
f : Filter E
⊢ Disjoint (𝓝 x) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y⁻¹ * x‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s : Set X
inst✝ : EMetricSpace X
⊢ 0 < ediam s ↔ s.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s : Set X
inst✝ : EMetricSpace X
⊢ 0 < ediam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht₁ : Icc a t₁ ⊆ s
t₁a : a ≤ t₁
t₁b : t₁ ≤ b
this : t₁ = b
⊢ Icc a b ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
f : Filter E
⊢ Disjoint (𝓝 1) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: 𝓕 : 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✝² : Group E
inst✝¹ : SeminormedGroup F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x y : E
⊢ dist x y = ‖f (x⁻¹ * y)‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a b = ‖a / b‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a b = ‖b / a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖a⁻¹ * b‖ = ‖a / b‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ edist a b = ‖a / b‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
x y : E
⊢ dist x⁻¹ y = dist x y⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑(J' + spanSingleton R⁰ (I'.divMod I J') * I) ≤ ↑J' ⊔ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: ι : 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
⊢ dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
y : E
ε : ℝ
⊢ ball y ε = {x | ‖x / y‖ < ε}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖b / a‖ < r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖a / b‖ < r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
⊢ {x | x / a ∈ ball 1 r} = ball a r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht₁ : Icc a t₁ ⊆ s
t₁a : a ≤ t₁
t₁b : t₁ ≤ b
t₁b' : t₁ < b
m : α
t₁m : m > t₁
H : Ioo t₁ m ⊆ s
t : α
hat : t₁ < t
ht : t < min m b
⊢ a ≤ t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖b / a‖ ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖a / b‖ ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
⊢ {x | x / a ∈ closedBall 1 r} = closedBall a r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ sphere a r ↔ ‖b / a‖ = r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
⊢ {x | x / a ∈ sphere 1 r} = sphere a r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a * b ∈ ball a r ↔ ‖b‖ < r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a * b ∈ closedBall a r ↔ ‖b‖ ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun x ↦ b * x) ⁻¹' ball a r = ball (a / b) r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun x ↦ b * x) ⁻¹' closedBall a r = closedBall (a / b) r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun x ↦ b * x) ⁻¹' sphere a r = sphere (a / b) r

Tactic:
by

Goal state after: