Theorem: isSaddlePointOn_iff (Sion/Sion.lean)

State before:
E : Type u_2
F : Type u_3
β : Type u_1
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:
constructor
State after:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
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

case mpr
E : Type u_2
F : Type u_3
β : Type u_1
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 → IsSaddlePointOn X Y f a b

State before:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
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:
intro h
State after:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
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

State before:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
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:
dsimp [IsSaddlePointOn] at h
State after:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b

State before:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Tactic:
constructor
State after:
case mp.left
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y = f a b

case mp.right
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨅ x ∈ X, f x b = f a b

State before:
case mp.left
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y = f a b
Tactic:
apply le_antisymm
State after:
case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y ≤ f a b

case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ f a b ≤ ⨆ y ∈ Y, f a y

State before:
case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y ≤ f a b
Tactic:
simp only [iSup_le_iff]
State after:
case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ∀ i ∈ Y, f a i ≤ f a b

State before:
case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ∀ i ∈ Y, f a i ≤ f a b
Tactic:
exact h a ha
State after:
no goals

State before:
case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ f a b ≤ ⨆ y ∈ Y, f a y
Tactic:
apply le_iSup₂ b hb
State after:
no goals

State before:
case mp.right
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨅ x ∈ X, f x b = f a b
Tactic:
apply le_antisymm
State after:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨅ x ∈ X, f x b ≤ f a b

case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ f a b ≤ ⨅ x ∈ X, f x b

State before:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨅ x ∈ X, f x b ≤ f a b
Tactic:
apply iInf₂_le a ha
State after:
no goals

State before:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ f a b ≤ ⨅ x ∈ X, f x b
Tactic:
simp only [le_iInf_iff]
State after:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ∀ i ∈ X, f a b ≤ f i b

State before:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ∀ i ∈ X, f a b ≤ f i b
Tactic:
intro x hx
State after:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
x : E
hx : x ∈ X
⊢ f a b ≤ f x b

State before:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
x : E
hx : x ∈ X
⊢ f a b ≤ f x b
Tactic:
exact h x hx b hb
State after:
no goals

State before:
case mpr
E : Type u_2
F : Type u_3
β : Type u_1
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 → IsSaddlePointOn X Y f a b
Tactic:
rintro ⟨h, h'⟩
State after:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
⊢ IsSaddlePointOn X Y f a b

State before:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
⊢ IsSaddlePointOn X Y f a b
Tactic:
intro x hx y hy
State after:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f x b

State before:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f x b
Tactic:
suffices f a y ≤ f a b by
  apply le_trans this
  rw [← h']
  apply iInf₂_le x hx
State after:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f a b

State before:
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
this : f a y ≤ f a b
⊢ f a y ≤ f x b
Tactic:
apply le_trans this
State after:
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
this : f a y ≤ f a b
⊢ f a b ≤ f x b

State before:
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
this : f a y ≤ f a b
⊢ f a b ≤ f x b
Tactic:
rw [← h']
State after:
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
this : f a y ≤ f a b
⊢ ⨅ x ∈ X, f x b ≤ f x b

State before:
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
this : f a y ≤ f a b
⊢ ⨅ x ∈ X, f x b ≤ f x b
Tactic:
apply iInf₂_le x hx
State after:
no goals

State before:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f a b
Tactic:
rw [← h]
State after:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ ⨆ y ∈ Y, f a y

State before:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
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
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ ⨆ y ∈ Y, f a y
Tactic:
apply le_iSup₂ y hy
State after:
no goals