mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist y z

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: r : ℝ≥0
hr : r ≠ 0
n : ℤ
⊢ ↑(r ^ n) = ↑r ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist z x = edist z y

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z t : α
⊢ edist x t ≤ edist x y + edist y z + edist z t

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α✝
α : Type u
edist : α → α → ℝ≥0∞
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
⊢ 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
⊢ PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist edist_self edist_comm edist_triangle

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else if 0 < n then 0 else ∞

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: n : ℤ
⊢ ∞ ^ n = if n = 0 then 1 else if 0 < n then ∞ else 0

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun x ↦ {p | edist p.1 p.2 < f x}

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
⊢ 0 < a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
n : ℤ
⊢ a ^ n < ∞

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ y ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun x ↦ {p | edist p.1 p.2 ≤ f x}

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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ count K v (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ exps v) = exps v

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
⊢ max (edist x.1 x.1) (edist x.2 x.2) = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α × β
⊢ max (edist x.1 y.1) (edist x.2 y.2) = max (edist y.1 x.1) (edist y.2 x.2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
hy : 1 < y
h'y : y ≠ ∞
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
⊢ comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 β) =
    ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | max (edist p.1.1 p.2.1) (edist p.1.2 p.2.2) < ε}

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ eball x ε ↔ edist x y < ε

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ closedEBall x ε ↔ edist x y ≤ ε

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, y ^ n < x ∧ x ≤ y ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, y ^ n < x ∧ x ≤ y ^ (n + 1)

Tactic:
by
    refine NNReal.exists_mem_Ioc_zpow ?_ (one_lt_coe_iff.1 hy)
    simpa only [Ne, coe_eq_zero] using hx

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
h : 0 < ε
⊢ x ∈ eball x ε

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ x ∈ closedEBall x ε

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ x ∈ eball y ε ↔ y ∈ eball x ε

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ x ∈ closedEBall y ε ↔ y ∈ closedEBall x ε

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
⊢ 0 < ε - edist y x

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
⊢ ∃ ε' > 0, eball y ε' ⊆ eball x ε

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x : α
⊢ edist x x < ∞

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
hy : 1 < y
h'y : y ≠ ∞
⊢ ∃ n, x ∈ Ioc (y ^ n) (y ^ (n + 1))

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
J : Ideal R
hJ : J ≠ 0
⊢ count K v ↑J = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x✝ y✝ : α
h : edist x✝ y✝ < ∞
⊢ edist y✝ x✝ < ∞

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
⊢ eball x 0 = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ ε > 0, eball x ε ⊆ s

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
J : Ideal R
⊢ 0 ≤ count K v ↑J

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ (∀ (i : ℝ≥0∞), 0 < i → ∃ y ∈ s, y ∈ eball x i) ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case inr.inr
α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
y : α
hy : y ∈ t
C : ℝ
hC : ∀ z ∈ s ∪ t, dist x z ≤ C
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
⊢ dist a x + dist x b ≤ C + C

Tactic:
simpa only [dist_comm] using add_le_add (hC _ ha) (hC _ hb)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
⊢ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ r > 0, (eball x r ∩ s).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
a : α
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, u x ∈ eball a ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
⊢ Ioo 0 ∞ = ⋃ n, Ico (y ^ n) (y ^ (n + 1))

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ x ∈ eball a δ ∩ s → f x ∈ eball b ε ∩ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
⊢ s ∪ t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Sort u_3
x y : α
dist : α → α → ℝ
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
⊢ dist x y + dist y x = 2 * dist x y

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
hx : 1 ≤ x
a b : ℤ
h : a ≤ b
⊢ x ^ a ≤ x ^ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: m n : ℤ
x : ℝ≥0
hx : ↑x ≠ 0
⊢ x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
m n : ℤ
⊢ x ^ (m + n) = x ^ m * x ^ n

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
⊢ count K v J ≤ count K v I

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
obtain hm | hm | hm := lt_trichotomy m 0 <;>
      simp_all [zero_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
s : Set α
⊢ ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, edist a b < δ → edist (f a) (f b) < ε

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
m : ℤ
hx₀ : x ≠ 0
hx : x ≠ ∞
⊢ x ^ (-m) * x ^ m = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
m : ℤ
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
m n : ℤ
⊢ x ^ (m - n) = x ^ m * (x ^ n)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
n : ℤ
⊢ x⁻¹ ^ n = (x ^ n)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
n : ℤ
⊢ x⁻¹ ^ n = x ^ (-n)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
hx : 1 ≤ x
m : ℤ
hn : -m ≤ 0
⊢ 0 ≤ m

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ eball x r ×ˢ eball y r ↔ z ∈ eball (x, y) r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ closedEBall x r ×ˢ closedEBall y r ↔ z ∈ closedEBall (x, y) r

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: n : ℤ
hn : n ≤ 0
x : ℝ≥0∞
hx : 1 ≤ x
⊢ x ^ n ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ IsUnit a ↔ a ≠ 0 ∧ a ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
ha : IsUnit a
⊢ ∀ {a_1 b : ℝ≥0∞}, ha.unit.mulLeft a_1 ≤ ha.unit.mulLeft b ↔ a_1 ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ≥0∞
⊢ val '' eball a r = eball (↑a) r ∩ {a | p a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
ha : IsUnit a
⊢ ∀ {a_1 b : ℝ≥0∞}, ha.unit.mulRight a_1 ≤ ha.unit.mulRight b ↔ a_1 ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ≥0∞
⊢ val '' closedEBall a r = closedEBall (↑a) r ∩ {a | p a}

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = I

Tactic:
by

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

Goal state before:
pp: α : Type u_2
m m' : EMetricSpace α
h : m.toEDist = m'.toEDist
⊢ m = m'

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝ : EMetricSpace γ
x y : γ
⊢ 0 < edist x y ↔ x ≠ y

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝ : EMetricSpace γ
x : γ
⊢ closedEBall x 0 = {x}

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ (⨆ i, f i) * a = ⨆ i, f i * a

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ a * sSup s = ⨆ b ∈ s, a * b

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ sSup s * a = ⨆ b ∈ s, b * a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
m m' : WeakPseudoEMetricSpace α
h : m.toEDist = m'.toEDist
⊢ m = m'

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u
inst : PseudoEMetricSpace α
⊢ (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace ≤ toUniformSpace.toTopologicalSpace

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
x✝¹ : ℝ≥0∞
x✝ : ⊥ < x✝¹
⊢ ∞ * f i < x✝¹

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
⊢ (uniformSpaceOfEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯).toTopologicalSpace ≤ e

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
x✝¹ : ℝ≥0∞
x✝ : ⊥ < x✝¹
⊢ f i < x✝¹

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
u : Set β
hu : IsOpen[n] u
uy : Subtype.val ⁻¹' u = Metric.eball (f x) ∞ ↓∩ Metric.eball (f x) r
⊢ Subtype.val ⁻¹' f ⁻¹' u = Metric.eball x ∞ ↓∩ Metric.eball x r

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
⊢ IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
m m' : WeakEMetricSpace α
h : m.toEDist = m'.toEDist
⊢ m = m'

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = 0 → Nonempty ι

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = ∞ → Nonempty ι
⊢ a⁻¹ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_3
m m' : MetricSpace α
h : m.toDist = m'.toDist
⊢ m = m'

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ 0 = dist x y ↔ x = y

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ dist x y ≠ 0 ↔ x ≠ y

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ dist x y ≤ 0 ↔ x = y

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ 0 < dist x y ↔ x ≠ y

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ nndist x y = 0 → x = y

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ nndist x y = 0 ↔ x = y

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ 0 = nndist x y ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = ∞ → Nonempty ι
⊢ a⁻¹ = 0 → Nonempty ι

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = ∞ → Nonempty ι

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: s : Set ℝ≥0∞
⊢ (sInf s)⁻¹ = ⨆ a ∈ s, a⁻¹

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr : r ≤ 0
⊢ (closedBall x r).Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: s : Set ℝ≥0∞
⊢ (sSup s)⁻¹ = ⨅ a ∈ s, a⁻¹

Tactic:
by

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

Goal state before:
pp: γ : Type u_3
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
⊢ m.replaceUniformity H = m

Tactic:
by

Goal state after: