Theorem: Tutorial.isSup_of_isInf (GlimpseOfLean/Solutions/Topics/GaloisAdjunctions.lean)

State before:
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
⊢ isSupFun fun s => I (upperBounds s)
Tactic:
intro s x
State after:
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ x ∈ upperBounds s ↔ (fun s => I (upperBounds s)) s ≤ x

State before:
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ x ∈ upperBounds s ↔ (fun s => I (upperBounds s)) s ≤ x
Tactic:
constructor
State after:
case mp
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ x ∈ upperBounds s → (fun s => I (upperBounds s)) s ≤ x

case mpr
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ (fun s => I (upperBounds s)) s ≤ x → x ∈ upperBounds s

State before:
case mp
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ x ∈ upperBounds s → (fun s => I (upperBounds s)) s ≤ x
Tactic:
intro hx
State after:
case mp
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
hx : x ∈ upperBounds s
⊢ (fun s => I (upperBounds s)) s ≤ x

State before:
case mp
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
hx : x ∈ upperBounds s
⊢ (fun s => I (upperBounds s)) s ≤ x
Tactic:
exact (h _).lowerBound hx
State after:
no goals

State before:
case mpr
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ (fun s => I (upperBounds s)) s ≤ x → x ∈ upperBounds s
Tactic:
intros hx y hy
State after:
case mpr
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
hx : (fun s => I (upperBounds s)) s ≤ x
y : X
hy : y ∈ s
⊢ y ≤ x

State before:
case mpr
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
hx : (fun s => I (upperBounds s)) s ≤ x
y : X
hy : y ∈ s
⊢ y ≤ x
Tactic:
calc
  y ≤ I (upperBounds s) := (h _ y).mp (fun z hz ↦ hz hy)
  _ ≤ x                 := hx
State after:
no goals