mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ ⋃ n,
      ⋃ j,
        ↑(match n, j with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => PEmpty.elim i) ''
          closedBall 0 1 =
    D

Tactic:
apply subset_antisymm (iUnion₂_subset_iff.mpr fun n ↦ by cases n <;> simp)

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ D ⊆
    ⋃ i,
      ⋃ j,
        ↑(match i, j with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => PEmpty.elim i) ''
          closedBall 0 1
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
f : E → F
hf : IsInducing f
hA : IsSeqCompact A
x : ℕ → F
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n
a : E
ha : a ∈ A
φ : ℕ → ℕ
hφ : StrictMono φ ∧ Tendsto (y ∘ φ) atTop (𝓝 a)
⊢ ∃ a ∈ f '' A, ∃ φ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
refine ⟨f a, mem_image_of_mem f ha, φ, hφ.1, ?_⟩

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
A : Set E
f : E → F
hf : IsInducing f
hA : IsSeqCompact A
x : ℕ → F
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n
a : E
ha : a ∈ A
φ : ℕ → ℕ
hφ : StrictMono φ ∧ Tendsto (y ∘ φ) atTop (𝓝 a)
⊢ Tendsto (x ∘ φ) atTop (𝓝 (f a))
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
m n : ↑(MaxProducts C ho)
h : MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ n
⊢ m = n

Tactic:
apply Subtype.ext ∘ Subtype.ext

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
m n : ↑(MaxProducts C ho)
h : MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ n
⊢ ↑↑m = ↑↑n
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
h : x ∈ some '' Metric.eball a r
⊢ x ∈ Metric.eball (some a) r

Tactic:
obtain ⟨y, yh, yx⟩ := h
    rw [← yx]
    simpa

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

Goal state before:
pp: t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ∈ Set.Icc 0 (1 / 2)

Tactic:
refine ⟨t.2.1, ?_⟩

Goal state after:
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ≤ 1 / 2
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = 1

Tactic:
· rw [(Set.projIcc_eq_right _).2]
    · linarith
    · exact zero_lt_one

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c i).radius

Tactic:
match i with
  | 0 => exact one_le_logSizeRadius ha
  | i + 1 => exact one_le_logSizeRadius ha

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

Goal state before:
pp: case inl
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N

Tactic:
use i

Goal state after:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (insertAt i) (t₀, t) i = 0 ∨ (insertAt i) (t₀, t) i = 1
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ ⋂ n, preCantorSet n = (⋂ i, (fun x ↦ x / 3) '' preCantorSet i) ∪ ⋂ i, (fun x ↦ (2 + x) / 3) '' preCantorSet i

Tactic:
simp_rw [← Function.comp_def,
    ← Set.iInter_union_of_antitone
      (Set.monotone_image.comp_antitone preCantorSet_antitone)
      (Set.monotone_image.comp_antitone preCantorSet_antitone),
    Function.comp_def, ← preCantorSet_succ]

Goal state after:
⊢ ⋂ n, preCantorSet n = ⋂ i, preCantorSet (i + 1)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
⊢ ofDigits a ∈ cantorSet

Tactic:
simp only [cantorSet, Set.mem_iInter]

Goal state after:
a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
⊢ ∀ (i : ℕ), ofDigits a ∈ preCantorSet i
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case refine_1
x : ℝ
h : x ∈ cantorSet
⊢ x ∈ {x | ∃ a, (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x}

pp: case refine_2
x : ℝ
x✝ : x ∈ {x | ∃ a, (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x}
a : ℕ → Fin 3
ha : (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x
⊢ x ∈ cantorSet

Tactic:
· use cantorToTernary x
    exact ⟨fun _ ↦ cantorToTernary_ne_one, ofDigits_cantorToTernary h⟩

Goal state after:
case refine_2
x : ℝ
x✝ : x ∈ {x | ∃ a, (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x}
a : ℕ → Fin 3
ha : (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x
⊢ x ∈ cantorSet
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t y : ↑I
yH : y ∈ {0, 1}
y✝ : { j // j ≠ i } → ↑I
⊢ (Cube.insertAt i) ((t, y).2, y✝) ∈ Cube.boundary N

Tactic:
use i

Goal state after:
case h
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t y : ↑I
yH : y ∈ {0, 1}
y✝ : { j // j ≠ i } → ↑I
⊢ (Cube.insertAt i) ((t, y).2, y✝) i = 0 ∨ (Cube.insertAt i) ((t, y).2, y✝) i = 1
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case inr
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hts : edist t s ≤ c
⊢ edist (f ↑↑⟨⟨t, ht⟩, hst⟩) (f ↑⟨s, hs⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
have hP : P = (fun l ↦
      t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset) := by
        ext; simp [P, and_comm]

Goal state after:
case inr
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hts : edist t s ≤ c
hP : P = fun l ↦ t ∈ (logSizeBallSeq J hJ a c l).finset ∧ s ∈ (logSizeBallSeq J hJ a c l).finset
⊢ edist (f ↑↑⟨⟨t, ht⟩, hst⟩) (f ↑⟨s, hs⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
x✝ : α × List α
a : α
l : List α
⊢ Tendsto (fun p ↦ p.2.insertIdx n p.1) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a, l).2.insertIdx n (a, l).1))

Tactic:
exact tendsto_insertIdx'

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
f : ↑(Ω^ N X x)
⊢ (fun t ↦ f fun j ↦ if j = i then σ (t i) else t j) = ⇑(fromLoop i (Path.symm (toLoop i f)))

Tactic:
by
    ext1; change _ = f _; congr; ext1; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : Compacts α
h : edist s t = 0
this :
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] ↑s =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] ↑t
⊢ ↑s = ↑t

Tactic:
s.isCompact.isClosed.closure_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : Compacts α
h : edist s t = 0
this : ↑s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] ↑t
⊢ ↑s = ↑t
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : NonemptyCompacts α
h : edist s t = 0
this :
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] ↑s =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] ↑t
⊢ ↑s = ↑t

Tactic:
s.isCompact.isClosed.closure_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
inst✝ : EMetricSpace β
s✝ : Set α
s t : NonemptyCompacts α
h : edist s t = 0
this : ↑s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] ↑t
⊢ ↑s = ↑t
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep < ∞

Tactic:
by
  rw [lt_top_iff_ne_top]
  exact hs.einfsep_ne_top

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set X
⊢ ediam (⇑ofSnowflaking ∘ ⇑toSnowflaking ⁻¹' s) ^ α = ediam s ^ α

Tactic:
ofSnowflaking_comp_toSnowflaking,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set X
⊢ ediam (id ⁻¹' s) ^ α = ediam s ^ α
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: case pos
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
h : DiscreteTopology X
⊢ ∃ U, (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst✝²] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
refine ⟨fun n ↦ {Infinite.natEmbedding X n}, fun _ ↦ singleton_nonempty _,
      fun _ ↦ isOpen_discrete _, fun _ _ h ↦ ?_⟩
    simpa using h

Goal state after:
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c ↦ range ⇑c)
f : α → Prop
a b : α
hab : a ≤ b
⊢ {a, b} ∈ range fun c ↦ range ⇑c

Tactic:
use Chain.pair a b hab

Goal state after:
case h
α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c ↦ range ⇑c)
f : α → Prop
a b : α
hab : a ≤ b
⊢ (fun c ↦ range ⇑c) (Chain.pair a b hab) = {a, b}
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
S : Set (Set (PT L))
hS : ∀ t ∈ S, ∃ u, {x | x u} = t
⊢ ∃ u, {x | x u} = ⋃₀ S

Tactic:
choose f hf using hS

Goal state after:
L : Type u_1
inst✝ : CompleteLattice L
S : Set (Set (PT L))
f : (t : Set (PT L)) → t ∈ S → L
hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x | x (f t a)} = t
⊢ ∃ u, {x | x u} = ⋃₀ S
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:
rw [← @isOpen_compl_iff, ← isOpen_compl_iff,
    (lawsonOpen_iff_scottOpen_of_isUpperSet' L S _ (isUpperSet_compl.mpr h))]

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 Ψ)
hΦ : IsCompact (range Φ)
⊢ range Φ = range Ψ

Tactic:
have hΨ : IsCompact (range Ψ) := isCompact_range Ψisom.continuous

Goal state after:
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 Ψ)
hΦ : IsCompact (range Φ)
hΨ : IsCompact (range Ψ)
⊢ range Φ = range Ψ
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 Ψ)
hΦ : IsCompact (range Φ)
hΨ : IsCompact (range Ψ)
⊢ IsClosed (range Ψ)

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 Ψ)
hΦ : IsCompact (range Φ)
hΨ : IsCompact (range Ψ)
⊢ hausdorffEDist (range Φ) (range Ψ) ≠ ∞

Tactic:
· exact hΨ.isClosed

Goal state after:
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 Ψ)
hΦ : IsCompact (range Φ)
hΨ : IsCompact (range Ψ)
⊢ hausdorffEDist (range Φ) (range Ψ) ≠ ∞
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case right
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 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝³
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝² : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝¹ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this✝ :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fr '' range Φ
y : Y
y_in_s' : y ∈ range Φ
yx' : Fr y = x'
x : ↑s
xy : Φ x = y
⊢ dist (Fl ↑x) (Fr (Φ x)) ≤ ε₂ / 2 + δ

Tactic:
exact le_of_eq (glueDist_glued_points (Z := s) Subtype.val Φ (ε₂ / 2 + δ) x)

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

Goal state before:
pp: X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
hF_bij : ∀ (x : ↑X), ∃ U, x ∈ U ∧ ∀ (y : ↑X) (hyU : y ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U y hyU))
⊢ IsCoveringMap base

Tactic:
refine fun x ↦ .to_isEvenlyCovered_preimage (I := WithDiscreteTopology (ToType (F.stalk x))) ?_
  use inferInstance
  rcases hF_bij x with ⟨U, hxU, hU_bij⟩
  use U, hxU, U.isOpen, U.isOpen.preimage (continuous_base F), homeomorph U hU_bij x hxU
  simp

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

Goal state before:
pp: t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
this : ∀ (p : GHSpace), ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)
⊢ ∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ

Tactic:
choose s N hN E hs using this

Goal state after:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
⊢ ∃ β x F, ∀ (x y : ↑t), F x = F y → dist ↑x ↑y < δ
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:

Tactic:
|dist x y - dist (Ψ x) (Ψ y)| = ε * ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| := by
          rw [mul_inv_cancel₀ (ne_of_gt εpos), one_mul]
        _ = ε * (|ε⁻¹| * |dist x y - dist (Ψ x) (Ψ y)|) := by
          rw [abs_of_nonneg (le_of_lt (inv_pos.2 εpos)), mul_assoc]
        _ ≤ ε * 1 := mul_le_mul_of_nonneg_left I (le_of_lt εpos)
        _ = ε := mul_one _

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

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun s ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
⊢ False

Tactic:
obtain ⟨⟨x, y⟩, hxy⟩ : ∃ p : γ × γ, ClusterPt p (F ⊓ 𝓟 Vᶜ) := exists_clusterPt_of_compactSpace _

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun s ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
⊢ False