no goals
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ⊔ b = b * (a / b) ⊔ b * 1
rw [mul_one b, div_eq_mul_inv, mul_comm a, mul_inv_cancel_left]
no goals
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ b * (a / b) ⊔ b * 1 = b * (a / b ⊔ 1)
rw [← mul_sup (a / b) 1 b]