α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
haveI : DecidableEq α := Classical.decEq α
case mp
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ a ::ₘ as = b ::ₘ bs → a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs

case mpr
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ (a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs) → a ::ₘ as = b ::ₘ bs
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
constructor
case mp
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
case mp
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ a ::ₘ as = b ::ₘ bs → a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
intro eq
case pos
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : a = b
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs

case neg
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
case mp
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
by_cases h : a = b
case pos
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = a ::ₘ bs
⊢ a = a ∧ as = bs ∨ a ≠ a ∧ ∃ cs, as = a ::ₘ cs ∧ bs = a ::ₘ cs
case pos
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : a = b
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
subst h
no goals
case pos
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = a ::ₘ bs
⊢ a = a ∧ as = bs ∨ a ≠ a ∧ ∃ cs, as = a ::ₘ cs ∧ bs = a ::ₘ cs
simp_all
case neg
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this : a ∈ b ::ₘ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
case neg
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
have : a ∈ b ::ₘ bs := eq ▸ mem_cons_self _ _
case neg
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
case neg
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this : a ∈ b ::ₘ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
have : a ∈ bs := by simpa [h]
case neg.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
case neg
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
rcases exists_cons_of_mem this with ⟨cs, hcs⟩
case neg.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ as = b ::ₘ cs
case neg.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
simp [h, hcs]
case neg.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝² : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝¹ : a ∈ b ::ₘ bs
this✝ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ as = b ::ₘ cs
case neg.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ as = b ::ₘ cs
have : a ::ₘ as = b ::ₘ a ::ₘ cs := by simp [eq, hcs]
case neg.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝³ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝² : a ∈ b ::ₘ bs
this✝¹ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this✝ : a ::ₘ as = b ::ₘ a ::ₘ cs
this : a ::ₘ as = a ::ₘ b ::ₘ cs
⊢ as = b ::ₘ cs
case neg.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝² : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝¹ : a ∈ b ::ₘ bs
this✝ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ as = b ::ₘ cs
have : a ::ₘ as = a ::ₘ b ::ₘ cs := by rwa [cons_swap]
no goals
case neg.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝³ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝² : a ∈ b ::ₘ bs
this✝¹ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this✝ : a ::ₘ as = b ::ₘ a ::ₘ cs
this : a ::ₘ as = a ::ₘ b ::ₘ cs
⊢ as = b ::ₘ cs
simpa using this
no goals
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this : a ∈ b ::ₘ bs
⊢ a ∈ bs
simpa [h]
no goals
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ a ::ₘ cs
simp [eq, hcs]
no goals
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this✝² : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝¹ : a ∈ b ::ₘ bs
this✝ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ a ::ₘ as = a ::ₘ b ::ₘ cs
rwa [cons_swap]
case mpr
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
h : a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs
case mpr
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ (a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs) → a ::ₘ as = b ::ₘ bs
intro h
case mpr.inl.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
eq₁ : a = b
eq₂ : as = bs
⊢ a ::ₘ as = b ::ₘ bs

case mpr.inr.intro.intro.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
left✝ : a ≠ b
cs : Multiset α
eq₁ : as = b ::ₘ cs
eq₂ : bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs
case mpr
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
h : a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs
rcases h with (⟨eq₁, eq₂⟩ | ⟨_, cs, eq₁, eq₂⟩)
no goals
case mpr.inl.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
eq₁ : a = b
eq₂ : as = bs
⊢ a ::ₘ as = b ::ₘ bs
simp [*]
no goals
case mpr.inr.intro.intro.intro
α : Type u_1
β : Type ?u.21180
γ : Type ?u.21183
a b : α
as bs : Multiset α
this : DecidableEq α
left✝ : a ≠ b
cs : Multiset α
eq₁ : as = b ::ₘ cs
eq₂ : bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs
simp [*, cons_swap a b]