α : 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
α : 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)
refine' ((hs.map inl_injective).add_iff <| ht.map inr_injective).2 fun x hs ht => _
α : 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
α : 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
rw [Multiset.mem_map] at hs ht
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
α : 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
obtain ⟨a, _, rfl⟩ := hs
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
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
obtain ⟨b, _, h⟩ := ht
no goals
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
exact inr_ne_inl h