mathlib-initiative/mathlib-tactics huggingface dataset:
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
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
x y z : X ⊕ Y
⊢ f z ∈ range Φ ∪ range Ψ

Tactic:
cases z

Goal state after:
case inl
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
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val✝ : X
⊢ f (inl val✝) ∈ range Φ ∪ range Ψ

case inr
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
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val✝ : Y
⊢ f (inr val✝) ∈ range Φ ∪ range Ψ
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
| a

Tactic:
rw [← OrderDual.ofDual_toDual a, ← (gi hG).l_u_eq a]

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
| OrderDual.ofDual (OrderDual.toDual ((⇑OrderDual.toDual ∘ kernel) ((hull T ∘ ⇑OrderDual.ofDual) a)))
Module: Mathlib.Topology.Order.NhdsSet

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
h : Nonempty ↑(Ioi a)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ i, a < i ∧ Iio i ⊆ s

Tactic:
exact ⟨b, hab, Iio_subset_Iio_union_Ico.trans (union_subset hs.2 hbs)⟩

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
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
⊢ ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q

Tactic:
intro p q hp hq

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
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case h₂
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
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
⊢ ∀ b ∈ (fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = toGHSpace X} ×ˢ {b | ⟦b⟧ = toGHSpace Y},
    hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ b

Tactic:
rintro b ⟨⟨p, q⟩, ⟨hp, hq⟩, rfl⟩
      exact B p q hp hq

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊥
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : x✝.Compatible
⊢ ∀ (x x_1 : (F ⋙ coyoneda.obj (op c)).obj (op ⊥)), x = x_1

Tactic:
apply it.hom_ext

Goal state after:
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
⊢ IsGδ s

Tactic:
by_cases! hse : s = ∅
        · simp_all
        -- pick `f` such that `s = f ⁻¹' {0} = ⋂ n, f ⁻¹' (Iio (1 / (n + 1)))`
        obtain ⟨f, hf, hfr⟩ := h s hs
        refine isGδ_iff_eq_iInter_nat.2 ⟨fun n => f ⁻¹' (Iio (1 / (n + 1))),
          fun n => ?_, ?_⟩
        · exact f.continuous.isOpen_preimage _ isOpen_Iio
        · simp only [hf, ← preimage_iInter,
            ← preimage_range_inter (s := ⋂ (n : ℕ), Iio (1 / (n + 1) : ℝ)), inter_iInter]
          congr
          rw [eq_comm, eq_singleton_iff_unique_mem]
          refine ⟨mem_iInter_of_mem fun n => ?_, fun x h => ?_⟩
          · exact ⟨(hf ▸ hse : (f ⁻¹' {0}).Nonempty), show 0 < (1 / (n + 1) : ℝ) by positivity⟩
          · apply le_antisymm
            · simp only [mem_iInter, mem_inter_iff, mem_Iio] at h
              exact ge_of_tendsto' tendsto_one_div_add_atTop_nhds_zero_nat (fun n => (h n).2.le)
            · rcases (mem_iInter.1 h 0).1 with ⟨x, rfl⟩
              exact (hfr x).1

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
inst✝ : HasColimits C
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
⊢ colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝ ≫
      colimMap
          ((OpenNhds.inclusion p₀).op.whiskerLeft
            {
              app := fun U ↦
                if h : p₀ ∈ unop U then X.germ (unop U) p₀ h ≫ 𝟙 (X.stalk p₀) ≫ eqToHom ⋯
                else (⋯ ▸ terminalIsTerminal).from (X.obj U),
              naturality := ⋯ }) ≫
        (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝ ≫ 𝟙 (colimit ((OpenNhds.inclusion p₀).op ⋙ X))

Tactic:
simp only [Functor.comp_obj, Functor.op_obj, ι_colimMap_assoc, skyscraperPresheaf_obj,
      Functor.whiskerLeft_app, Category.comp_id]

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
inst✝ : HasColimits C
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
⊢ (if h : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j✝) then
        X.germ ((OpenNhds.inclusion p₀).obj (unop j✝)) p₀ ⋯ ≫ 𝟙 (X.stalk p₀) ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j✝))))) ≫
      colimit.ι ((OpenNhds.inclusion p₀).op ⋙ skyscraperPresheaf p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X))) j✝ ≫
        (skyscraperPresheafStalkOfSpecializes p₀ (colimit ((OpenNhds.inclusion p₀).op ⋙ X)) ⋯).hom =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝
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)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
⊢ LeftInverse
    (fun x_1 ↦
      match x_1 with
      | (⟨y, hy⟩, WithTopology.toTopology .(⊥) g) =>
        ⟨{ base := y, germ := (ConcreteCategory.hom (F.germ U y hy)) (surjInv ⋯ g) }, hy⟩)
    fun s ↦ (⟨(↑s).base, ⋯⟩, WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑s).germ)))

Tactic:
rintro ⟨⟨base, s⟩, hs⟩
    simp only
    congr 2
    rw [leftInverse_surjInv (hF_bij _ _), surjInv_eq (hF_bij _ _).surjective]

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

Goal state before:
pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
⊢ x ∈ U → ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1

Tactic:
hxU

Goal state after:
case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map T))
U : Opens ↑X
t : ToType (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
⊢ ∃ U_1 f, (Presheaf.imageSieve T t).arrows f ∧ x ∈ U_1
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
y : Y
A : ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl default, inr y)
⊢ ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ diam univ + 1 + diam univ

Tactic:
have B : dist (inl default) (inr y) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) :=
      calc
        dist (inl (default : X)) (inr y) = dist default default + 1 + dist default y := rfl
        _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by
          gcongr <;>
            exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Goal state after:
case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
y : Y
A : ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl default, inr y)
B : dist (inl default) (inr y) ≤ diam univ + 1 + diam univ
⊢ ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ diam univ + 1 + diam univ
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
⊢ (𝓝 x).HasBasis (fun t ↦ t ∈ {s | IsClopen s} ∧ x ∈ t) id

Tactic:
simpa [and_comm] using nhds_basis_clopens x

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : CompleteLinearOrder β
inst✝¹⁰ : DenselyOrdered β
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
cX : Convex ℝ X
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
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
by
  have hlsc : LowerSemicontinuousOn (fun x => ⨆ y ∈ Y, f x y) X := fun x hx ↦ by
    apply lowerSemicontinuousWithinAt_iSup
    intro i
    exact lowerSemicontinuousWithinAt_iSup fun i_1 ↦ hfy i i_1 x hx
  have husc : UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y := fun y hy ↦ by
    apply upperSemicontinuousWithinAt_iInf
    intro i
    exact upperSemicontinuousWithinAt_iInf fun i_1 ↦ hfx i i_1 y hy
  obtain ⟨a, ha, ha'⟩ := LowerSemicontinuousOn.exists_isMinOn
   ne_X kX hlsc
  obtain ⟨b, hb, hb'⟩ := UpperSemicontinuousOn.exists_isMaxOn ne_Y kY husc
  use a, ha, b, hb
  rw [isSaddlePointOn_iff' ha hb]
  refine le_trans (le_iInf₂ ha') ?_
  refine le_trans ?_ (iSup₂_le_iff.mpr hb')
  rw [minimax' ne_X cX kX hfy hfy' cY hfx hfx']

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
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module ℝ E
inst✝¹² : IsTopologicalAddGroup E
inst✝¹¹ : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
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
inst✝⁷ : IsTopologicalAddGroup F
inst✝⁶ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝⁵ : TopologicalSpace β
inst✝⁴ : OrderTopology β
γ : Type u_5
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
ι : β ↪o γ
hι : Continuous ⇑ι
φ : E → F → γ := fun x y ↦ ι (f x y)
hφx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ φ x y) Y
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
have hφx' (x) (hx : x ∈ X) : QuasiconcaveOn ℝ Y fun y ↦ φ x y := by
    convert! (hfx' x hx).monotone_comp ι.monotone

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
cX : Convex ℝ X
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
inst✝⁷ : IsTopologicalAddGroup F
inst✝⁶ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝⁵ : TopologicalSpace β
inst✝⁴ : OrderTopology β
γ : Type u_5
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
ι : β ↪o γ
hι : Continuous ⇑ι
φ : E → F → γ := fun x y ↦ ι (f x y)
hφx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ φ x y) Y
hφx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ φ x y
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b