mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_1.succ
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M < l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
⊢ d x (x :: l)[M + 1] ≤ L.sum

Tactic:
]

Goal state after:
case refine_1.succ
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M < l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
⊢ d x (x :: l)[M + 1] ≤ L.sum
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε

Tactic:
]

Goal state after:
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝³ : SMul M X
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul M X
⊢ Continuous[instTopologicalSpaceProd, _] ((fun p ↦ p.1 • p.2) ∘ Prod.map id mk)

Tactic:
]

Goal state after:
M : Type u_1
X : Type u_2
inst✝³ : SMul M X
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul M X
⊢ Continuous[instTopologicalSpaceProd, _] ((fun p ↦ p.1 • p.2) ∘ Prod.map id mk)
Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
⊢ UniformContinuous fun p ↦ (mk p.1, mk p.2).1 / (mk p.1, mk p.2).2

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
⊢ UniformContinuous fun p ↦ (mk p.1, mk p.2).1 / (mk p.1, mk p.2).2
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
x : α
⊢ Inseparable (⋯.extend f (pkg.coe x)) (f x)

Tactic:
]

Goal state after:
α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
x : α
⊢ Inseparable (⋯.extend f (pkg.coe x)) (f x)
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pkg.coe a) = f a

Tactic:
]

Goal state after:
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pkg.coe a) = f a
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: case pos
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)

Tactic:
]

Goal state after:
case pos
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: case neg
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x ↦ f (⋯.some x)

Tactic:
]

Goal state after:
case neg
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x ↦ f (⋯.some x)
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
h : IsUniformInducing f
⊢ IsUniformInducing (⋯.extend f)

Tactic:
]

Goal state after:
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
h : IsUniformInducing f
⊢ IsUniformInducing (⋯.extend f)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ ε < ε * 2

Tactic:
]

Goal state after:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ ε < ε * 2
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n : ℕ
⊢ w n = (∏ k ∈ range n, v (k + 1)) * v 0

Tactic:
]

Goal state after:
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n : ℕ
⊢ w n = (∏ k ∈ range n, v (k + 1)) * v 0
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ (g ∘ pkg.coe) a = (g ∘ pkg.coe) a

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, ↑b), ↑x < a.1 - a.2

Tactic:
]

Goal state after:
b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, ↑b), ↑x < a.1 - a.2
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝³ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ f (g a) = (f ∘ g) a

Tactic:
]

Goal state after:
α : Type uα
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝³ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ f (g a) = (f ∘ g) a
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M < l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
hMl' : (take M l).length = M
⊢ zipWith d (x :: take M l) (take M l ++ [l[M]]) = zipWith d (x :: take M l) (take M l ++ [l[M]])

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)
⊢ ↑(b + 1) + ↑x < y.1

Tactic:
]

Goal state after:
b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)
⊢ ↑(b + 1) + ↑x < y.1
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0
x✝ : ↑a ≠ ∞ ∨ ∞ ≠ ∞
⊢ Tendsto (fun p ↦ p.1 - p.2) (𝓝 (↑a, ∞)) (𝓝 0)

Tactic:
]

Goal state after:
a : ℝ≥0
x✝ : ↑a ≠ ∞ ∨ ∞ ≠ ∞
⊢ Tendsto (fun p ↦ p.1 - p.2) (𝓝 (↑a, ∞)) (𝓝 0)
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ pkg'.coe a = id (pkg'.coe a)

Tactic:
]

Goal state after:
α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ pkg'.coe a = id (pkg'.coe a)
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous ((pkg.prod pkg').extend (uncurry f))

Tactic:
]

Goal state after:
α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous ((pkg.prod pkg').extend (uncurry f))
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case top
a b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
ha : ∞ ≠ 0 ∨ b ≠ ∞
hb : ¬b = 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 (∞ * b))

Tactic:
simp [ht b hb, top_mul hb]

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

Goal state before:
pp: case refine_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
⊢ d l[M] y ≤ L.sum

Tactic:
]

Goal state after:
case refine_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
⊢ d l[M] y ≤ L.sum
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ ((𝓤 α).lift' fun s ↦ gen s ○ gen s) = (𝓤 α).lift' fun s ↦ gen s ○ gen s

pp: case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen

pp: case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s ↦ s ○ s

Tactic:
]

Goal state after:
case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen

case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s ↦ s ○ s
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ ((𝓤 α).lift' fun s ↦ gen (s ○ s)) = (𝓤 α).lift' fun s ↦ gen (s ○ s)

pp: case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s ↦ s ○ s

pp: case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen

Tactic:
]

Goal state after:
case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s ↦ s ○ s

case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone gen
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: case refine_3
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
k : ℕ
hl : 0 < k + 1
⊢ ‖(v (k + 1))⁻¹‖ < b (k + 1)

Tactic:
]

Goal state after:
case refine_3
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
k : ℕ
hl : 0 < k + 1
⊢ ‖(v (k + 1))⁻¹‖ < b (k + 1)
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
⊢ f ∈ closure (range pureCauchy)

Tactic:
have h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y : α, (f, pureCauchy y) ∈ s := fun s hs =>
    let ⟨t'', ht''₁, (ht''₂ : gen t'' ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs
    let ⟨t', ht'₁, ht'₂⟩ := comp_mem_uniformity_sets ht''₁
    have : t' ∈ f.val ×ˢ f.val := f.property.right ht'₁
    let ⟨t, ht, (h : t ×ˢ t ⊆ t')⟩ := mem_prod_same_iff.mp this
    let ⟨x, (hx : x ∈ t)⟩ := f.property.left.nonempty_of_mem ht
    have : t'' ∈ f.val ×ˢ pure x :=
      mem_prod_iff.mpr
        ⟨t, ht, { y : α | (x, y) ∈ t' }, h <| mk_mem_prod hx hx,
          fun ⟨a, b⟩ ⟨(h₁ : a ∈ t), (h₂ : (x, b) ∈ t')⟩ =>
          ht'₂ <| SetRel.prodMk_mem_comp (@h (a, x) ⟨h₁, hx⟩) h₂⟩
    ⟨x, ht''₂ <| by dsimp [gen]; exact this⟩

Goal state after:
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
⊢ f ∈ closure (range pureCauchy)
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum

Tactic:
]

Goal state after:
case refine_3.inr
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl✝ : M ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
hlen : (drop (M + 1) l).length = l.length - (M + 1)
hlen_lt : l.length - (M + 1) < l.length
⊢ 2 * (zipWith d (drop M l) (drop (M + 1) l ++ [y])).sum ≤ L.sum
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
⊢ ((𝓤 (CauchyFilter α)).lift' fun t ↦ range pureCauchy ∩ UniformSpace.ball f t).NeBot

Tactic:
refine (lift'_neBot_iff ?_).mpr (fun s hs => ?_)

Goal state after:
case refine_1
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
⊢ Monotone fun t ↦ range pureCauchy ∩ UniformSpace.ball f t

case refine_2
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ⊢ ∀ x ∈ {p | p ≠ (∞, ∞)}, ContinuousWithinAt (fun p ↦ p.1 - p.2) {p | p ≠ (∞, ∞)} x

Tactic:
]

Goal state after:
⊢ ∀ x ∈ {p | p ≠ (∞, ∞)}, ContinuousWithinAt (fun p ↦ p.1 - p.2) {p | p ≠ (∞, ∞)} x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
a_ne_top : a ≠ ∞
x : ℝ≥0∞
⊢ (a, x) ∈ {p | p ≠ (∞, ∞)}

Tactic:
simp only [a_ne_top, Ne, mem_ofPred_eq, Prod.mk_inj, false_and, not_false_iff]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a : ℝ≥0∞
⊢ ContinuousOn ((fun p ↦ p.1 - p.2) ∘ fun x ↦ (a, x)) {x | x ≠ ∞}

Tactic:
]

Goal state after:
a : ℝ≥0∞
⊢ ContinuousOn ((fun p ↦ p.1 - p.2) ∘ fun x ↦ (a, x)) {x | x ≠ ∞}
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pureCauchy a) = f a

Tactic:
]

Goal state after:
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pureCauchy a) = f a
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case neg
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous ((fun p ↦ p.1 - p.2) ∘ fun x ↦ (x, a))

Tactic:
]

Goal state after:
case neg
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous ((fun p ↦ p.1 - p.2) ∘ fun x ↦ (x, a))
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case pos
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)

Tactic:
]

Goal state after:
case pos
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case neg
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x ↦ f ⋯.some

Tactic:
]

Goal state after:
case neg
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x ↦ f ⋯.some
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Inseparable a b ↔ Inseparable f g

Tactic:
]

Goal state after:
α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Inseparable a b ↔ Inseparable f g
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun x_1 ↦ x_1 * x) (𝓝[<] 1) (𝓝 x)
⊢ x ≤ y

Tactic:
]

Goal state after:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun x_1 ↦ x_1 * x) (𝓝[<] 1) (𝓝 x)
⊢ x ≤ y
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Tendsto (fun x ↦ ((id ∘ Prod.fst) x, (id ∘ Prod.snd) x)) (↑f ×ˢ ↑g) (𝓤 α) ↔ ↑f ×ˢ ↑g ≤ 𝓤 α

Tactic:
]

Goal state after:
α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Tendsto (fun x ↦ ((id ∘ Prod.fst) x, (id ∘ Prod.snd) x)) (↑f ×ˢ ↑g) (𝓤 α) ↔ ↑f ×ˢ ↑g ≤ 𝓤 α
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f g : CauchyFilter α
⊢ Inseparable f g ↔ Inseparable f g

Tactic:
]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case refine_1
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝ : Completion (SeparationQuotient α)
a : α
⊢ ↑(SeparationQuotient.mk a) = ↑(SeparationQuotient.mk a)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case refine_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝ : Completion α
a : α
⊢ ↑a = ↑a

Tactic:
]

Goal state after: