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

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
⊢ isInf S (⋂₀ S)
Tactic:
intro t
State after:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ lowerBounds S ↔ t ≤ ⋂₀ S

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ lowerBounds S ↔ t ≤ ⋂₀ S
Tactic:
constructor
State after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ lowerBounds S → t ≤ ⋂₀ S

case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ≤ ⋂₀ S → t ∈ lowerBounds S

State before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ∈ lowerBounds S → t ≤ ⋂₀ S
Tactic:
intro ht x hx u hu
State after:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ lowerBounds S
x : Y
hx : x ∈ t
u : Set Y
hu : u ∈ S
⊢ x ∈ u

State before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ lowerBounds S
x : Y
hx : x ∈ t
u : Set Y
hu : u ∈ S
⊢ x ∈ u
Tactic:
exact ht hu hx
State after:
no goals

State before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
⊢ t ≤ ⋂₀ S → t ∈ lowerBounds S
Tactic:
intro ht u hu x hx
State after:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ≤ ⋂₀ S
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ t
⊢ x ∈ u

State before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ≤ ⋂₀ S
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ t
⊢ x ∈ u
Tactic:
exact ht hx _ hu
State after:
no goals