ι : Type ?u.10983
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.10994
r : α → α → Prop
inst✝ : PartialOrder α
f : α → α → α
comm : Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f b a)
ι : Type ?u.10983
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.10994
r : α → α → Prop
inst✝ : PartialOrder α
f : α → α → α
comm : Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f a (f b c) ≤ f (f a b) c
rw [comm, comm b, comm _ c, comm a]
no goals
ι : Type ?u.10983
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.10994
r : α → α → Prop
inst✝ : PartialOrder α
f : α → α → α
comm : Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f b a)
exact assoc _ _ _