[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ ↑card (disjSum s t) = ↑card s + ↑card t
[PROOFSTEP]
rw [disjSum, card_add, card_map, card_map]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ x ∈ disjSum s t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x
[PROOFSTEP]
simp_rw [disjSum, mem_add, mem_map]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ inl a ∈ disjSum s t ↔ a ∈ s
[PROOFSTEP]
rw [mem_disjSum, or_iff_left]
  -- Porting note: Previous code for L62 was: simp only [exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ (∃ a_1, a_1 ∈ s ∧ inl a_1 = inl a) ↔ a ∈ s
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ b, b ∈ t ∧ inr b = inl a
[PROOFSTEP]
simp only [inl.injEq, exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ b, b ∈ t ∧ inr b = inl a
[PROOFSTEP]
rintro ⟨b, _, hb⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b✝ : β
x : α ⊕ β
b : β
left✝ : b ∈ t
hb : inr b = inl a
⊢ False
[PROOFSTEP]
exact inr_ne_inl hb
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ inr b ∈ disjSum s t ↔ b ∈ t
[PROOFSTEP]
rw [mem_disjSum, or_iff_right]
  -- Porting note: Previous code for L72 was: simp only [exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ (∃ b_1, b_1 ∈ t ∧ inr b_1 = inr b) ↔ b ∈ t
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ a, a ∈ s ∧ inl a = inr b
[PROOFSTEP]
simp only [inr.injEq, exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ a, a ∈ s ∧ inl a = inr b
[PROOFSTEP]
rintro ⟨a, _, ha⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a✝ : α
b : β
x : α ⊕ β
a : α
left✝ : a ∈ s
ha : inl a = inr b
⊢ False
[PROOFSTEP]
exact inl_ne_inr ha
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
hs : Nodup s
ht : Nodup t
⊢ Nodup (disjSum s t)
[PROOFSTEP]
refine' ((hs.map inl_injective).add_iff <| ht.map inr_injective).2 fun x hs ht => _
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x✝ : α ⊕ β
hs✝ : Nodup s
ht✝ : Nodup t
x : α ⊕ β
hs : x ∈ Multiset.map inl s
ht : x ∈ Multiset.map inr t
⊢ False
[PROOFSTEP]
rw [Multiset.mem_map] at hs ht 
[GOAL]
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x✝ : α ⊕ β
hs✝ : Nodup s
ht✝ : Nodup t
x : α ⊕ β
hs : ∃ a, a ∈ s ∧ inl a = x
ht : ∃ a, a ∈ t ∧ inr a = x
⊢ False
[PROOFSTEP]
obtain ⟨a, _, rfl⟩ := hs
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a✝ : α
b : β
x : α ⊕ β
hs : Nodup s
ht✝ : Nodup t
a : α
left✝ : a ∈ s
ht : ∃ a_1, a_1 ∈ t ∧ inr a_1 = inl a
⊢ False
[PROOFSTEP]
obtain ⟨b, _, h⟩ := ht
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a✝ : α
b✝ : β
x : α ⊕ β
hs : Nodup s
ht : Nodup t
a : α
left✝¹ : a ∈ s
b : β
left✝ : b ∈ t
h : inr b = inl a
⊢ False
[PROOFSTEP]
exact inr_ne_inl h
