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

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x : X
⊢ Inf {x' | x ≤ x'} = x
Tactic:
apply (CompleteLattice.I_isInf _).eq
State after:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x : X
⊢ isInf {x' | x ≤ x'} x

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x : X
⊢ isInf {x' | x ≤ x'} x
Tactic:
intro x'
State after:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ∈ lowerBounds {x' | x ≤ x'} ↔ x' ≤ x

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ∈ lowerBounds {x' | x ≤ x'} ↔ x' ≤ x
Tactic:
constructor
State after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ∈ lowerBounds {x' | x ≤ x'} → x' ≤ x

case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ≤ x → x' ∈ lowerBounds {x' | x ≤ x'}

State before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ∈ lowerBounds {x' | x ≤ x'} → x' ≤ x
Tactic:
intro h
State after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x' ∈ lowerBounds {x' | x ≤ x'}
⊢ x' ≤ x

State before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x' ∈ lowerBounds {x' | x ≤ x'}
⊢ x' ≤ x
Tactic:
exact h le_rfl
State after:
no goals

State before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x' ≤ x → x' ∈ lowerBounds {x' | x ≤ x'}
Tactic:
intro h x'' hx''
State after:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x' ≤ x
x'' : X
hx'' : x'' ∈ {x' | x ≤ x'}
⊢ x' ≤ x''

State before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x' ≤ x
x'' : X
hx'' : x'' ∈ {x' | x ≤ x'}
⊢ x' ≤ x''
Tactic:
exact h.trans hx''
State after:
no goals