α : Type u_2
β : Type u_1
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_2
β : Type u_1
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ b, b ∈ t ∧ inr b = inl a
α : Type u_2
β : Type u_1
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ inl a ∈ disjSum s t ↔ a ∈ s
rw [mem_disjSum, or_iff_left]
α : Type u_2
β : Type u_1
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ b, b ∈ t ∧ inr b = inl a
α : Type u_2
β : Type u_1
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_2
β : Type u_1
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ b, b ∈ t ∧ inr b = inl a
simp only [inl.injEq, exists_eq_right]
case intro.intro
α : Type u_2
β : Type u_1
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b✝ : β
x : α ⊕ β
b : β
left✝ : b ∈ t
hb : inr b = inl a
⊢ False
α : Type u_2
β : Type u_1
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b : β
x : α ⊕ β
⊢ ¬∃ b, b ∈ t ∧ inr b = inl a
rintro ⟨b, _, hb⟩
no goals
case intro.intro
α : Type u_2
β : Type u_1
s : Multiset α
t : Multiset β
s₁ s₂ : Multiset α
t₁ t₂ : Multiset β
a : α
b✝ : β
x : α ⊕ β
b : β
left✝ : b ∈ t
hb : inr b = inl a
⊢ False
exact inr_ne_inl hb