mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i

Tactic:
rintro rfl

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ¬↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
n : ℕ
x : α
hx : x ∈ s n
this : ∀ (l : ℕ) (z : ↥(s (n + l))), ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l
⊢ ∀ (k : ℕ), edist ↑(Nat.rec ⟨x, hx⟩ (fun l z ↦ ⋯.choose) k) ↑⋯.choose ≤ B n / 2 ^ k

Tactic:
exact fun k => (this k _).choose_spec

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y = ∞ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞

Tactic:
iInf_eq_top

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

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : EDist α
y b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b

Tactic:
try simp only [le_refl, true_or, or_true]

Goal state after:
case inl.inl
α : Type u_1
inst✝ : EDist α
y b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist a b ≤ edist a b ∨ edist b a ≤ edist a b

Tactic:
try simp only [le_refl, true_or, or_true]

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : EDist α
a b : α
hab : a ≠ b
⊢ edist b a ≤ edist a b ∨ edist a b ≤ edist a b

Tactic:
try simp only [le_refl, true_or, or_true]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : EDist α
x b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b

Tactic:
try simp only [le_refl, true_or, or_true]

Goal state after:
case inr.inr
α : Type u_1
inst✝ : EDist α
x b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: p q : GHSpace
⊢ dist p q = ghDist p.Rep q.Rep

Tactic:
ghDist,

Goal state after:
p q : GHSpace
⊢ dist p q = dist (toGHSpace p.Rep) (toGHSpace q.Rep)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (⇑f ⁻¹' Ici b))
⊢ b ≤ ↑f (sInf (⇑f ⁻¹' Ici b))

Tactic:
refine LE.le.trans ?_ (map_sInf f _).ge

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (⇑f ⁻¹' Ici b))
⊢ b ≤ sInf (⇑f '' ⇑f ⁻¹' Ici b)
Module: Mathlib.Topology.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder γ
g : β →Co γ
f₁ f₂ : α →Co β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)

Tactic:
comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder γ
g : β →Co γ
f₁ f₂ : α →Co β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₂ a) = g (f₂ a)
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : PseudoEpimorphism β γ
f₁ f₂ : PseudoEpimorphism α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)

Tactic:
comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : PseudoEpimorphism β γ
f₁ f₂ : PseudoEpimorphism α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₂ a) = g (f₂ a)
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder γ
g : EsakiaHom β γ
f₁ f₂ : EsakiaHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)

Tactic:
comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder γ
g : EsakiaHom β γ
f₁ f₂ : EsakiaHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₂ a) = g (f₂ a)
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:
← @isOpen_compl_iff,

Goal state after:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsOpen[L] sᶜ ↔ IsClosed[S] s
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:
obtain (rfl | ⟨a, ha⟩) := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : Topology.IsUpperSet α
t : Set α
hcst : Disjoint (closure ∅) t
hsct : Disjoint ∅ (closure t)
⊢ Disjoint (nhdsSet ∅) (nhdsSet t)

case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
⊢ Disjoint (nhdsSet s) (nhdsSet t)
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
⊢ ghDist X Y + ghDist Y Z = dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z)

Tactic:
ghDist,

Goal state after:
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) + ghDist Y Z = dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z)
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
f g : C(X, ℝ)
x : X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = {x | f x = 0} ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsClosed[inst✝] {x | f x = 0}
ht : IsClosed[inst✝] {x | g x = 0}
hst : Disjoint {x | f x = 0} {x | g x = 0}
hf : s = {x | f x = 0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
hg : t = {x | g x = 0}
hgr : ∀ (x : X), g x ∈ Icc 0 1
hsn : SeparatedNhds {0} {1}
hfx : f x ≠ 0
⊢ f x + g x ≠ 0

Tactic:
· positivity [(hgr x).1, (hfr x).1]

Goal state after:
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: X : TopCat
p₀ : ↑X
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : Abelian C
inst✝ : HasColimits C
⊢ (Presheaf.stalkFunctor C p₀).Additive

Tactic:
dsimp [Presheaf.stalkFunctor]

Goal state after:
X : TopCat
p₀ : ↑X
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : Abelian C
inst✝ : HasColimits C
⊢ ((Functor.whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op ⋙ colim).Additive
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
⊢ principalOpen x ≤ U ↔ x ∈ U

Tactic:
refine ⟨fun h => h <| self_mem_principalOpen _, fun hx y hy => ?_⟩
  · have := U.isOpen
    rw [IsUpperSet.isOpen_iff_isUpperSet] at this
    exact this hy hx

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
f' : unop (op y) ⟶ unop (op x)
⊢ f = f'.op →
    ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
        Opposite.rec
          (fun x ↦
            Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
              c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
          (op y) =
      Opposite.rec
          (fun x ↦
            Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
              c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
          (op x) ≫
        ((diagram U).op ⋙ F).map f

Tactic:
rintro rfl

Goal state after:
case op.op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : CategoryTheory.Pairwise ι
f' : unop (op y) ⟶ unop (op x)
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op y) =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op x) ≫
      ((diagram U).op ⋙ F).map f'.op
Module: Mathlib.Topology.Sheaves.Sheafify

Goal state before:
pp: case h.refine_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : (ConcreteCategory.hom (F.map iU'.op)) gU = (ConcreteCategory.hom (F.map iV'.op)) gV
⊢ ∀ (w : ↥↑⟨W ⊓ (U' ⊓ V'), ⋯⟩),
    fU ((id (W.infLERight (U' ⊓ V') ≫ U'.infLELeft V' ≫ iU)) w) =
      fV ((id (W.infLERight (U' ⊓ V') ≫ U'.infLERight V' ≫ iV)) w)

Tactic:
· intro w
    specialize wU ⟨w.1, w.2.2.1⟩
    specialize wV ⟨w.1, w.2.2.2⟩
    refine wU.trans <| .trans ?_ wV.symm
    rw [← F.germ_res iU' w w.2.1, ← F.germ_res iV' w w.2.1,
      CategoryTheory.types_comp_apply, CategoryTheory.types_comp_apply, e']

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
⊢ ε > 0 → ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε

Tactic:
ε_pos

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
⊢ ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (Prod.map f f ⁻¹' id i)

Tactic:
dsimp
    rintro _ ⟨_, _, _⟩
    infer_instance

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (Prod.map f f ⁻¹' id i)

Tactic:
dsimp
    rintro _ ⟨_, _, _⟩
    infer_instance

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
X : ι → Type u_4
U : (i : ι) → UniformSpace (X i)
h : ∀ (i : ι), IsUltraUniformity (X i)
this : IsUltraUniformity ((x : ι) → X x)
⊢ IsUltraUniformity ((i : ι) → X i)

Tactic:
simpa +instances [Pi.uniformSpace_eq _] using this

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

Goal state before:
pp: X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
this✝ : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := fun n ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
c : (n : ℕ) → GlueSpace ⋯ ⋯ → (Y (n + 1)).Space := fun n ↦ cast ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → (Y (n + 1)).Space := fun n ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (Y n).Space → InductiveLimit I := toInductiveLimit I
coeZ : Z0 → UniformSpace.Completion Z0 := UniformSpace.Completion.coe'
X2 : ℕ → Set (UniformSpace.Completion Z0) := fun n ↦ range (coeZ ∘ Φ n ∘ (Y n).embed)
isom : ∀ (n : ℕ), Isometry (coeZ ∘ Φ n ∘ (Y n).embed)
X2n : ∀ (n : ℕ), X2 n = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjl (X n) (X n.succ))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
D2 : ∀ (n : ℕ), hausdorffDist (X2 n) (X2 n.succ) < d n
X3 : ℕ → NonemptyCompacts Z := fun n ↦ { carrier := X2 n, isCompact' := ⋯, nonempty' := ⋯ }
this : CauchySeq X3
L : NonemptyCompacts Z
hL : Tendsto X3 atTop (𝓝 L)
n : ℕ
⊢ (NonemptyCompacts.toGHSpace ∘ X3) n = u n

Tactic:
rw [Function.comp_apply, NonemptyCompacts.toGHSpace, ← (u n).toGHSpace_rep,
      toGHSpace_eq_toGHSpace_iff_isometryEquiv]

Goal state after:
X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
this✝ : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := fun n ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
c : (n : ℕ) → GlueSpace ⋯ ⋯ → (Y (n + 1)).Space := fun n ↦ cast ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → (Y (n + 1)).Space := fun n ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (Y n).Space → InductiveLimit I := toInductiveLimit I
coeZ : Z0 → UniformSpace.Completion Z0 := UniformSpace.Completion.coe'
X2 : ℕ → Set (UniformSpace.Completion Z0) := fun n ↦ range (coeZ ∘ Φ n ∘ (Y n).embed)
isom : ∀ (n : ℕ), Isometry (coeZ ∘ Φ n ∘ (Y n).embed)
X2n : ∀ (n : ℕ), X2 n = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjl (X n) (X n.succ))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
D2 : ∀ (n : ℕ), hausdorffDist (X2 n) (X2 n.succ) < d n
X3 : ℕ → NonemptyCompacts Z := fun n ↦ { carrier := X2 n, isCompact' := ⋯, nonempty' := ⋯ }
this : CauchySeq X3
L : NonemptyCompacts Z
hL : Tendsto X3 atTop (𝓝 L)
n : ℕ
⊢ Nonempty (↥(X3 n) ≃ᵢ (u n).Rep)
Module: Mathlib.Topology.Sion

Goal state before:
pp: case a.inl.mpr
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
sup_inf : β
cY : Convex ℝ ∅
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) ∅
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ ∅ fun y ↦ f x y
hfy hfy' hinf_x : True
hsup_inf : IsBot sup_inf
hsup_y : ∀ x ∈ X, sup_y x = sup_inf
t : β
⊢ t = sup_inf → ∃ x ∈ X, sup_y x = t

Tactic:
rintro rfl

Goal state after:
case a.inl.mpr
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
cY : Convex ℝ ∅
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) ∅
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ ∅ fun y ↦ f x y
hfy hfy' hinf_x : True
t : β
hsup_inf : IsBot t
hsup_y : ∀ x ∈ X, sup_y x = t
⊢ ∃ x ∈ X, sup_y x = t