mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith K₁ fun a ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
⊢ ¬Bornology.IsBounded (image2 f s {b})

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith K₁ fun a ↦ f a b
s : Set α
t : Set β
hst : Bornology.IsBounded (image2 f s t)
⊢ Bornology.IsBounded s ∨ Bornology.IsBounded t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
⊢ edist x y ≤ ↑K * edist (g x) (g y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.ProperSpace.Real

Goal state before:
pp: x : ℝ≥0
r : ℝ
⊢ IsCompact (Metric.closedBall x r)

Tactic:
by

Goal state after:
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
x : X
⊢ (zipWith d [x] ([] ++ [x])).sum = 0

Tactic:
by

Goal state after:
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
x y : X
⊢ ⨅ l, (zipWith d (x :: l) (l ++ [y])).sum = ⨅ l, (zipWith d (y :: l) (l ++ [x])).sum

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ Isometry f ↔ ∀ (x y : α), nndist (f x) (f y) = nndist x y

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ Isometry f ↔ ∀ (x y : α), dist (f x) (f y) = dist x y

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x y : α
⊢ edist x y ≤ ↑1 * edist (f x) (f y)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
x y : α
⊢ edist (f x) (f y) = edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
δ : Type u_3
inst✝ : PseudoEMetricSpace δ
f : α → β
g : γ → δ
hf : Isometry f
hg : Isometry g
x y : α × γ
⊢ edist (Prod.map f g x) (Prod.map f g y) = edist x y

Tactic:
by

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

Goal state before:
pp: ι : Type u_5
inst✝² : Fintype ι
α : ι → Type u_3
β : ι → Type u_4
inst✝¹ : (i : ι) → PseudoEMetricSpace (α i)
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : (i : ι) → α i → β i
hf : ∀ (i : ι), Isometry (f i)
x y : (i : ι) → α i
⊢ edist (Pi.map f x) (Pi.map f y) = edist x y

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
x y : E i
⊢ edist x y ≤ edist (Pi.single i x i) (Pi.single i y i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
⊢ Isometry (Pi.single i)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
⊢ Isometry ⇑(AddMonoidHom.inl α β)

Tactic:
by

Goal state after:
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
x y z : X
lxy lyz : List X
⊢ (zipWith d (x :: lxy ++ y :: lyz) (lxy ++ y :: lyz ++ [z])).sum =
    (zipWith d (x :: lxy) (lxy ++ [y])).sum + (zipWith d (y :: lyz) (lyz ++ [z])).sum

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
⊢ Isometry ⇑(AddMonoidHom.inr α β)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
inst✝ : Fintype α
g : β → γ
hg : Isometry g
x✝¹ x✝ : α → β
⊢ edist ((fun f ↦ g ∘ f) x✝¹) ((fun f ↦ g ∘ f) x✝) = edist x✝¹ x✝

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
g : β → α
h : Isometry f
hg : RightInverse g f
x y : β
⊢ edist (g x) (g y) = edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
⊢ f ⁻¹' Metric.closedEBall (f x) r = Metric.closedEBall x r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
⊢ f ⁻¹' Metric.eball (f x) r = Metric.eball x r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
s : Set α
d : ℝ≥0∞
⊢ Metric.ediam (f '' s) ≤ d ↔ Metric.ediam s ≤ d

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.ediam (range f) = Metric.ediam univ

Tactic:
by

Goal state after:
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
x y z : X
⊢ ↑(⨅ l, (zipWith d (x :: l) (l ++ [z])).sum) ≤
    ↑(⨅ l, (zipWith d (x :: l) (l ++ [y])).sum) + ↑(⨅ l, (zipWith d (y :: l) (l ++ [z])).sum)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
s : Set α
⊢ Metric.diam (f '' s) = Metric.diam s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.diam (range f) = Metric.diam univ

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
p : ℝ → Prop
⊢ f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)}

Tactic:
by

Goal state after:
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
x y : X
⊢ (zipWith d [x] ([] ++ [y])).sum = d x y

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ range ⇑h = univ

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Metric.ediam univ = Metric.ediam univ

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.ediam (⇑h ⁻¹' s) = Metric.ediam s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.eball x r = Metric.eball (h.symm x) r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.closedEBall x r = Metric.closedEBall (h.symm x) r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ ⇑h.symm ⁻¹' Metric.eball x r = Metric.eball (h x) r

Tactic:
h.symm.preimage_eball,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ Metric.eball (h.symm.symm x) r = Metric.eball (h x) r
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ ⇑h '' Metric.eball x r = Metric.eball (h x) r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ ⇑h '' Metric.closedEBall x r = Metric.closedEBall (h x) r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
e : α ≃ᵢ β
⊢ CompleteSpace α ↔ CompleteSpace β

Tactic:
by

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
Y : ι → Type u_4
inst✝ : (j : ι) → PseudoEMetricSpace (Y j)
e : ι ≃ ι'
x1 x2 : (i : ι) → Y i
⊢ edist ((Equiv.piCongrLeft' Y e).toFun x1) ((Equiv.piCongrLeft' Y e).toFun x2) = edist x1 x2

Tactic:
by

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝¹ x✝ : α ⊕ β → γ
⊢ edist ((Equiv.sumArrowEquivProdArrow α β γ).toFun x✝¹) ((Equiv.sumArrowEquivProdArrow α β γ).toFun x✝) = edist x✝¹ x✝

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
m n : ℕ
x x2 : Fin m → α
y y2 : Fin n → α
⊢ edist (Fin.append x y) (Fin.append x2 y2) = max (edist x x2) (edist y y2)

Tactic:
simp [edist_pi_def, Finset.sup_univ_eq_iSup, ← Equiv.iSup_comp (e := finSumFinEquiv),
    iSup_sum]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
m n : ℕ
x x2 : Fin m → α
y y2 : Fin n → α
⊢ edist (Fin.append x y) (Fin.append x2 y2) = max (edist x x2) (edist y y2)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
m n : ℕ
x✝¹ x✝ : (Fin m → α) × (Fin n → α)
⊢ edist ((Fin.appendEquiv m n).toFun x✝¹) ((Fin.appendEquiv m n).toFun x✝) = edist x✝¹ x✝

Tactic:
by

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : Unique ι
inst✝ : Fintype ι
x hx : ι → α
⊢ edist ((Equiv.funUnique ι α).toFun x) ((Equiv.funUnique ι α).toFun hx) = edist x hx

Tactic:
by

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
α : Fin 2 → Type u_3
inst✝ : (i : Fin 2) → PseudoEMetricSpace (α i)
x hx : (i : Fin 2) → α i
⊢ edist ((piFinTwoEquiv α).toFun x) ((piFinTwoEquiv α).toFun hx) = edist x hx

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.diam (⇑h ⁻¹' s) = Metric.diam s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.ball x r = Metric.ball (h.symm x) r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.sphere x r = Metric.sphere (h.symm x) r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ ⇑h '' Metric.ball x r = Metric.ball (h x) r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ ⇑h '' Metric.sphere x r = Metric.sphere (h x) r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ ⇑h '' Metric.closedBall x r = Metric.closedBall (h x) r

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
g : β → γ
K : ℝ≥0
h : Isometry g
⊢ LipschitzWith K (g ∘ f) ↔ LipschitzWith K f

Tactic:
by

Goal state after:
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₄))
x y : X
l : List X
⊢ IsTrans X fun x y ↦ d x y = 0

Tactic:
by

Goal state after:
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₄))
x y : X
l : List X
this✝ : IsTrans X fun x y ↦ d x y = 0
this : ∀ (n : ℕ), l.length = n → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
⊢ d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ closure[inst✝¹] s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
⊢ Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
hx : x ∉ s
⊢ ∃ u, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ (x : ℕ) in atTop, u x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
⊢ FrechetUrysohnSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
⊢ IsClosed[inst✝²] s

Tactic:
by

Goal state after:
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])
⊢ L.length = l.length + 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
⊢ FrechetUrysohnSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
j a : ℕ
⊢ (Iic a).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
j : ℕ
⊢ ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, y n ∈ closure[inst✝¹] {x k}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
⊢ IsClosed[inst✝¹] (⋃ i, closure[inst✝¹] {x i})

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
x : ℕ → X
inst✝¹ : SequentialSpace X
inst✝ : T1Space X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
⊢ IsClosed[inst✝²] (range x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
⊢ SequentialSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : SequentialSpace X
h₂ : SequentialSpace X
⊢ SequentialSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
⊢ IsSeqCompact (f '' K)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : SeqCompactSpace X
f_cont : SeqContinuous f
⊢ IsSeqCompact (Set.range f)

Tactic:
by

Goal state after:
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}
⊢ 0 ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ V}
⊢ ∃ u, (∀ (n : ℕ), u n ∈ s) ∧ ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
s : Set X
h : IsSeqCompact s
⊢ TotallyBounded s

Tactic:
by

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

Goal state before:
pp: b : ℝ≥0∞
⊢ IsOpen (Ico 0 b)

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 a)

Tactic:
by

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

Goal state before:
pp: α : Type u_4
l : Filter α
x : ℝ≥0
f : ℝ≥0∞ → α
⊢ Tendsto f (𝓝 ↑x) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ENNReal.toNNReal (𝓝 a) (𝓝 a.toNNReal)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ∞
hf : ∀ (x : α), f x ≠ ∞
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal) ↔ Tendsto f u (𝓝 a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
u : Filter α
a : ℝ≥0
hf : ∀ (x : α), f x ≠ ∞
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a) ↔ Tendsto f u (𝓝 ↑a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
n : ℕ
⊢ ⋂ k, ⋂ (_ : k ≤ n), t k ⊆ t n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : (fun x ↦ (f x).toReal) =ᶠ[l] fun x ↦ (g x).toReal
⊢ f =ᶠ[l] g

Tactic:
by

Goal state after: