α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) → ↑card m1 = ↑card m2 → Rel r m1 m2
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m1 m2 : Multiset α
r : α → α → Prop
h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b
hc : ↑card m1 = ↑card m2
⊢ Rel r m1 m2
revert m1
case refine'_1
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ 0 → r a b) → ↑card m1 = ↑card 0 → Rel r m1 0

case refine'_2
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ s → r a b) → ↑card m1 = ↑card s → Rel r m1 s) →
      ∀ {m1 : Multiset α},
        (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ s → r a_2 b) → ↑card m1 = ↑card (a ::ₘ s) → Rel r m1 (a ::ₘ s)
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) → ↑card m1 = ↑card m2 → Rel r m1 m2
refine' @(m2.induction_on _ _)
case refine'_1
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → b ∈ 0 → r a b
hc : ↑card m = ↑card 0
⊢ Rel r m 0
case refine'_1
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ 0 → r a b) → ↑card m1 = ↑card 0 → Rel r m1 0
intro m _h hc
no goals
case refine'_1
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → b ∈ 0 → r a b
hc : ↑card m = ↑card 0
⊢ Rel r m 0
rw [rel_zero_right, ← card_eq_zero, hc, card_zero]
case refine'_2
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : ↑card m = ↑card (a ::ₘ t)
⊢ Rel r m (a ::ₘ t)
case refine'_2
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ s → r a b) → ↑card m1 = ↑card s → Rel r m1 s) →
      ∀ {m1 : Multiset α},
        (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ s → r a_2 b) → ↑card m1 = ↑card (a ::ₘ s) → Rel r m1 (a ::ₘ s)
intro a t ih m h hc
case refine'_2
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : ↑card m = ↑card t + 1
⊢ Rel r m (a ::ₘ t)
case refine'_2
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : ↑card m = ↑card (a ::ₘ t)
⊢ Rel r m (a ::ₘ t)
rw [card_cons] at hc
case refine'_2.intro
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : ↑card m = ↑card t + 1
b : α
hb : b ∈ m
⊢ Rel r m (a ::ₘ t)
case refine'_2
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : ↑card m = ↑card t + 1
⊢ Rel r m (a ::ₘ t)
obtain ⟨b, hb⟩ := card_pos_iff_exists_mem.1 (show 0 < card m from hc.symm ▸ Nat.succ_pos _)
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : ↑card (b ::ₘ m') = ↑card t + 1
hb : b ∈ b ::ₘ m'
⊢ Rel r (b ::ₘ m') (a ::ₘ t)
case refine'_2.intro
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : ↑card m = ↑card t + 1
b : α
hb : b ∈ m
⊢ Rel r m (a ::ₘ t)
obtain ⟨m', rfl⟩ := exists_cons_of_mem hb
case refine'_2.intro.intro.refine'_1
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : ↑card (b ::ₘ m') = ↑card t + 1
hb : b ∈ b ::ₘ m'
⊢ ∀ (a b : α), a ∈ m' → b ∈ t → r a b

case refine'_2.intro.intro.refine'_2
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : ↑card (b ::ₘ m') = ↑card t + 1
hb : b ∈ b ::ₘ m'
⊢ ↑card m' = ↑card t
case refine'_2.intro.intro
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : ↑card (b ::ₘ m') = ↑card t + 1
hb : b ∈ b ::ₘ m'
⊢ Rel r (b ::ₘ m') (a ::ₘ t)
refine' rel_cons_right.mpr ⟨b, m', h _ _ hb (mem_cons_self _ _), ih _ _, rfl⟩
no goals
case refine'_2.intro.intro.refine'_1
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : ↑card (b ::ₘ m') = ↑card t + 1
hb : b ∈ b ::ₘ m'
⊢ ∀ (a b : α), a ∈ m' → b ∈ t → r a b
exact fun _ _ ha hb => h _ _ (mem_cons_of_mem ha) (mem_cons_of_mem hb)
no goals
case refine'_2.intro.intro.refine'_2
α : Type u_1
β : Type ?u.470703
γ : Type ?u.470706
δ : Type ?u.470709
r✝ : α → β → Prop
p : γ → δ → Prop
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → ↑card m1 = ↑card t → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : ↑card (b ::ₘ m') = ↑card t + 1
hb : b ∈ b ::ₘ m'
⊢ ↑card m' = ↑card t
simpa using hc