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

State before:
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
⊢ adjunction (l' ∘ l) (r ∘ r')
Tactic:
intro x z
State after:
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
x : X
z : Z
⊢ (l' ∘ l) x ≤ z ↔ x ≤ (r ∘ r') z

State before:
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
x : X
z : Z
⊢ (l' ∘ l) x ≤ z ↔ x ≤ (r ∘ r') z
Tactic:
rw [Function.comp_apply, h', h]
State after:
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
x : X
z : Z
⊢ x ≤ r (r' z) ↔ x ≤ (r ∘ r') z

State before:
X : Type
inst✝⁵ : PartialOrder X
inst✝⁴ : CompleteLattice X
Y : Type
inst✝³ : PartialOrder Y
inst✝² : CompleteLattice Y
Z : Type
inst✝¹ : PartialOrder Z
inst✝ : CompleteLattice Z
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
x : X
z : Z
⊢ x ≤ r (r' z) ↔ x ≤ (r ∘ r') z
Tactic:
rfl
State after:
no goals