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

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
⊢ 𝓝 x = ⨆ i, comap (fun x_1 ↦ x) (𝓝 i) ⊓ comap (fun x ↦ x) (𝓝 i)

Tactic:
comap_id'

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
⊢ 𝓝 x = ⨆ i, comap (fun x_1 ↦ x) (𝓝 i) ⊓ 𝓝 i
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, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
hsup_y : ∀ x ∈ X, IsLUB {x_1 | ∃ y ∈ Y, f x y = x_1} (sup_y x)
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
hinf_x : ∀ y ∈ Y, IsGLB {x | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y)
sup_inf : β
hsup_inf : IsLUB {x | ∃ y ∈ Y, inf_x y = x} sup_inf
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ inf_x y ≤ f x y

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, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
hsup_y : ∀ x ∈ X, IsLUB {x_1 | ∃ y ∈ Y, f x y = x_1} (sup_y x)
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
hinf_x : ∀ y ∈ Y, IsGLB {x | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y)
sup_inf : β
hsup_inf : IsLUB {x | ∃ y ∈ Y, inf_x y = x} sup_inf
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f x y ≤ sup_y x

Tactic:
· exact (hinf_x y hy).1 ⟨x, hx, rfl⟩

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, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
hsup_y : ∀ x ∈ X, IsLUB {x_1 | ∃ y ∈ Y, f x y = x_1} (sup_y x)
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
hinf_x : ∀ y ∈ Y, IsGLB {x | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y)
sup_inf : β
hsup_inf : IsLUB {x | ∃ y ∈ Y, inf_x y = x} sup_inf
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f x y ≤ sup_y 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
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 ⇑ι
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
by
  -- Reduce to the cae of EReal-valued functions
  let φ : E → F → γ := fun x y ↦ ι (f x y)
  -- suffices : ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y φ a b
  have hφx (x) (hx : x ∈ X) : UpperSemicontinuousOn (fun y ↦ φ x y) Y := by
    convert! Continuous.comp_upperSemicontinuousOn hι (hfx x hx) ι.monotone
  have hφx' (x) (hx : x ∈ X) : QuasiconcaveOn ℝ Y fun y ↦ φ x y := by
    convert! (hfx' x hx).monotone_comp ι.monotone
  have hφy (y) (hy : y ∈ Y) : LowerSemicontinuousOn (fun x ↦ φ x y) X := by
    convert! Continuous.comp_lowerSemicontinuousOn hι (hfy y hy) ι.monotone
  have hφy' (y) (hy : y ∈ Y) : QuasiconvexOn ℝ X fun x ↦ φ x y := by
    convert! (hfy' y hy).monotone_comp ι.monotone
  obtain ⟨a, ha, b, hb, hab⟩ :=
    exists_isSaddlePointOn' ne_X kX hφy hφy' cY kY hφx hφx' cX ne_Y
  use a, ha, b, hb
  intro x hx y hy
  simpa only [OrderEmbedding.le_iff_le, φ] using hab x hx y hy

Goal state after: