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

State before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
⊢ isSup 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 ∈ upperBounds S ↔ ⋃₀ S ≤ t

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

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

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

State before:
case mp
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ upperBounds S
x : Y
hx : x ∈ ⋃₀ S
⊢ x ∈ t
Tactic:
rcases hx with ⟨s, hs, hx⟩
State after:
case mp.intro.intro
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ upperBounds S
x : Y
s : Set Y
hs : s ∈ S
hx : x ∈ s
⊢ x ∈ t

State before:
case mp.intro.intro
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : t ∈ upperBounds S
x : Y
s : Set Y
hs : s ∈ S
hx : x ∈ s
⊢ x ∈ t
Tactic:
exact ht hs 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
⊢ ⋃₀ S ≤ t → t ∈ upperBounds 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 : ⋃₀ S ≤ t
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ u
⊢ x ∈ t

State before:
case mpr
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : ⋃₀ S ≤ t
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ u
⊢ x ∈ t
Tactic:
apply ht
State after:
case mpr.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : ⋃₀ S ≤ t
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ u
⊢ x ∈ ⋃₀ S

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