mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
⊢ IsCompact A

Tactic:
refine IsCompact.of_isClosed_subset ((?_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed
      fun f hf => ?_

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
⊢ IsCompact (F ⁻¹' A)

case refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
⊢ f ∈ comp Subtype.val M '' F ⁻¹' A
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
⊢ IsCountablyCompact (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]; exact hf.isCountablyCompact_biUnion hc

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s

Tactic:
mem_interior_iff_mem_nhds,

Goal state after:
α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ s ∈ 𝓝 l ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝ : PseudoEMetricSpace T
a : ℝ≥0∞
t : T
V : Finset T
ha : 1 < a
c : ℝ≥0∞
this : ∀ᶠ (a_1 : ℕ) in Filter.atTop, ↑(#V) < ((fun x ↦ a ^ x) ∘ Nat.cast) a_1
⊢ ∃ r, 1 ≤ r ∧ ↑(#({x ∈ V | edist t x ≤ ↑r * c})) ≤ a ^ r

Tactic:
simp only [Function.comp_apply, ENNReal.rpow_natCast, Filter.eventually_atTop] at this

Goal state after:
T : Type u_1
inst✝ : PseudoEMetricSpace T
a : ℝ≥0∞
t : T
V : Finset T
ha : 1 < a
c : ℝ≥0∞
this : ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → ↑(#V) < a ^ b
⊢ ∃ r, 1 ≤ r ∧ ↑(#({x ∈ V | edist t x ≤ ↑r * c})) ≤ a ^ r
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
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 := ⋯
l : ℕ := ⋯
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
hl : #J ≤ l + 1
hlJ : l + 1 = #J
⊢ s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset

Tactic:
suffices h_emp : (logSizeBallSeq J hJ a c (l + 1)).finset = ∅ from by simp [h_emp]

Goal state after:
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
hl : #J ≤ l + 1
hlJ : l + 1 = #J
⊢ (logSizeBallSeq J hJ a c (l + 1)).finset = ∅
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ Cube.boundary N,
      {
            toFun := fun x_2 ↦
              { toContinuousMap := homotopyFrom i H, map_zero_left := ?refine_1, map_one_left := ?refine_2 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        ↑p x_1

Tactic:
rintro t y ⟨j, jH⟩

Goal state after:
case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
⊢ {
        toFun := fun x_1 ↦
          { toContinuousMap := homotopyFrom i H, map_zero_left := ?refine_1, map_one_left := ?refine_2 }.toFun (t, x_1),
        continuous_toFun := ⋯ }
      y =
    ↑p y
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

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

Tactic:
by
  simp_rw [externalCoveringNumber]
  gcongr
  exact iInf_const_mono (fun h_cover ↦ h_cover.mono_radius h)

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
⊢ ∀ (i : Set X), IsCover ε B i → ⨅ C, ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard

Tactic:
exact fun C hC ↦ iInf_le_of_le C <| iInf_le_of_le (hC.anti h) le_rfl

Goal state after:
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∞ := ⋯
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 α := ⋯
t : Closeds α := ⋯
n : ℕ
x : α
hx : x ∈ s n
z : (l : ℕ) → ↥(s (n + l))
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this : CauchySeq fun k ↦ ↑(z k)
y : α
y_lim : Tendsto (fun k ↦ ↑(z k)) atTop (𝓝 y)
⊢ y ∈ t0 ∧ edist x y ≤ 2 * B n

Tactic:
have : y ∈ t0 :=
      mem_iInter.2 fun k =>
        mem_closure_of_tendsto y_lim
          (by
            simp only [exists_prop, Set.mem_iUnion, Filter.eventually_atTop]
            exact ⟨k, fun m hm => ⟨n + m, by lia, (z m).2⟩⟩)

Goal state after:
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
z : (l : ℕ) → ↥(s (n + l))
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this✝ : CauchySeq fun k ↦ ↑(z k)
y : α
y_lim : Tendsto (fun k ↦ ↑(z k)) atTop (𝓝 y)
this : y ∈ t0
⊢ y ∈ t0 ∧ edist x y ≤ 2 * B n
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ∞
C : ℝ≥0
hC : HolderWith C r f
⊢ edist (f x₁) (f x₂) / edist x₁ x₂ ^ ↑r ≤ ↑C

Tactic:
rw [ENNReal.div_le_iff h₁ h₂]

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ∞
C : ℝ≥0
hC : HolderWith C r f
⊢ edist (f x₁) (f x₂) ≤ ↑C * edist x₁ x₂ ^ ↑r
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
hf : MemHolder r f
c : α
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
eHolderNorm_smul

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
hf : MemHolder r f
c : α
⊢ ↑‖c‖₊ * eHolderNorm r f = ↑‖c‖₊ * eHolderNorm r f
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ IsUpper αᵒᵈ ↔ IsLower α

Tactic:
constructor
  · apply OrderDual.instIsLower
  · apply OrderDual.instIsUpper

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

Goal state before:
pp: h : Set Prop
hs : h ∈ {∅, {True}}
⊢ ∃ a, Ioi a = h

Tactic:
← Ioi_True,

Goal state after:
h : Set Prop
hs : h ∈ {Ioi True, {True}}
⊢ ∃ a, Ioi a = h
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:
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.Order.HullKernel

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
T : Set α
S : Set ↑T
⊢ ⋯.closureOperator S = hull T (kernel S)

Tactic:
simp only [toDual_sInf, GaloisConnection.closureOperator_apply, ofDual_sSup]
  rw [← preimage_comp, ← OrderDual.toDual_symm_eq, Equiv.symm_comp_self, preimage_id_eq, id_eq]

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

Goal state before:
pp: α : Type ?u.3
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : αᵒᵈ
⊢ a ≤ OrderDual.toDual (kernel (hull T (OrderDual.ofDual a)))

Tactic:
obtain ⟨S, rfl⟩ := hG a

Goal state after:
α : Type ?u.3
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set ↑T
⊢ kernel S ≤ OrderDual.toDual (kernel (hull T (OrderDual.ofDual (kernel S))))
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: case h
α : Type u_1
inst✝² : TopologicalSpace α
K : Compacts α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
U : ↑K.openNhds
L : Set α
h1 : IsCompact L
h2 : ↑K ⊆ interior L
h3 : L ⊆ ↑↑U
⊢ K.openRcNhdsToOpenNhds ⟨{ carrier := interior L, is_open' := ⋯ }, ⋯⟩ ≤ U

Tactic:
exact Subset.trans interior_subset h3

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
K : Compacts α
inst✝ : T2Space α
⊢ ∀ (j₁ : ↑K.compactNhds), ∃ j₂, K.openRcNhdsToCompactNhds j₂ ≤ j₁

Tactic:
intro L

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
K : Compacts α
inst✝ : T2Space α
L : ↑K.compactNhds
⊢ ∃ j₂, K.openRcNhdsToCompactNhds j₂ ≤ L
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
n : ℕ
⊢ Disjoint s (U n)ᶜ

Tactic:
apply LE.le.disjoint_compl_right

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
n : ℕ
⊢ s ⊆ U n
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X✝ : TopCat
p₀ : ↑X✝
inst✝³ : (U : Opens ↑X✝) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
X : Presheaf C X✝
⊢ (Presheaf.stalkFunctor C p₀).map ((StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).app X) ≫
      (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀).app ((Presheaf.stalkFunctor C p₀).obj X) =
    𝟙 ((Presheaf.stalkFunctor C p₀).obj X)

Tactic:
by
    dsimp [Presheaf.stalkFunctor, toSkyscraperPresheaf]
    ext
    simp only [Functor.comp_obj, Functor.op_obj, ι_colimMap_assoc, skyscraperPresheaf_obj,
      Functor.whiskerLeft_app, Category.comp_id]
    split_ifs with h
    · simp [skyscraperPresheafStalkOfSpecializes]
      rfl
    · simp only [skyscraperPresheafStalkOfSpecializes, colimit.isoColimitCocone_ι_hom,
        skyscraperPresheafCoconeOfSpecializes_pt, skyscraperPresheafCoconeOfSpecializes_ι_app,
        Functor.comp_obj, Functor.op_obj, skyscraperPresheaf_obj, Functor.const_obj_obj]
      rw [comp_eqToHom_iff]
      apply ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext

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

Goal state before:
pp: case refine_3
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝¹ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this✝ : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε

Tactic:
have I :=
        calc
          ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| = |ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))| := by
            rw [abs_mul, abs_of_nonneg (inv_pos.2 εpos).le]
          _ = |ε⁻¹ * dist x y - ε⁻¹ * dist (Ψ x) (Ψ y)| := by congr; ring
          _ ≤ 1 := le_of_lt (abs_sub_lt_one_of_floor_eq_floor this)

Goal state after:
case refine_3
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝¹ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this✝ : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
I : ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| ≤ 1
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
⊢ IsCompact (⋂₀ s)

Tactic:
refine QuasiSeparatedSpace.isCompact_sInter hf (fun t ht ↦ ?_) (fun t ht ↦ ?_)

Goal state after:
case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t

case refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ IsCompact t