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

Goal state before:
pp: case a
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ((Finset.range #J).biUnion fun x ↦
      {x_1 ∈ (logSizeBallSeq J hJ a c x).finset |
        edist (logSizeBallSeq J hJ a c x).point x_1 ≤ (↑(logSizeBallSeq J hJ a c x).radius - 1) * c}) ⊆
    J

Tactic:
rw [Finset.biUnion_subset_iff_forall_subset]

Goal state after:
case a
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ∀ x ∈ Finset.range #J,
    {x_1 ∈ (logSizeBallSeq J hJ a c x).finset |
        edist (logSizeBallSeq J hJ a c x).point x_1 ≤ (↑(logSizeBallSeq J hJ a c x).radius - 1) * c} ⊆
      J
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
Hj : y j = 0 ∨ y j = 1
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
⊢ (↑(p.toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = x

pp: case inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
y : N → ↑I
j : N
Hj : y j = 0 ∨ y j = 1
Hne : j ≠ i
⊢ (↑(p.toContinuousMap (y i)) fun j ↦ y ↑j) = x

Tactic:
· rcases Hj with Hj | Hj <;> simp only [Hj, p.coe_toContinuousMap, p.source, p.target] <;> rfl

Goal state after:
case inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
y : N → ↑I
j : N
Hj : y j = 0 ∨ y j = 1
Hne : j ≠ i
⊢ (↑(p.toContinuousMap (y i)) fun j ↦ y ↑j) = x
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: case h₁
α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist x ↑t ≤ infEDist y ↑t + edist x y

Tactic:
apply infEDist_le_infEDist_add_edist

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

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist y ↑t + (edist x y + hausdorffEDist ↑s ↑t) ≤ infEDist y ↑t + (edist (x, s) (y, t) + edist (x, s) (y, t))

Tactic:
gcongr <;> apply_rules [le_max_left, le_max_right]

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
⊢ packingNumber ε A = packingNumber (2 * (ε / 2)) A

Tactic:
ring_nf

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞

Tactic:
rw [infsep, ENNReal.toReal_eq_zero_iff]

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
⊢ ⇑ofSnowflaking ⁻¹' closedBall x r = closedBall (toSnowflaking x) (r ^ α)

Tactic:
ext ⟨y⟩
  simp (disch := positivity) [Real.rpow_le_rpow_iff]

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
xX : X
h✝ : xX ∈ univ
this : ∃ y ∈ range Ψ, dist (Φ xX) y < diam univ + 1 + diam univ
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ

Tactic:
rcases this with ⟨y, hy, dy⟩

Goal state after:
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
xX : X
h✝ : xX ∈ univ
y : ↥(lp (fun n ↦ ℝ) ∞)
hy : y ∈ range Ψ
dy : dist (Φ xX) y < diam univ + 1 + diam univ
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ IsLowerSet sᶜ ↔ IsUpperSet s

Tactic:
isUpperSet_compl.symm,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ IsUpperSet sᶜᶜ ↔ IsUpperSet s
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsUpper α
inst✝⁴ : OrderTop α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsUpper β
inst✝ : OrderTop β
⊢ instTopologicalSpaceProd = upper (α × β)

Tactic:
suffices IsLower (α × β)ᵒᵈ from IsLower.topology_eq_lowerTopology (α := (α × β)ᵒᵈ)
    exact instIsLowerProd (α := αᵒᵈ) (β := βᵒᵈ)

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
⊢ kernel (hull T a) = a

Tactic:
by
  conv_rhs => rw [← OrderDual.ofDual_toDual a, ← (gi hG).l_u_eq a]
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
⊢ Ici b ⊆ Ioi a ↔ a < b

Tactic:
Ici_subset_Ioi

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
⊢ a < b ↔ a < b
Module: Mathlib.Topology.Partial

Goal state before:
pp: case mpr
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
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ f.preimage s ∈ 𝓝 x

Tactic:
change f.preimage s ∈ 𝓝 x

Goal state after:
case mpr
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
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ f.preimage s ∈ 𝓝 x
Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology

Goal state before:
pp: 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)

pp: 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)

Tactic:
case inl => simp

Goal state after:
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.Separation.LinearUpperLowerSetTopology

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : Topology.IsUpperSet α
s : Set α
a : α
ha : a ∈ s
hcst : Disjoint (closure s) ∅
hsct : Disjoint s (closure ∅)
⊢ Disjoint (nhdsSet s) (nhdsSet ∅)

pp: case inr.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
b : α
hb : b ∈ t
⊢ Disjoint (nhdsSet s) (nhdsSet t)

Tactic:
case inl => simp

Goal state after:
case inr.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
b : α
hb : b ∈ t
⊢ Disjoint (nhdsSet s) (nhdsSet t)
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.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ ((skyscraperPresheaf p₀ a).map i ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj V)) =
    (if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)) ≫
      (skyscraperPresheaf p₀ b).map i

Tactic:
by
    simp only [skyscraperPresheaf_map]
    by_cases hV : p₀ ∈ V.unop
    · have hU : p₀ ∈ U.unop := leOfHom i.unop hV
      simp only [skyscraperPresheaf_obj, hU, hV, ↓reduceDIte, eqToHom_trans_assoc, Category.assoc,
        eqToHom_trans]
    · apply ((if_neg hV).symm.ndrec terminalIsTerminal).hom_ext

Goal state after:
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
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ c.ι.app (op ⊤) = c.ι.app U

Tactic:
← c.w (homOfLE <| (le_top : unop U ≤ _)).op

Goal state after:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom ⋯ ≫
      eqToHom ⋯ ≫ ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map (homOfLE ⋯).op ≫ c.ι.app (op (unop U)) =
    c.ι.app U
Module: Mathlib.Topology.Sheaves.MayerVietoris

Goal state before:
pp: case inr
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:
exact ⟨_, _, ⟨Sieve.ofArrows_mk _ _ WalkingPair.right, hx⟩⟩

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n : ℕ
p : Fin (n + 1) → X
F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)
H : (k : Fin n) → (F k).Homotopy (G k)
⊢ (concat p F).Homotopy (concat p G)

Tactic:
induction n with
  | zero =>
    rw [concat_zero, concat_zero]
    exact refl (Path.refl _)
  | succ n ih =>
    rw [concat_succ, concat_succ]
    exact hcomp (ih _ _ _ (fun k ↦ H k.castSucc)) (H (last n))

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
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e ↦ ‖F e x - f x‖) atTop (𝓝 0)
n : ι
hn : ‖F n x - f x‖ < ε
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε

Tactic:
refine ⟨{y | ‖F n y - f y‖ < ε}, ⟨isOpen_lt (by fun_prop) continuous_const |>.mem_nhds hn, ?_⟩⟩

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
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e ↦ ‖F e x - f x‖) atTop (𝓝 0)
n : ι
hn : ‖F n x - f x‖ < ε
⊢ ∀ᶠ (n_1 : ι) in atTop, ∀ y ∈ {y | ‖F n y - f y‖ < ε}, ‖F n_1 y - f y‖ < ε
Module: Mathlib.Topology.UniformSpace.Path

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
x y z : X
U : Set (X × X)
hU : U ∈ 𝓤 X
x✝² x✝¹ : Path x y × Path y z
t : ↑I
fst✝¹ : Path x y
snd✝¹ : Path y z
fst✝ : Path x y
snd✝ : Path y z
x✝ :
  ((fst✝¹, snd✝¹), fst✝, snd✝) ∈
    entourageProd {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).1} {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).2}
h₁ : (fst✝¹, fst✝) ∈ {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).1}
h₂ : (snd✝¹, snd✝) ∈ {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).2}
⊢ ((Function.uncurry trans (fst✝¹, snd✝¹), Function.uncurry trans (fst✝, snd✝)).1 t,
      (Function.uncurry trans (fst✝¹, snd✝¹), Function.uncurry trans (fst✝, snd✝)).2 t) ∈
    U

Tactic:
by_cases ht : (t : ℝ) ≤ 2⁻¹

Goal state after:
case pos
X : Type u_1
inst✝ : UniformSpace X
x y z : X
U : Set (X × X)
hU : U ∈ 𝓤 X
x✝² x✝¹ : Path x y × Path y z
t : ↑I
fst✝¹ : Path x y
snd✝¹ : Path y z
fst✝ : Path x y
snd✝ : Path y z
x✝ :
  ((fst✝¹, snd✝¹), fst✝, snd✝) ∈
    entourageProd {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).1} {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).2}
h₁ : (fst✝¹, fst✝) ∈ {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).1}
h₂ : (snd✝¹, snd✝) ∈ {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).2}
ht : ↑t ≤ 2⁻¹
⊢ ((Function.uncurry trans (fst✝¹, snd✝¹), Function.uncurry trans (fst✝, snd✝)).1 t,
      (Function.uncurry trans (fst✝¹, snd✝¹), Function.uncurry trans (fst✝, snd✝)).2 t) ∈
    U

case neg
X : Type u_1
inst✝ : UniformSpace X
x y z : X
U : Set (X × X)
hU : U ∈ 𝓤 X
x✝² x✝¹ : Path x y × Path y z
t : ↑I
fst✝¹ : Path x y
snd✝¹ : Path y z
fst✝ : Path x y
snd✝ : Path y z
x✝ :
  ((fst✝¹, snd✝¹), fst✝, snd✝) ∈
    entourageProd {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).1} {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).2}
h₁ : (fst✝¹, fst✝) ∈ {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).1}
h₂ : (snd✝¹, snd✝) ∈ {γ | ∀ (t : ↑I), (γ.1 t, γ.2 t) ∈ (U, U).2}
ht : ¬↑t ≤ 2⁻¹
⊢ ((Function.uncurry trans (fst✝¹, snd✝¹), Function.uncurry trans (fst✝, snd✝)).1 t,
      (Function.uncurry trans (fst✝¹, snd✝¹), Function.uncurry trans (fst✝, snd✝)).2 t) ∈
    U
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 ∈ 𝓝Δ, F ⊓ 𝓟 Vᶜ = ⊥

Tactic:
intro V V_in

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 ∈ 𝓝Δ
⊢ F ⊓ 𝓟 Vᶜ = ⊥
Module: Mathlib.Topology.Sion

Goal state before:
pp: case insert.inr
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
s✝ : Set F
t : β
b : F
s : Set F
a✝ : b ∉ s
hs : s.Finite
X : Set 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
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun x ↦ f x b) ⁻¹' Iic t
hrec : s ⊆ Y → (∀ x ∈ X', ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
refine exists_lt_iInf_of_lt_iInf_of_sup ne_X kX hfy hfy' cY hfx hfx' hb hy1 fun x hx ↦ ?_

Goal state after:
case insert.inr
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
s✝ : Set F
t : β
b : F
s : Set F
a✝ : b ∉ s
hs : s.Finite
X : Set 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
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun x ↦ f x b) ⁻¹' Iic t
hrec : s ⊆ Y → (∀ x ∈ X', ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
x : E
hx : x ∈ X
⊢ t < max (f x b) (f x y1)