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

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ≤ Inf s
Tactic:
apply (CompleteLattice.I_isInf s _).1
State after:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ∈ lowerBounds s

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ∈ lowerBounds s
Tactic:
apply lowerBounds_mono_set h
State after:
case a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ∈ lowerBounds t

State before:
case a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ∈ lowerBounds t
Tactic:
exact lowerBound_Inf t
State after:
no goals