case empty
α✝ : Type ?u.22553
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : DecidableEq α
⊢ Nodup (sup 0) ↔ ∀ (a : Multiset α), a ∈ 0 → Nodup a

case cons
α✝ : Type ?u.22553
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
inst✝¹ : DecidableEq α✝
α : Type u_1
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
α✝ : Type ?u.22553
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : DecidableEq α
m : Multiset (Multiset α)
⊢ Nodup (sup m) ↔ ∀ (a : Multiset α), a ∈ m → Nodup a
induction' m using Multiset.induction_on with _ _ h
no goals
case empty
α✝ : Type ?u.22553
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : DecidableEq α
⊢ Nodup (sup 0) ↔ ∀ (a : Multiset α), a ∈ 0 → Nodup a
simp
no goals
case cons
α✝ : Type ?u.22553
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
inst✝¹ : DecidableEq α✝
α : Type u_1
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
simp [h]