simp
case h.mp.intro.intro.a
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b x y : Ideal S
hxy : x * a + y * b = 1
h2 : x * a + y * b ≤ a + b
⊢ 1 ∈ 1

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
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1
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
⊢ a + b = ⊤ → ∃ a_2 b_1, a_2 * a + b_1 * b = 1