awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : Preorder β
a a' : E
b b' : F
ha' : a' ∈ X
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
h' : IsSaddlePointOn X Y f a' b'
⊢ IsSaddlePointOn X Y f a b'

Tactic:
fun x hx y hy ↦
  le_trans (h a' ha' y hy) (h' x hx b hb)

Premises used: IsSaddlePointOn, le_trans
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : Preorder β
a a' : E
b b' : F
ha : a ∈ X
hb' : b' ∈ Y
h : IsSaddlePointOn X Y f a b
h' : IsSaddlePointOn X Y f a' b'
⊢ IsSaddlePointOn X Y f a' b

Tactic:
IsSaddlePointOn.swap_left ha hb' h' h

Premises used: IsSaddlePointOn.swap_left
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b

Tactic:
⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, h'⟩ x hx y hy ↦ ?_⟩

Premises used: LE.le, And.intro, Iff.intro, _private.0.isSaddlePointOn_iff.match_1
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
refine_1 : ∀ (h : IsSaddlePointOn X Y f a b), ⨆ y ∈ Y, f a y = f a b
refine_2 : ∀ (h : IsSaddlePointOn X Y f a b), ⨅ x ∈ X, f x b = f a b
refine_3 :
  ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b →
    ∀ (x : E) (hx : x ∈ X) (y : F) (hy : y ∈ Y) (h : ⨆ y ∈ Y, f a y = f a b) (h' : ⨅ x ∈ X, f x b = f a b),
      f a y ≤ f x b
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, h'⟩ x hx y hy ↦ ?_⟩
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
refine_1 : ⨆ y ∈ Y, f a y ≤ f a b
refine_1₁ : f a b ≤ ⨆ y ∈ Y, f a y
⊢ ⨆ y ∈ Y, f a y = f a b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
refine_1 : ∀ (i : F) (i_1 : i ∈ Y), f a i ≤ f a b
⊢ ⨆ y ∈ Y, f a y ≤ f a b

Tactic:
simp only [iSup_le_iff]

Premises used: iSup_le_iff
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ∀ (i : F) (i_1 : i ∈ Y), f a i ≤ f a b

Tactic:
h a ha
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ∀ (i : F) (i_1 : i ∈ Y), f a i ≤ f a b

Tactic:
exact h a ha
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ f a b ≤ ⨆ y ∈ Y, f a y

Tactic:
apply le_iSup₂ b hb

Premises used: le_iSup₂
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
refine_2 : ⨅ x ∈ X, f x b ≤ f a b
refine_2₁ : f a b ≤ ⨅ x ∈ X, f x b
⊢ ⨅ x ∈ X, f x b = f a b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨅ x ∈ X, f x b ≤ f a b

Tactic:
apply iInf₂_le a ha

Premises used: iInf₂_le
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
refine_2 : ∀ (i : E) (i_1 : i ∈ X), f a b ≤ f i b
⊢ f a b ≤ ⨅ x ∈ X, f x b

Tactic:
simp only [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
x : E
hx : x ∈ X
⊢ f a b ≤ f x b

Tactic:
h x hx b hb
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
x : E
hx : x ∈ X
⊢ f a b ≤ f x b

Tactic:
exact h x hx b hb
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
trans : f a y ≤ f a b
trans₁ : f a b ≤ f x b
⊢ f a y ≤ f x b

Tactic:
trans f a b
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
rw : f a y ≤ ⨆ y ∈ Y, f a y
⊢ f a y ≤ f a b

Tactic:
rw [← h]
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a y ≤ ⨆ y ∈ Y, f a y

Tactic:
apply le_iSup₂ y hy

Premises used: le_iSup₂
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
rw : ⨅ x ∈ X, f x b ≤ f x b
⊢ f a b ≤ f x b

Tactic:
rw [← h']
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ f x b

Tactic:
apply iInf₂_le x hx

Premises used: iInf₂_le
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
rw : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b ↔ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
⊢ IsSaddlePointOn X Y f a b ↔ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)

Tactic:
rw [isSaddlePointOn_iff ha hb]

Premises used: isSaddlePointOn_iff
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b ↔ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)

Tactic:
⟨fun ⟨h, h'⟩ ↦ ?_, fun h ↦ ⟨?_, ?_⟩⟩

Premises used: iInf, iSup, LE.le, And.intro, Iff.intro, _private.0.isSaddlePointOn_iff.match_1
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
refine_1 :
  ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b →
    ∀ (h : ⨆ y ∈ Y, f a y = f a b) (h' : ⨅ x ∈ X, f x b = f a b), LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
refine_2 : ∀ (h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)), ⨆ y ∈ Y, f a y = f a b
refine_3 : ∀ (h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)), ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b ↔ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)

Tactic:
refine ⟨fun ⟨h, h'⟩ ↦ ?_, fun h ↦ ⟨?_, ?_⟩⟩
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)

Tactic:
le_trans (le_of_eq h) (le_of_eq h'.symm)

Premises used: le_of_eq, Eq.symm, le_trans
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h_1 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)

Tactic:
exact le_trans (le_of_eq h) (le_of_eq h'.symm)

Premises used: le_of_eq, Eq.symm, le_trans
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
refine_2 : ⨆ y ∈ Y, f a y ≤ f a b
refine_2₁ : f a b ≤ ⨆ y ∈ Y, f a y
⊢ ⨆ y ∈ Y, f a y = f a b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
⊢ ⨆ y ∈ Y, f a y ≤ f a b

Tactic:
le_trans h (iInf₂_le a ha)

Premises used: iInf₂_le, le_trans
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
⊢ ⨆ y ∈ Y, f a y ≤ f a b

Tactic:
exact le_trans h (iInf₂_le a ha)

Premises used: iInf₂_le, le_trans
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
⊢ f a b ≤ ⨆ y ∈ Y, f a y

Tactic:
apply le_iSup₂ b hb

Premises used: le_iSup₂
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
refine_3 : ⨅ x ∈ X, f x b ≤ f a b
refine_3₁ : f a b ≤ ⨅ x ∈ X, f x b
⊢ ⨅ x ∈ X, f x b = f a b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
⊢ ⨅ x ∈ X, f x b ≤ f a b

Tactic:
apply iInf₂_le a ha

Premises used: iInf₂_le
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
⊢ f a b ≤ ⨅ x ∈ X, f x b

Tactic:
apply le_trans (le_iSup₂ b hb) h

Premises used: le_iSup₂, le_trans
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b

Tactic:
rw [isSaddlePointOn_iff ha hb] at h

Premises used: isSaddlePointOn_iff
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
left : ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b
right : ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b

Tactic:
constructor
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
left : ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ f a b
left₁ : f a b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
left : LE.le.{u_3} (α := β) (⨅ x ∈ X, ⨆ y ∈ Y, f x y) (⨆ y ∈ Y, f a y)
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ f a b

Tactic:
rw [← h.1]

Premises used: And.left
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ LE.le.{u_3} (α := β) (⨅ x ∈ X, ⨆ y ∈ Y, f x y) (⨆ y ∈ Y, f a y)

Tactic:
le_trans (iInf₂_le a ha) (le_rfl)

Premises used: le_rfl, iInf₂_le, le_trans
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ LE.le.{u_3} (α := β) (⨅ x ∈ X, ⨆ y ∈ Y, f x y) (⨆ y ∈ Y, f a y)

Tactic:
exact le_trans (iInf₂_le a ha) (le_rfl)

Premises used: le_rfl, iInf₂_le, le_trans
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
left : LE.le.{u_3} (α := β) (⨅ x ∈ X, f x b) (⨅ x ∈ X, ⨆ y ∈ Y, f x y)
⊢ f a b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

Tactic:
rw [← h.2]

Premises used: And.right
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
left : ∀ (i : E) (j : i ∈ X), f i b ≤ ⨆ y ∈ Y, f i y
⊢ LE.le.{u_3} (α := β) (⨅ x ∈ X, f x b) (⨅ x ∈ X, ⨆ y ∈ Y, f x y)

Tactic:
apply iInf₂_mono

Premises used: iInf₂_mono
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
left : x ∈ X → f x b ≤ ⨆ y ∈ Y, f x y
⊢ ∀ (j : x ∈ X), f x b ≤ ⨆ y ∈ Y, f x y

Tactic:
_
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
j : x ∈ X
⊢ f x b ≤ ⨆ y ∈ Y, f x y

Tactic:
apply le_iSup₂ b hb

Premises used: le_iSup₂
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
right : ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ f a b
right₁ : f a b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
right : LE.le.{u_3} (α := β) (⨆ y ∈ Y, ⨅ x ∈ X, f x y) (⨆ y ∈ Y, f a y)
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ f a b

Tactic:
rw [← h.1]

Premises used: And.left
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
right : ∀ (i : F) (j : i ∈ Y), ⨅ x ∈ X, f x i ≤ f a i
⊢ LE.le.{u_3} (α := β) (⨆ y ∈ Y, ⨅ x ∈ X, f x y) (⨆ y ∈ Y, f a y)

Tactic:
apply iSup₂_mono

Premises used: iSup₂_mono
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
y : F
right : y ∈ Y → ⨅ x ∈ X, f x y ≤ f a y
⊢ ∀ (j : y ∈ Y), ⨅ x ∈ X, f x y ≤ f a y

Tactic:
_
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
y : F
j : y ∈ Y
⊢ ⨅ x ∈ X, f x y ≤ f a y

Tactic:
apply iInf₂_le a ha

Premises used: iInf₂_le
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
right : LE.le.{u_3} (α := β) (⨅ x ∈ X, f x b) (⨆ y ∈ Y, ⨅ x ∈ X, f x y)
⊢ f a b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y

Tactic:
rw [← h.2]

Premises used: And.right
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ LE.le.{u_3} (α := β) (⨅ x ∈ X, f x b) (⨆ y ∈ Y, ⨅ x ∈ X, f x y)

Tactic:
apply le_trans (le_rfl) (le_iSup₂ b hb)

Premises used: le_rfl, le_iSup₂, le_trans
-- Module: Mathlib.Order.ScottContinuity.Complete
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
h : ScottContinuous f
x : Set α
d₁ : x.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) x
rw rw₁ : f (sSup x) = f (sSup x)
⊢ f (sSup x) = sSup (f '' x)

Tactic:
rw [IsLUB.sSup_eq (h d₁ d₂ (isLUB_iff_sSup_eq.mpr rfl))]

Premises used: Iff.mpr, isLUB_iff_sSup_eq, IsLUB.sSup_eq, rfl
-- Module: Mathlib.Order.ScottContinuity.Complete
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → f (sSup d) = sSup (f '' d)
x : Set α
d₁ : x.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) x
x_1 : α
hda : IsLUB x x_1
rw : sSup (f '' x) = f x_1
rw₁ : f (sSup x) = f x_1
rw₂ rw₃ : f x_1 = f x_1
⊢ IsLUB (f '' x) (f x_1)

Tactic:
rw [isLUB_iff_sSup_eq, ← (h d₁ d₂), IsLUB.sSup_eq hda]

Premises used: isLUB_iff_sSup_eq, IsLUB.sSup_eq
-- Module: Mathlib.Order.ScottContinuity.Complete
Goal:
β : Type u_2
inst : CompleteLinearOrder β
a : β
d : Set β
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d
rw : Eq (α := β) (⨆ b ∈ d, min a b) (sSup ((fun (b : β) ↦ min a b) '' d))
rw₁ rw₂ : Eq.{u_2 + 1} (α := β) (⨆ b ∈ d, min a b) (⨆ a_1 ∈ d, min a a_1)
⊢ min a (sSup d) = sSup ((fun (b : β) ↦ min a b) '' d)

Tactic:
rw [inf_sSup_eq, sSup_image]

Premises used: inf_sSup_eq, sSup_image
-- Module: Mathlib.Order.ScottContinuity.Complete
Goal:
β : Type u_2
inst : CompleteLinearOrder β
b : β
d : Set β
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β) ↦ x1 ≤ x2) d
rw : Eq (α := β) (⨆ a ∈ d, min a b) (sSup ((fun (a : β) ↦ min a b) '' d))
rw₁ rw₂ : Eq.{u_2 + 1} (α := β) (⨆ a ∈ d, min a b) (⨆ a ∈ d, min a b)
⊢ min (sSup d) b = sSup ((fun (a : β) ↦ min a b) '' d)

Tactic:
rw [sSup_inf_eq, sSup_image]

Premises used: sSup_image, sSup_inf_eq
-- Module: Mathlib.Order.ScottContinuity.Complete
Goal:
β : Type u_2
inst : CompleteLinearOrder β
⊢ ScottContinuous (β := β) fun (x : β × β) ↦
    match (motive := β × β → β) x with
    | (a, b) => min a b

Tactic:
ScottContinuous.fromProd (fun a => scottContinuous_inf_right a) scottContinuous_inf_left

Premises used: scottContinuous_inf_right, ScottContinuous.fromProd, scottContinuous_inf_left
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ :
  ∀ (a : α), ScottContinuousOn.{u_2, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.snd '' d) '' D) fun (b : β) ↦ f (a, b)
h₂ :
  ∀ (b : β), ScottContinuousOn.{u_1, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.fst '' d) '' D) fun (a : α) ↦ f (a, b)
h₁' : ∀ (a : α), Monotone.{u_2, u_3} (β := γ) fun (b : β) ↦ f (a, b)
h₂' : ∀ (b : β), Monotone.{u_1, u_3} (β := γ) fun (a : α) ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
x : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
a : (↑(Prod.fst '' d) : Type u_1)
rw :
  IsLUB.{u_3} (α := γ) ((fun (x : β) ↦ f ((↑a : α), x)) '' Prod.snd '' d) ((fun (b : β) ↦ f ((↑a : α), b)) (p1, p2).2)
⊢ IsLUB (f '' SProd.sprod (α := Set α) {(↑a : α)} (Prod.snd '' d)) ((fun (b : β) ↦ f ((↑a : α), b)) (p1, p2).2)

Tactic:
rw [singleton_prod, image_image f (fun b ↦ (a, b))]

Premises used: Set.image_image, Set.singleton_prod, Prod.mk, Subtype.val
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ :
  ∀ (a : α), ScottContinuousOn.{u_2, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.snd '' d) '' D) fun (b : β) ↦ f (a, b)
h₂ :
  ∀ (b : β), ScottContinuousOn.{u_1, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.fst '' d) '' D) fun (a : α) ↦ f (a, b)
h₁' : ∀ (a : α), Monotone.{u_2, u_3} (β := γ) fun (b : β) ↦ f (a, b)
h₂' : ∀ (b : β), Monotone.{u_1, u_3} (β := γ) fun (a : α) ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
x : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
a : (↑(Prod.fst '' d) : Type u_1)
⊢ IsLUB.{u_3} (α := γ) ((fun (x : β) ↦ f ((↑a : α), x)) '' Prod.snd '' d) ((fun (b : β) ↦ f ((↑a : α), b)) (p1, p2).2)

Tactic:
h₁ _ (mem_image_of_mem (fun d ↦ Prod.snd '' d) hX) (Nonempty.image Prod.snd hd₁)
        (DirectedOn.snd hd₂) (isLUB_prod.mp hdp).2

Premises used: isLUB_prod, And.right, Set.mem_image_of_mem, DirectedOn.snd, Set.Nonempty.image, Iff.mp, Set.image, Prod.snd
-- Module: Mathlib.Order.ScottContinuity.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ :
  ∀ (a : α), ScottContinuousOn.{u_2, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.snd '' d) '' D) fun (b : β) ↦ f (a, b)
h₂ :
  ∀ (b : β), ScottContinuousOn.{u_1, u_3} (β := γ) ((fun (d : Set (α × β)) ↦ Prod.fst '' d) '' D) fun (a : α) ↦ f (a, b)
h₁' : ∀ (a : α), Monotone.{u_2, u_3} (β := γ) fun (b : β) ↦ f (a, b)
h₂' : ∀ (b : β), Monotone.{u_1, u_3} (β := γ) fun (a : α) ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) d
x : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
a : (↑(Prod.fst '' d) : Type u_1)
⊢ IsLUB.{u_3} (α := γ) ((fun (x : β) ↦ f ((↑a : α), x)) '' Prod.snd '' d) ((fun (b : β) ↦ f ((↑a : α), b)) (p1, p2).2)

Tactic:
exact h₁ _ (mem_image_of_mem (fun d ↦ Prod.snd '' d) hX) (Nonempty.image Prod.snd hd₁)
        (DirectedOn.snd hd₂) (isLUB_prod.mp hdp).2

Premises used: isLUB_prod, And.right, Set.mem_image_of_mem, DirectedOn.snd, Set.Nonempty.image, Iff.mp, Set.image, Prod.snd