rw [← h]
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ a ⊔ b = ⊤
case h.mpr
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b : Ideal S
h : a + b = ⊤
⊢ a ⊔ b = a + b