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

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Inf {x, x'} = x
Tactic:
constructor
State after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' → Inf {x, x'} = x

case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ Inf {x, x'} = x → x ≤ x'

State before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' → Inf {x, x'} = x
Tactic:
intro h
State after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
⊢ Inf {x, x'} = x

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

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

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

case mp.mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
⊢ z ≤ x → z ∈ lowerBounds {x, x'}

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

State before:
case mp.mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
hz : z ∈ lowerBounds {x, x'}
⊢ z ≤ x
Tactic:
apply hz
State after:
case mp.mp.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
hz : z ∈ lowerBounds {x, x'}
⊢ x ∈ {x, x'}

State before:
case mp.mp.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
hz : z ∈ lowerBounds {x, x'}
⊢ x ∈ {x, x'}
Tactic:
simp
State after:
no goals

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

State before:
case mp.mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : x ≤ x'
z : X
hz : z ≤ x
⊢ z ∈ lowerBounds {x, x'}
Tactic:
simp [hz, hz.trans h]
State after:
no goals

State before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ Inf {x, x'} = x → x ≤ x'
Tactic:
intro h
State after:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ x ≤ x'

State before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ x ≤ x'
Tactic:
rw [← h]
State after:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ Inf {x, x'} ≤ x'

State before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ Inf {x, x'} ≤ x'
Tactic:
apply lowerBound_Inf
State after:
case mpr.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ x' ∈ {x, x'}

State before:
case mpr.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
h : Inf {x, x'} = x
⊢ x' ∈ {x, x'}
Tactic:
simp
State after:
no goals