[GOAL]
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s₁ s₂ : Multiset α
⊢ sup (s₁ + s₂) = fold (fun x x_1 => x ⊔ x_1) (⊥ ⊔ ⊥) (s₁ + s₂)
[PROOFSTEP]
simp [sup]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ sup 0 ≤ a ↔ ∀ (b : α), b ∈ 0 → b ≤ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (sup s ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a) → (sup (a_1 ::ₘ s) ≤ a ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → b ≤ a)
[PROOFSTEP]
simp (config := { contextual := true }) [or_imp, forall_and]
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ sup (ndunion s₁ s₂) = sup s₁ ⊔ sup s₂
[PROOFSTEP]
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ ndunion s₁ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ sup (s₁ ∪ s₂) = sup s₁ ⊔ sup s₂
[PROOFSTEP]
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ sup (ndinsert a s) = a ⊔ sup s
[PROOFSTEP]
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_cons]
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
m : Multiset (Multiset α)
⊢ Nodup (sup m) ↔ ∀ (a : Multiset α), a ∈ m → Nodup a
[PROOFSTEP]
induction' m using Multiset.induction_on with _ _ h
[GOAL]
case empty
α✝ : Type u_1
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
⊢ Nodup (sup 0) ↔ ∀ (a : Multiset α), a ∈ 0 → Nodup a
[PROOFSTEP]
simp
[GOAL]
case cons
α✝ : Type u_1
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
a✝ : Multiset α
s✝ : Multiset (Multiset α)
h : Nodup (sup s✝) ↔ ∀ (a : Multiset α), a ∈ s✝ → Nodup a
⊢ Nodup (sup (a✝ ::ₘ s✝)) ↔ ∀ (a : Multiset α), a ∈ a✝ ::ₘ s✝ → Nodup a
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s₁ s₂ : Multiset α
⊢ inf (s₁ + s₂) = fold (fun x x_1 => x ⊓ x_1) (⊤ ⊓ ⊤) (s₁ + s₂)
[PROOFSTEP]
simp [inf]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s : Multiset α
a : α
⊢ a ≤ inf 0 ↔ ∀ (b : α), b ∈ 0 → a ≤ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s : Multiset α
a : α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (a ≤ inf s ↔ ∀ (b : α), b ∈ s → a ≤ b) → (a ≤ inf (a_1 ::ₘ s) ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → a ≤ b)
[PROOFSTEP]
simp (config := { contextual := true }) [or_imp, forall_and]
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ inf (ndunion s₁ s₂) = inf s₁ ⊓ inf s₂
[PROOFSTEP]
rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_add]
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ ndunion s₁ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ inf (s₁ ∪ s₂) = inf s₁ ⊓ inf s₂
[PROOFSTEP]
rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_add]
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ inf (ndinsert a s) = a ⊓ inf s
[PROOFSTEP]
rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_cons]
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
[PROOFSTEP]
simp
