α : Type u_1
β : Type ?u.7502
γ : Type ?u.7505
G : Type u_2
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))
α : Type u_1
β : Type ?u.7502
γ : Type ?u.7505
G : Type u_2
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)
refine' fun y => (H _).unique _
α : Type u_1
β : Type ?u.7502
γ : Type ?u.7505
G : Type u_2
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))
α : Type u_1
β : Type ?u.7502
γ : Type ?u.7505
G : Type u_2
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))
have := (f₁ g).leftOrdContinuous (H y)
α : Type u_1
β : Type ?u.7502
γ : Type ?u.7505
G : Type u_2
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))
α : Type u_1
β : Type ?u.7502
γ : Type ?u.7505
G : Type u_2
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))
rw [← range_comp, ← (Equiv.mulRight g).surjective.range_comp _] at this