[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : β ≃o γ
y : γ
⊢ IsLUB {x | (↑e ∘ f) x ≤ y} ((g ∘ ↑(OrderIso.symm e)) y)
[PROOFSTEP]
simpa [e.le_symm_apply] using h (e.symm y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
⊢ IsOrderRightAdjoint (f ∘ ↑e) (↑(OrderIso.symm e) ∘ g)
[PROOFSTEP]
intro y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x | (f ∘ ↑e) x ≤ y} ((↑(OrderIso.symm e) ∘ g) y)
[PROOFSTEP]
change IsLUB (e ⁻¹' {x | f x ≤ y}) (e.symm (g y))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB (↑e ⁻¹' {x | f x ≤ y}) (↑(OrderIso.symm e) (g y))
[PROOFSTEP]
rw [e.isLUB_preimage, e.apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x | f x ≤ y} (g y)
[PROOFSTEP]
exact h y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ↑fa ↑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
⊢ Semiconj g' ↑fb ↑fa
[PROOFSTEP]
refine' fun y => (hg' _).unique _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ↑fa ↑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB {x | g x ≤ ↑fb y} (↑fa (g' y))
[PROOFSTEP]
rw [← fa.surjective.image_preimage {x | g x ≤ fb y}, preimage_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g ↑fa ↑fb
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB (↑fa '' {a | g (↑fa a) ≤ ↑fb y}) (↑fa (g' y))
[PROOFSTEP]
simp only [h.eq, fb.le_iff_le, fa.leftOrdContinuous (hg' _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') x)) (h x)
g : G
⊢ Semiconj h ↑(↑f₂ g) ↑(↑f₁ g)
[PROOFSTEP]
refine' fun y => (H _).unique _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') x)) (h x)
g : G
y : α
⊢ IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') (↑(↑f₂ g) y))) (↑(↑f₁ g) (h y))
[PROOFSTEP]
have := (f₁ g).leftOrdContinuous (H y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') x)) (h x)
g : G
y : α
this : IsLUB (↑(↑f₁ g) '' range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') y)) (↑(↑f₁ g) (h y))
⊢ IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') (↑(↑f₂ g) y))) (↑(↑f₁ g) (h y))
[PROOFSTEP]
rw [← range_comp, ← (Equiv.mulRight g).surjective.range_comp _] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
G : Type u_4
inst✝¹ : PartialOrder α
inst✝ : Group G
f₁ f₂ : G →* α ≃o α
h : α → α
H : ∀ (x : α), IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') x)) (h x)
g : G
y : α
this : IsLUB (range ((↑(↑f₁ g) ∘ fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') y)) ∘ ↑(Equiv.mulRight g))) (↑(↑f₁ g) (h y))
⊢ IsLUB (range fun g' => ↑(↑f₁ g')⁻¹ (↑(↑f₂ g') (↑(↑f₂ g) y))) (↑(↑f₁ g) (h y))
[PROOFSTEP]
simpa [(· ∘ ·)] using this
