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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this✝¹ : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
I1 : ∀ (x : X), ⨅ y, Fb (inl x, inr y) ≤ r
y : Y
this✝ : f (inr y) ∈ ↑q
z : ↥(lp (fun n ↦ ℝ) ∞)
zq : z ∈ ↑p
hz : dist z (f (inr y)) < r
this : z ∈ range Φ
x : X
hx : Φ x = z
⊢ BddBelow (range fun x ↦ Fb (inl x, inr y))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝ˢ (Ioc a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this✝¹ : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
I1 : ∀ (x : X), ⨅ y, Fb (inl x, inr y) ≤ r
y : Y
this✝ : f (inr y) ∈ ↑q
z : ↥(lp (fun n ↦ ℝ) ∞)
zq : z ∈ ↑p
hz : dist z (f (inr y)) < r
this : z ∈ range Φ
x : X
hx : Φ x = z
⊢ dist (Φ x) (Ψ y) = dist z (f (inr y))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a ≤ b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
⊢ Ioi a ∈ 𝓝ˢ (Ici b) ↔ a < b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c : α
h : b ≤ c
⊢ Iio c ∈ 𝓝ˢ (Iio b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b c : α
h : a ≤ b
⊢ Ioi a ∈ 𝓝ˢ (Ioi b)

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
I1 : ∀ (x : X), ⨅ y, Fb (inl x, inr y) ≤ r
⊢ ∀ (y : Y), ⨅ x, Fb (inl x, inr y) ≤ r

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
⊢ (𝓝ˢ (Iic a)).HasBasis (fun x ↦ a < x) Iio

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : (𝓝[>] a).NeBot
⊢ (𝓝ˢ (Iic a)).HasBasis (fun x ↦ a < x) Iic

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
⊢ ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q

Tactic:
by

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

Goal state before:
pp: L : Type u_1
inst✝² : SemilatticeSup L
inst✝¹ : TopologicalSpace L
inst✝ : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ Tendsto ((partialSups f) n) l (𝓝 ((partialSups g) n))

Tactic:
by

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

Goal state before:
pp: L : Type u_1
inst✝² : SemilatticeSup L
inst✝¹ : TopologicalSpace L
inst✝ : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ Tendsto (fun a ↦ (partialSups fun x ↦ f x a) n) l (𝓝 ((partialSups g) n))

Tactic:
by

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

Goal state before:
pp: L : Type u_1
inst✝³ : SemilatticeSup L
inst✝² : TopologicalSpace L
inst✝¹ : ContinuousSup L
X : Type u_2
inst✝ : TopologicalSpace X
f : ℕ → X → L
n : ℕ
x : X
hf : ∀ k ≤ n, ContinuousAt (f k) x
⊢ ContinuousAt ((partialSups f) n) x

Tactic:
by

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

Goal state before:
pp: L : Type u_1
inst✝³ : SemilatticeSup L
inst✝² : TopologicalSpace L
inst✝¹ : ContinuousSup L
X : Type u_2
inst✝ : TopologicalSpace X
f : ℕ → X → L
n : ℕ
s : Set X
x : X
hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x
⊢ ContinuousWithinAt ((partialSups f) n) s x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h : x ≠ y
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
⊢ lawsonBasis α =
    image2 (fun x x_1 ↦ ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
      {U | IsOpen[scott α univ] U}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Partial

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
r : SetRel Y X
l : Filter Y
x : X
⊢ RTendsto' r l (𝓝 x) ↔ ∀ (s : Set X), IsOpen[inst✝] s → x ∈ s → r.preimage s ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Partial

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
⊢ IsOpen[inst✝¹] f.Dom

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
⊢ IsTopologicalBasis (lawsonBasis α)

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
⊢ ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
⊢ L ≤ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Partial

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst✝] s
x : X
y : Y
ys : y ∈ s
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s ⊆ t
⊢ ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
L : TopologicalSpace α
inst✝ : IsLawson α
⊢ scottHausdorff α univ ≤ L

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsUpperSet s
⊢ IsOpen[L] s ↔ IsOpen[S] s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsClosed[L] s ↔ IsClosed[S] s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsClosed[L] s ↔ DirSupClosed s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Partial

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
⊢ PContinuous f ↔ ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed[inst✝¹] {a}

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
by

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

Goal state before:
pp: x : GHSpace
y : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ 0 ∈ lowerBounds ((fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = x})

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.AlexandrovDiscrete

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
⊢ nhdsKer s = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.AlexandrovDiscrete

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : AlexandrovDiscrete X
inst✝ : T1Space X
⊢ DiscreteTopology X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
⊢ Disjoint (nhdsSet s) (nhdsSet t)

Tactic:
by

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

Goal state before:
pp: x : GHSpace
⊢ dist x x = 0

Tactic:
by

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

Goal state before:
pp: x y : GHSpace
⊢ (fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = y} =
    (fun p ↦ hausdorffDist ↑p.1 ↑p.2) ∘ Prod.swap '' {a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = y}

Tactic:
by

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

Goal state before:
pp: x y : GHSpace
⊢ dist x y = dist y x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.Lemmas

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
s : Set X
hs : s.Countable
⊢ IsTotallyDisconnected s

Tactic:
by

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

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ dist x z = dist (toGHSpace X) (toGHSpace Z)

Tactic:
by

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

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y)) (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) ≤
    hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y)) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) +
      hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z))

Tactic:
by

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

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y)) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) +
      hausdorffDist (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) =
    hausdorffDist (toGlueL hΦ hΨ '' range (optimalGHInjl X Y)) (toGlueL hΦ hΨ '' range (optimalGHInjr X Y)) +
      hausdorffDist (toGlueR hΦ hΨ '' range (optimalGHInjl Y Z)) (toGlueR hΦ hΨ '' range (optimalGHInjr Y Z))

Tactic:
by

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

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ hausdorffDist (toGlueL hΦ hΨ '' range (optimalGHInjl X Y)) (toGlueL hΦ hΨ '' range (optimalGHInjr X Y)) +
      hausdorffDist (toGlueR hΦ hΨ '' range (optimalGHInjl Y Z)) (toGlueR hΦ hΨ '' range (optimalGHInjr Y Z)) =
    hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) +
      hausdorffDist (range (optimalGHInjl Y Z)) (range (optimalGHInjr Y Z))

Tactic:
by

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

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) +
      hausdorffDist (range (optimalGHInjl Y Z)) (range (optimalGHInjr Y Z)) =
    dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z)

Tactic:
by

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

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z) = dist x y + dist y z

Tactic:
by

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

Goal state before:
pp: x y z : GHSpace
⊢ dist x z ≤ dist x y + dist y z

Tactic:
by

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

Goal state before:
pp: x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
⊢ range Φ = range Ψ

Tactic:
by

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

Goal state before:
pp: x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
⊢ (↑(range Ψ) ≃ᵢ y.Rep) = (↑(range Φ) ≃ᵢ y.Rep)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.NotNormal

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
t : Set X
ht : t ∈ 𝒫 s
⊢ IsClosed t

Tactic:
by

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

Goal state before:
pp: x y : GHSpace
hxy : dist x y = 0
⊢ x = y

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.NotNormal

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
h_closed : ∀ t ∈ 𝒫 s, IsClosed t
U V : ↑(𝒫 s) → Set X
hU : ∀ (t : ↑(𝒫 s)), IsOpen (U t)
hV : ∀ (t : ↑(𝒫 s)), IsOpen (V t)
hUs : ∀ (t : ↑(𝒫 s)), ↑t ⊆ U t
hVs : ∀ (t : ↑(𝒫 s)), s \ ↑t ⊆ V t
hUV : ∀ (t : ↑(𝒫 s)), Disjoint (U t) (V t)
t₁ t₂ : ↑(𝒫 s)
h : U t₁ ∩ d = U t₂ ∩ d
⊢ ↑t₁ ⊆ ↑t₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.NotNormal

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
⊢ 2 ^ #↑s ≤ 2 ^ #↑d

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝ : Nonempty ↑s := Nonempty.to_subtype sne
this : 0 ≤ ε₂
p q : ↑s
⊢ ε₂ ≤ 2 * (ε₂ / 2 + δ)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
U V W : Opens α
h : U ⟶ V
k : V ⟶ W
K : ↑U.compactsInside
⊢ baseChangeCompactsInside (h ≫ k) K = baseChangeCompactsInside k (baseChangeCompactsInside h K)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
U : Opens α
K : ↑U.compactsInside
⊢ baseChangeCompactsInside (𝟙 U) K = K

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L M : Compacts α
h : K ⟶ L
k : L ⟶ M
U : ↑M.openNhds
⊢ baseChangeOpenNhds (h ≫ k) U = baseChangeOpenNhds h (baseChangeOpenNhds k U)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Compacts α
U : ↑K.openNhds
⊢ baseChangeOpenNhds (𝟙 K) U = U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝ : ↑⊥.openNhds
⊢ ⊥ ≤ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝¹ : ↑⊥.openNhds
x✝ : ⊥ ⟶ x✝¹
⊢ ∀ {Z : ↑⊥.openNhds} (h : Z ⟶ ⊥), h ≫ x✝ = h ≫ homOfLE ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
K : Compacts α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
⊢ ⋯.functor.Initial

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
K : Compacts α
inst✝ : T2Space α
⊢ ⋯.functor.Initial

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝ : Nonempty ↑s := Nonempty.to_subtype sne
this✝ : 0 ≤ ε₂
this : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
⊢ 0 < ε₂ / 2 + δ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LE α
s t : ClopenUpperSet α
h : (fun s ↦ s.carrier) s = (fun s ↦ s.carrier) t
⊢ s = t

Tactic:
by

Goal state after: