no goals
α : Type u_1
inst✝³ : ConditionallyCompleteLattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
s t : Set α
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
ht₀ : Set.Nonempty t
ht₁ : BddBelow t
⊢ sSup (s / t) = sSup s / sInf t
rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]