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

State before:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
⊢ adjunction l (mk_right l)
Tactic:
intro x y
State after:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
⊢ l x ≤ y ↔ x ≤ mk_right l y

State before:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
⊢ l x ≤ y ↔ x ≤ mk_right l y
Tactic:
constructor
State after:
case mp
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
⊢ l x ≤ y → x ≤ mk_right l y

case mpr
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
⊢ x ≤ mk_right l y → l x ≤ y

State before:
case mp
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
⊢ l x ≤ y → x ≤ mk_right l y
Tactic:
intro h'
State after:
case mp
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : l x ≤ y
⊢ x ≤ mk_right l y

State before:
case mp
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : l x ≤ y
⊢ x ≤ mk_right l y
Tactic:
exact (CompleteLattice.S_isSup {x | l x ≤ y}).upperBound h'
State after:
no goals

State before:
case mpr
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
⊢ x ≤ mk_right l y → l x ≤ y
Tactic:
intro h'
State after:
case mpr
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
⊢ l x ≤ y

State before:
case mpr
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
⊢ l x ≤ y
Tactic:
have l_mono : Monotone l := by {
  intro a b hab
  have := h {a, b}
  rw [Sup_pair.1 hab, Set.image_pair] at this
  exact Sup_pair.2 this.symm
}
State after:
case mpr
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
l_mono : Monotone l
⊢ l x ≤ y

State before:
case mpr
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
l_mono : Monotone l
⊢ l x ≤ y
Tactic:
calc
  l x ≤ l (mk_right l y) := l_mono h'
  _   = Sup (l '' { x | l x ≤ y }) := h {x | l x ≤ y}
  _   ≤ Sup { y' | y' ≤ y } := Sup_subset (Set.image_preimage_subset l { y' | y' ≤ y })
  _   = y := Sup_le_self y
State after:
no goals

State before:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
⊢ Monotone l
Tactic:
intro a b hab
State after:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
⊢ l a ≤ l b

State before:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
⊢ l a ≤ l b
Tactic:
have := h {a, b}
State after:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
this : l (Sup {a, b}) = Sup (l '' {a, b})
⊢ l a ≤ l b

State before:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
this : l (Sup {a, b}) = Sup (l '' {a, b})
⊢ l a ≤ l b
Tactic:
rw [Sup_pair.1 hab, Set.image_pair] at this
State after:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
this : l b = Sup {l a, l b}
⊢ l a ≤ l b

State before:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
x : X
y : Y
h' : x ≤ mk_right l y
a b : X
hab : a ≤ b
this : l b = Sup {l a, l b}
⊢ l a ≤ l b
Tactic:
exact Sup_pair.2 this.symm
State after:
no goals