Theorem: Ideal.le_add (FltRegular/NumberTheory/Cyclotomic/CyclRat.lean)

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ a + c ≤ b + d
Tactic:
simp at *
State after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ a ≤ b ⊔ d ∧ c ≤ b ⊔ d

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ a ≤ b ⊔ d ∧ c ≤ b ⊔ d
Tactic:
constructor
State after:
case left
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ a ≤ b ⊔ d

case right
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ c ≤ b ⊔ d

State before:
case left
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ a ≤ b ⊔ d

case right
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ c ≤ b ⊔ d
Tactic:
apply le_trans hab (@le_sup_left _ _ _ _)
State after:
case right
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ c ≤ b ⊔ d

State before:
case right
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
S : Type u_1
inst✝ : CommRing S
a b c d : Ideal S
hab : a ≤ b
hcd : c ≤ d
⊢ c ≤ b ⊔ d
Tactic:
apply le_trans hcd (@le_sup_right _ _ _ _)
State after:
no goals