case zero
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s : Multiset α
t : Multiset β
⊢ ∀ {a : α}, a ∈ 0 → ∃ b, b ∈ 0 ∧ r a b

case cons
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
⊢ ∀ {a : α}, a ∈ x ::ₘ s → ∃ b, b ∈ y ::ₘ t ∧ r a b
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
induction' h with x y s t hxy _hst ih
no goals
case zero
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s : Multiset α
t : Multiset β
⊢ ∀ {a : α}, a ∈ 0 → ∃ b, b ∈ 0 ∧ r a b
simp
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha : a ∈ x ::ₘ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
⊢ ∀ {a : α}, a ∈ x ::ₘ s → ∃ b, b ∈ y ::ₘ t ∧ r a b
intro a ha
case cons.inl
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a = x
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b

case cons.inr
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha : a ∈ x ::ₘ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
cases' mem_cons.1 ha with ha ha
no goals
case cons.inl
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a = x
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩
case cons.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
b : β
hbt : b ∈ t
hab : r a b
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
case cons.inr
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
rcases ih ha with ⟨b, hbt, hab⟩
no goals
case cons.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.468460
δ : Type ?u.468463
r✝ : α → β → Prop
p : γ → δ → Prop
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
_hst : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
b : β
hbt : b ∈ t
hab : r a b
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
exact ⟨b, mem_cons.2 (Or.inr hbt), hab⟩