case mp
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ (∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs ↔ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
constructor
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
⊢ Rel r m bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
generalize hm : a ::ₘ as = m
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
h : Rel r m bs
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
⊢ Rel r m bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
intro h
case mp.zero
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs : Multiset β
m as : Multiset α
hm : a ::ₘ as = 0
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ 0 = b ::ₘ bs'

case mp.cons
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs : Multiset β
m : Multiset α
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : ∀ {as : Multiset α}, a ::ₘ as = as✝ → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs✝ = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a✝² ::ₘ as✝
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ b✝ ::ₘ bs✝ = b ::ₘ bs'
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
h : Rel r m bs
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
induction h generalizing as
case mp.cons
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs : Multiset β
m : Multiset α
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : ∀ {as : Multiset α}, a ::ₘ as = as✝ → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs✝ = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a✝² ::ₘ as✝
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ b✝ ::ₘ bs✝ = b ::ₘ bs'
case mp.zero
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs : Multiset β
m as : Multiset α
hm : a ::ₘ as = 0
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ 0 = b ::ₘ bs'

case mp.cons
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs : Multiset β
m : Multiset α
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : ∀ {as : Multiset α}, a ::ₘ as = as✝ → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs✝ = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a✝² ::ₘ as✝
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ b✝ ::ₘ bs✝ = b ::ₘ bs'
case zero => simp at hm
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs : Multiset β
m as : Multiset α
hm : a ::ₘ as = 0
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ 0 = b ::ₘ bs'
simp at hm
case inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
eq₁ : a = a'
eq₂ : as = as'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

case inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
rcases cons_eq_cons.1 hm with (⟨eq₁, eq₂⟩ | ⟨_h, cs, eq₁, eq₂⟩)
case inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
b : β
as' : Multiset α
bs : Multiset β
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
eq₂ : as = as'
ha'b : r a b
hm : a ::ₘ as = a ::ₘ as'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
case inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
eq₁ : a = a'
eq₂ : as = as'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
subst eq₁
case inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
b : β
bs : Multiset β
as : Multiset α
ha'b : r a b
h : Rel r as bs
ih : ∀ {as_1 : Multiset α}, a ::ₘ as_1 = as → ∃ b bs', r a b ∧ Rel r as_1 bs' ∧ bs = b ::ₘ bs'
hm : a ::ₘ as = a ::ₘ as
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
case inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
b : β
as' : Multiset α
bs : Multiset β
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
eq₂ : as = as'
ha'b : r a b
hm : a ::ₘ as = a ::ₘ as'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
subst eq₂
no goals
case inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
b : β
bs : Multiset β
as : Multiset α
ha'b : r a b
h : Rel r as bs
ih : ∀ {as_1 : Multiset α}, a ::ₘ as_1 = as → ∃ b bs', r a b ∧ Rel r as_1 bs' ∧ bs = b ::ₘ bs'
hm : a ::ₘ as = a ::ₘ as
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
exact ⟨b, bs, ha'b, h, rfl⟩
case inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
b' : β
bs' : Multiset β
h₁ : r a b'
h₂ : Rel r cs bs'
eq : bs = b' ::ₘ bs'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
case inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
no goals
case inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
b' : β
bs' : Multiset β
h₁ : r a b'
h₂ : Rel r cs bs'
eq : bs = b' ::ₘ bs'
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩
no goals
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.444789
δ : Type ?u.444792
r : α → β → Prop
p : γ → δ → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ (∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs
exact fun ⟨b, bs', hab, h, Eq⟩ => Eq.symm ▸ Rel.cons hab h