mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
⊢ ∑ p ∈ s, a p ∈ J

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
⊢ ∑ p ∈ s, a p ∈ J
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddBelow s
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: x y : ℝ
⊢ x - y ≤ x - y ∨ x - y ≤ -(x - y)

Tactic:
]

Goal state after:
x y : ℝ
⊢ x - y ≤ x - y ∨ x - y ≤ -(x - y)
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
f : ι → ℕ
⊢ BddAbove (range fun x ↦ ↑(f x)) ↔ BddAbove (range (Nat.cast ∘ f))

Tactic:
]

Goal state after:
ι : Sort u_3
f : ι → ℕ
⊢ BddAbove (range fun x ↦ ↑(f x)) ↔ BddAbove (range (Nat.cast ∘ f))
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x r y : ℝ
⊢ x - r < y ∧ y - x < r ↔ x - r < y ∧ y - x < r

Tactic:
]

Goal state after:
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨅ i, ↑(f i)) * ↑a = ⨅ i, ↑(f i * a)

Tactic:
]

Goal state after:
ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨅ i, ↑(f i)) * ↑a = ⨅ i, ↑(f i * a)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x r y : ℝ
⊢ x - r ≤ y ∧ y - x ≤ r ↔ x - r ≤ y ∧ y - x ≤ r

Tactic:
]

Goal state after:
Module: Mathlib.Data.NNReal.Basic

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

Tactic:
]

Goal state after:
ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑a * ⨆ i, ↑(f i) = ⨆ i, ↑(a * f i)
Module: Mathlib.Data.NNReal.Basic

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

Tactic:
]

Goal state after:
ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ⨆ i, a * f i = ⨆ i, f i * a
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x y : ℝ
⊢ Ioo x y = Ioo x y

Tactic:
]

Goal state after:
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ ⨆ i, g * h i ≤ a

Tactic:
]

Goal state after:
ι : Sort u_3
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ ⨆ i, g * h i ≤ a
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ ⨆ i, g i * h ≤ a

Tactic:
]

Goal state after:
ι : Sort u_3
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ ⨆ i, g i * h ≤ a
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ ⨅ i, g * h i

Tactic:
]

Goal state after:
ι : Sort u_3
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ ⨅ i, g * h i
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x y : ℝ
⊢ Icc x y = Icc x y

Tactic:
]

Goal state after:
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ ⨅ i, g i * h

Tactic:
]

Goal state after:
ι : Sort u_3
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ ⨅ i, g i * h
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : ι → α × α
p : Filter ι
⊢ Tendsto (fun x ↦ dist (f x).1 (f x).2) p (𝓝 0) ↔ Tendsto (fun x ↦ dist (f x).1 (f x).2) p (𝓝 0)

Tactic:
]

Goal state after:
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_4
f : ι → ℕ
⊢ ↑(⨆ i, f i) = ⨆ i, ↑(f i)

Tactic:
by_cases h : BddAbove (Set.range f)
  · apply eq_of_forall_ge_iff
    simp [ciSup_le_iff', ← Nat.le_floor_iff, *]
  · simp [*]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
x : Filter β
a : α
⊢ Tendsto (fun x ↦ dist (f x) a) x (𝓝 0) ↔ Tendsto (fun b ↦ dist (f b) a) x (𝓝 0)

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
l : Filter β
inst✝ : l.NeBot
hf₀ : ∀ (i : β), p i → 0 < f i
hf₁ : ∀ᶠ (i : β) in l, p i
hf : ∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ closedBall 0 i
⊢ ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
l : Filter β
inst✝ : l.NeBot
hf₀ : ∀ (i : β), p i → 0 < f i
hf₁ : ∀ᶠ (i : β) in l, p i
hf : ∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ closedBall 0 i
⊢ ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs✝ : IsSeparable s
u : Set X
hu : u.Countable
hs : s ⊆ closure[inst✝¹] u
this : Countable ↑u
⊢ closure[inst✝¹] u ⊆ closure[inst✝¹] u

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
⊢ ∀ (i : ℕ), True → ∃ x_1 ∈ V i, ∃ a, (x, a) = x_1 ∧ a ∈ iUnion U

Tactic:
]

Goal state after:
ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
⊢ ∀ (i : ℕ), True → ∃ x_1 ∈ V i, ∃ a, (x, a) = x_1 ∧ a ∈ iUnion U
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
n : ℕ
a✝ : True
i : X
hi : i ∈ U n
hx : x ∈ {y | (y, i) ∈ V n}
⊢ ∃ x_1 ∈ V n, ∃ a, (x, a) = x_1 ∧ a ∈ iUnion U

Tactic:
]

Goal state after:
ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
n : ℕ
a✝ : True
i : X
hi : i ∈ U n
hx : x ∈ {y | (y, i) ∈ V n}
⊢ ∃ x_1 ∈ V n, ∃ a, (x, a) = x_1 ∧ a ∈ iUnion U
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: case base
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ dist (f n) (f (n + 1)) + ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) =
    dist (f n) (f (n + 1)) + ∑ x ∈ Finset.Ico m n, dist (f x) (f (x + 1))

pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
q : HeightOneSpectrum R
hq : q ∈ s ∧ ¬q = p'
⊢ a q ∈ J * p

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
q : HeightOneSpectrum R
hq : q ∈ s ∧ ¬q = p'
⊢ a q ∈ J * p
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ (Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ) ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set ↑s
htc : (Subtype.val '' t).Countable
hst : s ⊆ closure[inst✝¹] (Subtype.val '' t)
⊢ ∀ (a : X) (b : a ∈ s), ↑⟨a, b⟩ ∈ closure[inst✝¹] (Subtype.val '' t)

Tactic:
]

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set ↑s
htc : (Subtype.val '' t).Countable
hst : s ⊆ closure[inst✝¹] (Subtype.val '' t)
⊢ ∀ (a : X) (b : a ∈ s), ↑⟨a, b⟩ ∈ closure[inst✝¹] (Subtype.val '' t)
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s = ∅
⊢ TotallyBounded ∅

Tactic:
]

Goal state after:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
hs : s = ∅
⊢ TotallyBounded ∅
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : Bornology β
f : α → β
⊢ Bornology.IsBounded (range f) ↔ Bornology.IsBounded (range f)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : Bornology α
p : α → Prop
⊢ Bornology.IsBounded {x | p x} ↔ Bornology.IsBounded {x | p x}

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
⊢ (∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ univ, dist (f x) (F n x) < ε) ↔
    ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε

Tactic:
]

Goal state after:
α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
⊢ (∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ univ, dist (f x) (F n x) < ε) ↔
    ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = 0 ↔ nndist x y = 0

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun x ↦ dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun x ↦ dist (Prod.map u u x).1 (Prod.map u u x).2) atTop (𝓝 0) ↔
    Tendsto (fun n ↦ dist (u n.1) (u n.2)) atTop (𝓝 0)
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
⊢ ∀ (i : Subtype (Membership.mem s)), a p' ∈ J * (↑i).asIdeal

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
⊢ ∀ (i : Subtype (Membership.mem s)), a p' ∈ J * (↑i).asIdeal
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: case base
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ edist (f n) (f (n + 1)) + ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) =
    edist (f n) (f (n + 1)) + ∑ x ∈ Finset.Ico m n, edist (f x) (f (x + 1))

pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable ((fun x ↦ f ↑x) '' univ)

Tactic:
]

Goal state after:
β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : IsSeparable s
⊢ IsSeparable ((fun x ↦ f ↑x) '' univ)
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
hq : p' ∈ s
⊢ a p' = a p'

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p | edist p.1 p.2 ≤ ε} ⊆ U
t : Set α
tC : t.Countable
ht : s ⊆ ⋃ x ∈ t, closedEBall x ε
x : α
hx : x ∈ t
y : α
hy : edist x y ≤ ε
⊢ y ∈ UniformSpace.ball x {p | edist p.1 p.2 ≤ ε}

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p | edist p.1 p.2 ≤ ε} ⊆ U
t : Set α
tC : t.Countable
ht : s ⊆ ⋃ x ∈ t, closedEBall x ε
x : α
hx : x ∈ t
y : α
hy : edist x y ≤ ε
⊢ y ∈ UniformSpace.ball x {p | edist p.1 p.2 ≤ ε}
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: β : Type v
γ : Type w
inst✝¹ : EMetricSpace γ
inst✝ : PseudoEMetricSpace β
f : γ → β
⊢ ((∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ) ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ i, ↑i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, eball x δ ⊆ t

Tactic:
]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ i, ↑i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, eball x δ ⊆ t
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ
⊢ ball (↑a) r ∩ {x | p x} = ball (↑a) r ∩ {a | p a}

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
p : α → Prop
a : { a // p a }
r : ℝ
⊢ closedBall (↑a) r ∩ {x | p x} = closedBall (↑a) r ∩ {a | p a}

Tactic:
]

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

Goal state before:
pp: z : ℝ≥0
⊢ nndist 0 z = z

Tactic:
]

Goal state after:
z : ℝ≥0
⊢ nndist 0 z = z
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: a b : ℝ≥0
this : ↑a ≤ ↑b + dist a b
⊢ ↑a ≤ ↑b + dist a b

Tactic:
]

Goal state after:
a b : ℝ≥0
this : ↑a ≤ ↑b + dist a b
⊢ ↑a ≤ ↑b + dist a b
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: a b : ℝ≥0
⊢ ↑a - ↑b ≤ dist a b

Tactic:
]

Goal state after:
a b : ℝ≥0
⊢ ↑a - ↑b ≤ dist a b
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ a ∈ closure[inst✝³] (Ioi a)

Tactic:
]

Goal state after:
case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ a ∈ closure[inst✝³] (Ioi a)
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ {a, b} ⊆ closure[inst✝³] (Ioo a b)

Tactic:
]

Goal state after:
case h₂.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : a < b
⊢ {a, b} ⊆ closure[inst✝³] (Ioo a b)
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case h₂.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ ∅ ⊆ closure[inst✝³] (Ioo a b)

Tactic:
]

Goal state after:
case h₂.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ ∅ ⊆ closure[inst✝³] (Ioo a b)
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ Icc a b

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∉ ⋃ r', ⋃ (_ : r' < r), ball x r' ↔ x✝ ∉ ball x r

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∉ ⋃ r', ⋃ (_ : r' < r), ball x r' ↔ x✝ ∉ ball x r
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ Ioi a = Ioi a

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∉ ⋃ r', ⋃ (_ : r' < r), closedBall x r' ↔ x✝ ∉ ball x r

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∉ ⋃ r', ⋃ (_ : r' < r), closedBall x r' ↔ x✝ ∉ ball x r
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a b = Ioo a b

Tactic:
]

Goal state after: