Theorem: Tutorial.left_comm_of_right_comm (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✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
⊢ lWZ ∘ lZX = lWY ∘ lYX
Tactic:
have A₁ := hXZ.compose hZW
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✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
A₁ : adjunction (lWZ ∘ lZX) (uXZ ∘ uZW)
⊢ lWZ ∘ lZX = lWY ∘ lYX

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✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
A₁ : adjunction (lWZ ∘ lZX) (uXZ ∘ uZW)
⊢ lWZ ∘ lZX = lWY ∘ lYX
Tactic:
rw [h] at A₁
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✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
A₁ : adjunction (lWZ ∘ lZX) (uXY ∘ uYW)
⊢ lWZ ∘ lZX = lWY ∘ lYX

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✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
A₁ : adjunction (lWZ ∘ lZX) (uXY ∘ uYW)
⊢ lWZ ∘ lZX = lWY ∘ lYX
Tactic:
exact unique_left A₁ (hXY.compose hWY)
State after:
no goals