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

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
j : ι
h : j ∉ S
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ ↑a.1 ⟨j, h⟩

Tactic:
· exact ((continuous_apply _).comp continuous_subtype_val).comp continuous_fst

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h : ofDigits a = ofDigits b
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
⊢ False

Tactic:
have : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x := by
    apply Finset.sum_congr rfl
    grind [ofDigitsTerm]

Goal state after:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h : ofDigits a = ofDigits b
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
⊢ False
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ |3⁻¹| < 1

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun p ↦ p.2.length.add 0) (𝓝 a ×ˢ 𝓝 l) (pure l.length)

Tactic:
exact Tendsto.comp ih tendsto_snd

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
⊢ Path.Homotopic (toLoop i p) (toLoop i q) → Homotopic p q

Tactic:
refine Nonempty.map fun H ↦ ⟨⟨homotopyFrom i H, ?_, ?_⟩, ?_⟩
  pick_goal 3
  · rintro t y ⟨j, jH⟩
    erw [homotopyFrom_apply]
    obtain rfl | h := eq_or_ne j i
    · simp only [Prod.map_apply, id_eq, funSplitAt_apply, Function.uncurry_apply_pair]
      rw [H.eq_fst]
      exacts [congr_arg p ((Cube.splitAt j).left_inv _), jH]
    · rw [p.2 _ ⟨j, jH⟩]; apply boundary; exact ⟨⟨j, h⟩, jH⟩
  all_goals
    intro
    apply (homotopyFrom_apply _ _ _).trans
    simp only [Prod.map_apply, id_eq, funSplitAt_apply,
      Function.uncurry_apply_pair, ContinuousMap.HomotopyWith.apply_zero,
      ContinuousMap.HomotopyWith.apply_one, ne_eq, Path.coe_toContinuousMap]
    first
    | apply congr_arg p
    | apply congr_arg q
    apply (Cube.splitAt i).left_inv

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: 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
⊢ (if ↑(y✝ i) ≤ 1 / 2 then
      if ↑(y✝ j) ≤ 1 / 2 then
        a
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
            (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))))
      else
        b
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
            (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)))
    else
      if ↑(y✝ j) ≤ 1 / 2 then
        c
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
            (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))))
      else
        d
          (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
            (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)))) =
    if ↑(y✝ j) ≤ 1 / 2 then
      if ↑(y✝ i) ≤ 1 / 2 then
        a
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
            (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))))
      else
        c
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
            (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)))
    else
      if ↑(y✝ i) ≤ 1 / 2 then
        b
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
            (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))))
      else
        d
          (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
            (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)))

Tactic:
split_ifs <;>
    · congr 1; ext1; simp only [Function.update, eq_rec_constant, dite_eq_ite]
      apply ite_ite_comm; rintro rfl; exact h.symm

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A B : Set X
ε : ℝ≥0
h : A ⊆ B
⊢ externalCoveringNumber ε A ≤ externalCoveringNumber ε B

Tactic:
simp only [externalCoveringNumber, le_iInf_iff]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
A B : Set X
ε : ℝ≥0
h : A ⊆ B
⊢ ∀ (i : Set X), IsCover ε B i → ⨅ C, ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard
Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff

Goal state before:
pp: ⊢ 1 < 2

Tactic:
by norm_num

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

Goal state before:
pp: X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
⊢ ∃ f, Continuous f ∧ Function.Surjective f

Tactic:
obtain ⟨emb, h_emb⟩ := Metric.PiNatEmbed.exists_embedding_to_hilbert_cube (X := X)

Goal state after:
X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
⊢ ∃ f, Continuous f ∧ Function.Surjective f
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_1
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
h : IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
⊢ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑p

Tactic:
have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.trans e

Goal state after:
case refine_1
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
h : IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
f : X ≃ᵢ ↥p
⊢ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑p
Module: Mathlib.Topology.MetricSpace.ShrinkingLemma

Goal state before:
pp: α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (fun r ↦ 0 < r ∧ r < R x) fun r ↦ ball x r
ι : Type u
c : ι → α
r' : ι → ℝ
hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a)
hsub' : s ⊆ ⋃ a, ball (c a) (r' a)
hfin : LocallyFinite fun a ↦ ball (c a) (r' a)
r : ι → ℝ
hsub : s ⊆ ⋃ i, ball (c i) (r i)
hlt : ∀ (i : ι), r i ∈ Ioo 0 (r' i)
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)

Tactic:
exact ⟨ι, c, r, r', fun i => ⟨(hr' i).1, (hlt i).1, (hlt i).2, (hr' i).2.2⟩, hfin, hsub⟩

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b c : α
hc : c ∈ {a | (Ici a)ᶜ ∈ S}
hb : ∀ i ∈ S, b ∈ iᶜ
⊢ ¬b < c

Tactic:
← mem_Iio,

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b c : α
hc : c ∈ {a | (Ici a)ᶜ ∈ S}
hb : ∀ i ∈ S, b ∈ iᶜ
⊢ b ∉ Iio c
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁵ : FunLike F α β
inst✝⁴ : PartialOrder α
inst✝³ : OrderTop α
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : PseudoEpimorphismClass F α β
f : F
⊢ f ⊤ = ⊤

Tactic:
by
    let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ <| f ⊤)
    rw [← top_le_iff.1 h.1, h.2]

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

Goal state before:
pp: case refine_2
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
⊢ ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄), homOfLE ⋯ ≫ sq.f₁₂ = s.fst

pp: case refine_3
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
⊢ ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄), homOfLE ⋯ ≫ sq.f₁₃ = s.snd

pp: case refine_4
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
⊢ ∀ (s : PullbackCone sq.f₂₄ sq.f₃₄) (m : s.pt ⟶ sq.X₁), m ≫ sq.f₁₂ = s.fst → m ≫ sq.f₁₃ = s.snd → m = homOfLE ⋯

Tactic:
all_goals intros; apply Subsingleton.elim

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ sq.X₄
⊢ ∃ U f, (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

Tactic:
rw [h₄] at hx
      obtain (hx | hx) := hx
      · exact ⟨_, _, ⟨Sieve.ofArrows_mk _ _ WalkingPair.left, hx⟩⟩
      · exact ⟨_, _, ⟨Sieve.ofArrows_mk _ _ WalkingPair.right, hx⟩⟩

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝ : TopologicalSpace E
b : β
y : ↑Y
hfy : LowerSemicontinuous (X.domRestrict fun x ↦ f x ↑y)
⊢ IsClosed (sublevelLeft X f b ↑y)

Tactic:
lowerSemicontinuous_iff_isClosed_preimage

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝ : TopologicalSpace E
b : β
y : ↑Y
hfy : ∀ (y_1 : β), IsClosed ((X.domRestrict fun x ↦ f x ↑y) ⁻¹' Iic y_1)
⊢ IsClosed (sublevelLeft X f b ↑y)
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
h : smallInductiveDimension X < ↑n
⊢ HasSmallInductiveDimensionLT X n

Tactic:
contrapose! h

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
h : ¬HasSmallInductiveDimensionLT X n
⊢ ↑n ≤ smallInductiveDimension X
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝⁸ : LinearOrder β
X : Set E
Y : Set F
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
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
cY : Convex ℝ Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ∃ᶠ (x : F) in nhdsWithin (↑z) Y, ∃ (h : x ∈ segment ℝ ↑y ↑y'), ⟨x, h⟩ ∈ J
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
hfx : ∀ᶠ (x' : F) in nhdsWithin (↑z) Y, f (↑x) x' < b'
this :
  ∀ᶠ (z' : F) in nhdsWithin (↑z) Y,
    (∃ (hz' : z' ∈ segment ℝ ↑y ↑y'), ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y') →
      ∃ (hz' : z' ∈ segment ℝ ↑y ↑y'),
        x ∈ sublevelLeft X f b' z' ∧ ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
⊢ ∃ z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y', x ∈ sublevelLeft X f b' ↑z'

Tactic:
obtain ⟨z', hz', hxz'1, hxz'2⟩ := hz.mp this |>.exists

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝⁸ : LinearOrder β
X : Set E
Y : Set F
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
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
cY : Convex ℝ Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ∃ᶠ (x : F) in nhdsWithin (↑z) Y, ∃ (h : x ∈ segment ℝ ↑y ↑y'), ⟨x, h⟩ ∈ J
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
hfx : ∀ᶠ (x' : F) in nhdsWithin (↑z) Y, f (↑x) x' < b'
this :
  ∀ᶠ (z' : F) in nhdsWithin (↑z) Y,
    (∃ (hz' : z' ∈ segment ℝ ↑y ↑y'), ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y') →
      ∃ (hz' : z' ∈ segment ℝ ↑y ↑y'),
        x ∈ sublevelLeft X f b' z' ∧ ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
z' : F
hz' : z' ∈ segment ℝ ↑y ↑y'
hxz'1 : x ∈ sublevelLeft X f b' z'
hxz'2 : ⟨z', hz'⟩ ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
⊢ ∃ z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y', x ∈ sublevelLeft X f b' ↑z'
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))
n : ℕ
⊢ hausdorffDist (X2 n) (X2 n.succ) < d n

Tactic:
rw [X2n n, X2nsucc n, range_comp, range_comp, hausdorffDist_image,
      hausdorffDist_optimal, ← dist_ghDist]
    · exact hu n n n.succ (le_refl n) (le_succ n)
    · apply UniformSpace.Completion.coe_isometry.comp _
      exact (toInductiveLimit_isometry _ _).comp ((ic n).comp (toGlueR_isometry _ _))

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

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
x y z : X
inst✝ : CompleteSpace X
⊢ IsComplete (Set.range _root_.toContinuousMap)

Tactic:
by simpa [Set.EqOn, range_coe]
    using ContinuousMap.isComplete_setOfPred_eqOn (Function.update (fun _ : I ↦ y) 0 x) {0, 1}

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' := ⋯ }
⊢ 1 / 2 < 1

Tactic:
by norm_num

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
x✝¹ : SetRel X X
x✝ : x✝¹ ∈ 𝓤 X ∧ x✝¹.IsSymm ∧ x✝¹.IsTrans
left✝ : x✝¹ ∈ 𝓤 X
hU : x✝¹.IsSymm
right✝ : x✝¹.IsTrans
⊢ SetRel.IsSymm (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id x✝¹)

Tactic:
by rw [id_eq]; infer_instance

Goal state after:
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 → β
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

Tactic:
exact ⟨_, ne_X.choose_spec, hsup_y _ ne_X.choose_spec⟩

Goal state after: