no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
b : FactorSet α
⊢ ⊤ ⊔ b + ⊤ ⊓ b = ⊤ + b
simp
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a : FactorSet α
⊢ a ⊔ ⊤ + a ⊓ ⊤ = a + ⊤
simp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a b : Multiset { a // Irreducible a }
⊢ a ⊔ b + a ⊓ b = a + b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a b : Multiset { a // Irreducible a }
⊢ ↑a ⊔ ↑b + ↑a ⊓ ↑b = ↑a + ↑b
rw [← WithTop.coe_sup, ← WithTop.coe_inf, ← WithTop.coe_add, ← WithTop.coe_add,
  WithTop.coe_eq_coe]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a b : Multiset { a // Irreducible a }
⊢ a ⊔ b + a ⊓ b = a + b
exact Multiset.union_add_inter _ _