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