awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ s.card = 4 ↔ ∃ (x : α), ∃ (y : α), ∃ (z : α), ∃ (w : α), s = {x, y, z, w}

Tactic:
⟨Quot.inductionOn s fun _l h =>
      (List.length_eq_four.mp h).imp fun _a =>
        Exists.imp fun _b => Exists.imp fun _c => Exists.imp fun _d => congr_arg _,
    fun ⟨_a, _b, _c, _d, e⟩ => e.symm ▸ rfl⟩

Premises used: Quot.inductionOn, Eq.rec, _private.0.Multiset.card_eq_four.match_1, Iff.intro, Multiset.card, OfNat.ofNat, Eq.symm, Eq, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
n : ℕ
⊢ (∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = s ∧ t.card = n) → s.card = n + 1

Tactic:
aesop
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
n : ℕ
refine : s.card = n + 1 → ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = s ∧ t.card = n
⊢ s.card = n + 1 ↔ ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = s ∧ t.card = n

Tactic:
refine ⟨?_, by aesop⟩
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
n : ℕ
⊢ card.{u_1} (α := α) 0 = n + 1 → ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = 0 ∧ t.card = n

Tactic:
aesop
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
s : Multiset α
h : ∀ {n : ℕ}, s.card = n + 1 → ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = s ∧ t.card = n
n : ℕ
⊢ (a ::ₘ s).card = n + 1 → ∃ (a_2 : α), ∃ (t : Multiset α), a_2 ::ₘ t = a ::ₘ s ∧ t.card = n

Tactic:
aesop
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
n : ℕ
empty : ∀ {n : ℕ}, card.{u_1} (α := α) 0 = n + 1 → ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = 0 ∧ t.card = n
cons :
  ∀ (a : α) (s : Multiset α),
    (∀ {n : ℕ}, s.card = n + 1 → ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = s ∧ t.card = n) →
      ∀ {n : ℕ}, (a ::ₘ s).card = n + 1 → ∃ (a_3 : α), ∃ (t : Multiset α), a_3 ::ₘ t = a ::ₘ s ∧ t.card = n
⊢ s.card = n + 1 → ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = s ∧ t.card = n

Tactic:
induction s using Multiset.induction generalizing n with aesop
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → p a
⊢ pmap (p := p) f 0 h = 0

Tactic:
rfl

Premises used: Multiset.zero, List.pmap, Multiset.ofList, Multiset.pmap, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
m : Multiset α
⊢ ∀ (h : ∀ (b : α), b ∈ a ::ₘ m → p b), pmap (p := p) f (a ::ₘ m) h = f a ⋯ ::ₘ pmap (p := p) f m ⋯

Tactic:
Quotient.inductionOn m fun _l _h => rfl

Premises used: Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Multiset { x : α // Membership.mem (γ := Multiset α) 0 x }) (attach 0) 0

Tactic:
rfl

Premises used: Multiset.zero, List.pmap, Multiset.ofList, Multiset.pmap, Multiset.attach, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ Rel (flip r) t s

Tactic:
Rel.recOn h Rel.zero fun h₀ _h₁ ih => Rel.cons h₀ ih

Premises used: Multiset.Rel.recOn
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset β
t : Multiset α
⊢ Rel (flip r) s t ↔ Rel r t s

Tactic:
⟨rel_flip_aux, rel_flip_aux⟩

Premises used: _private.0.Multiset.rel_flip_aux, Iff.intro
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ m → r x x) → Rel r m m

Tactic:
m.induction_on ?_ ?_

Premises used: Multiset.induction_on
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
m : Multiset α
r : α → α → Prop
refine_1 : (∀ (x : α), Membership.mem (γ := Multiset α) 0 x → r x x) → Rel r 0 0
refine_2 :
  ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)
⊢ (∀ (x : α), x ∈ m → r x x) → Rel r m m

Tactic:
refine m.induction_on ?_ ?_
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
m : Multiset α
r : α → α → Prop
h : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → r x x
⊢ Rel r 0 0

Tactic:
apply Rel.zero

Premises used: Multiset.Rel.zero
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
m_1 : Multiset α
r : α → α → Prop
a : α
m : Multiset α
ih : (∀ (x : α), x ∈ m → r x x) → Rel r m m
h : ∀ (x : α), x ∈ a ::ₘ m → r x x
⊢ Rel r (a ::ₘ m) (a ::ₘ m)

Tactic:
Rel.cons (h _ (mem_cons_self _ _)) (ih fun _ ha => h _ (mem_cons_of_mem ha))

Premises used: Multiset.mem_cons_of_mem, Multiset.Rel.cons, Multiset.mem_cons_self
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
m_1 : Multiset α
r : α → α → Prop
a : α
m : Multiset α
ih : (∀ (x : α), x ∈ m → r x x) → Rel r m m
h : ∀ (x : α), x ∈ a ::ₘ m → r x x
⊢ Rel r (a ::ₘ m) (a ::ₘ m)

Tactic:
exact Rel.cons (h _ (mem_cons_self _ _)) (ih fun _ ha => h _ (mem_cons_of_mem ha))

Premises used: Multiset.mem_cons_of_mem, Multiset.Rel.cons, Multiset.mem_cons_self
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ Rel (fun (x1 x2 : α) ↦ x1 = x2) s s

Tactic:
rel_refl_of_refl_on fun _x _hx => rfl

Premises used: Multiset.rel_refl_of_refl_on, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
mp : Rel (fun (x1 x2 : α) ↦ x1 = x2) s t → s = t
mpr : s = t → Rel (fun (x1 x2 : α) ↦ x1 = x2) s t
⊢ Rel (fun (x1 x2 : α) ↦ x1 = x2) s t ↔ s = t

Tactic:
constructor
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
h : Rel (fun (x1 x2 : α) ↦ x1 = x2) s t
mp : Eq.{u_1 + 1} (α := Multiset α) 0 0
mp₁ : ∀ {a b : α} {as bs : Multiset α}, a = b → Rel (fun (x1 x2 : α) ↦ x1 = x2) as bs → as = bs → a ::ₘ as = b ::ₘ bs
⊢ s = t

Tactic:
induction h
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
⊢ Eq.{u_1 + 1} (α := Multiset α) 0 0

Tactic:
simp [*]
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
a b : α
as bs : Multiset α
h : a = b
h_1 : Rel (fun (x1 x2 : α) ↦ x1 = x2) as bs
a_ih : as = bs
⊢ a ::ₘ as = b ::ₘ bs

Tactic:
simp [*]
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ Rel (fun (x1 x2 : α) ↦ x1 = x2) s s

Tactic:
rel_eq_refl

Premises used: Multiset.rel_eq_refl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
⊢ Rel (fun (x1 x2 : α) ↦ x1 = x2) s s

Tactic:
exact rel_eq_refl

Premises used: Multiset.rel_eq_refl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r p : α → β → Prop
s : Multiset α
t : Multiset β
h : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → ∀ (b : β), Membership.mem (γ := Multiset β) 0 b → r a b → p a b
⊢ Rel p 0 0

Tactic:
Rel.zero

Premises used: Multiset.Rel.zero
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r p : α → β → Prop
s : Multiset α
t : Multiset β
h : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → ∀ (b : β), Membership.mem (γ := Multiset β) 0 b → r a b → p a b
⊢ Rel p 0 0

Tactic:
exact Rel.zero

Premises used: Multiset.Rel.zero
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r p : α → β → Prop
s_1 : Multiset α
t_1 : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : ∀ (h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b), Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
cons : Rel p s t
⊢ Rel p (a ::ₘ s) (b ::ₘ t)

Tactic:
apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)

Premises used: Multiset.Rel.cons, Multiset.mem_cons_self
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r p : α → β → Prop
s_1 : Multiset α
t_1 : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : ∀ (h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b), Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p s t

Tactic:
ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'

Premises used: Multiset.mem_cons_of_mem
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r p : α → β → Prop
s_1 : Multiset α
t_1 : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : ∀ (h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b), Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p s t

Tactic:
exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'

Premises used: Multiset.mem_cons_of_mem
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r p : α → β → Prop
s : Multiset α
t : Multiset β
hst : Rel r s t
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b
zero :
  ∀
    (h :
      ∀ (a : α),
        Membership.mem (γ := Multiset α) 0 a → ∀ (b : β), Membership.mem (γ := Multiset β) 0 b → r a b → p a b),
    Rel p 0 0
cons :
  ∀ {a : α} {b : β} {s : Multiset α} {t : Multiset β} (hab : r a b) (_hst : Rel r s t)
    (ih : ∀ (h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b), Rel p s t)
    (h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1), Rel p (a ::ₘ s) (b ::ₘ t)
⊢ Rel p s t

Tactic:
induction hst with
  | zero => exact Rel.zero
  | @cons a b s t hab _hst ih =>
    apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
    exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'

Premises used: Multiset.Rel.zero, Multiset.Rel.cons
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s t : Multiset α
rw : Rel (fun (x1 x2 : α) ↦ x1 = x2) t s ↔ s = t
rw₁ : t = s ↔ s = t
rw₂ rw₃ : s = t ↔ s = t
⊢ Rel (flip fun (x1 x2 : α) ↦ x1 = x2) s t ↔ s = t

Tactic:
rw [rel_flip, rel_eq, eq_comm]

Premises used: Multiset.rel_flip, eq_comm, Multiset.rel_eq
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
rw :
  (Eq.{u_1 + 1} (α := Multiset α) 0 0 ∧ b = 0 ∨
      ∃ (a : α),
        ∃ (b_1 : β), ∃ (as : Multiset α), ∃ (bs : Multiset β), r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔
    b = 0
⊢ Rel r 0 b ↔ b = 0

Tactic:
rw [rel_iff]

Premises used: Multiset.rel_iff
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ (Eq.{u_1 + 1} (α := Multiset α) 0 0 ∧ b = 0 ∨
      ∃ (a : α),
        ∃ (b_1 : β), ∃ (as : Multiset α), ∃ (bs : Multiset β), r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔
    b = 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
rw :
  (a = 0 ∧ Eq.{v + 1} (α := Multiset β) 0 0 ∨
      ∃ (a_1 : α),
        ∃ (b : β), ∃ (as : Multiset α), ∃ (bs : Multiset β), r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔
    a = 0
⊢ Rel r a 0 ↔ a = 0

Tactic:
rw [rel_iff]

Premises used: Multiset.rel_iff
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ (a = 0 ∧ Eq.{v + 1} (α := Multiset β) 0 0 ∨
      ∃ (a_1 : α),
        ∃ (b : β), ∃ (as : Multiset α), ∃ (bs : Multiset β), r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔
    a = 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
mp : Rel r (a ::ₘ as) bs → ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
mpr : (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs
⊢ Rel r (a ::ₘ as) bs ↔ ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

Tactic:
constructor
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
mp :
  ∀ (m : Multiset α) (hm : a ::ₘ as = m),
    Rel r m bs → ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
⊢ Rel r (a ::ₘ as) bs → ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

Tactic:
generalize hm : a ::ₘ as = m
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs : Multiset β
m as : Multiset α
hm : a ::ₘ as = 0
⊢ ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ 0 = b ::ₘ bs'

Tactic:
simp at hm
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs_1 : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α} (hm : a ::ₘ as = as'), ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
mp :
  ∀ (ha'b : r a b) (h : Rel r as bs)
    (ih :
      ∀ {as_1 : Multiset α} (hm : a ::ₘ as_1 = as),
        ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as_1 bs' ∧ bs = b ::ₘ bs')
    (hm : a ::ₘ as = a ::ₘ as), ∃ (b_1 : β), ∃ (bs' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
mp₁ :
  ∀ (_h : a ≠ a') (cs : Multiset α) (eq₁ : as = a' ::ₘ cs) (eq₂ : as' = a ::ₘ cs),
    ∃ (b_1 : β), ∃ (bs' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
⊢ ∃ (b_1 : β), ∃ (bs' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
rcases cons_eq_cons.1 hm with (⟨rfl, rfl⟩ | ⟨_h, cs, eq₁, eq₂⟩)

Premises used: Multiset.cons_eq_cons, Iff.mp, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs_1 : Multiset β
m : Multiset α
b : β
bs : Multiset β
as : Multiset α
ha'b : r a b
h : Rel r as bs
ih :
  ∀ {as_1 : Multiset α} (hm : a ::ₘ as_1 = as), ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as_1 bs' ∧ bs = b ::ₘ bs'
hm : a ::ₘ as = a ::ₘ as
⊢ ∃ (b_1 : β), ∃ (bs' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
⟨b, bs, ha'b, h, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs_1 : Multiset β
m : Multiset α
b : β
bs : Multiset β
as : Multiset α
ha'b : r a b
h : Rel r as bs
ih :
  ∀ {as_1 : Multiset α} (hm : a ::ₘ as_1 = as), ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as_1 bs' ∧ bs = b ::ₘ bs'
hm : a ::ₘ as = a ::ₘ as
⊢ ∃ (b_1 : β), ∃ (bs' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
exact ⟨b, bs, ha'b, h, rfl⟩
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs_1 : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α} (hm : a ::ₘ as = as'), ∃ (b : β), ∃ (bs' : Multiset β), 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
mp :
  ∀ (b' : β) (bs' : Multiset β) (h₁ : r a b') (h₂ : Rel r cs bs') (eq : bs = b' ::ₘ bs'),
    ∃ (b_1 : β), ∃ (bs' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
⊢ ∃ (b_1 : β), ∃ (bs' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩

Premises used: Eq.symm
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs_1 : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α} (hm : a ::ₘ as = as'), ∃ (b : β), ∃ (bs' : Multiset β), 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' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩

Premises used: Multiset.cons_swap, Eq.rec, Multiset.cons, Multiset.Rel.cons, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs_1 : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α} (hm : a ::ₘ as = as'), ∃ (b : β), ∃ (bs' : Multiset β), 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' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
h : Rel r m bs
mp : ∀ {as : Multiset α} (hm : a ::ₘ as = 0), ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ 0 = b ::ₘ bs'
mp₁ :
  ∀ {a' : α} {b : β} {as' : Multiset α} {bs : Multiset β} (ha'b : r a' b) (h : Rel r as' bs)
    (ih :
      ∀ {as : Multiset α} (hm : a ::ₘ as = as'), ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs')
    {as : Multiset α} (hm : a ::ₘ as = a' ::ₘ as'),
    ∃ (b_1 : β), ∃ (bs' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
⊢ ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

Tactic:
induction h generalizing as with
    | zero => simp at hm
    | @cons a' b as' bs ha'b h ih =>
      rcases cons_eq_cons.1 hm with (⟨rfl, rfl⟩ | ⟨_h, cs, eq₁, eq₂⟩)
      · exact ⟨b, bs, ha'b, h, rfl⟩
      · rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
        exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩

Premises used: Multiset.cons, Multiset.cons_eq_cons, Iff.mp, Nat.zero, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs

Tactic:
fun ⟨b, bs', hab, h, Eq⟩ => Eq.symm ▸ Rel.cons hab h

Premises used: Eq.rec, Multiset.cons, Multiset.Rel.cons, Multiset.Rel, Eq.symm, _private.0.Multiset.rel_cons_left.match_1
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs

Tactic:
exact fun ⟨b, bs', hab, h, Eq⟩ => Eq.symm ▸ Rel.cons hab h
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
rw :
  (∃ (b_1 : α), ∃ (bs' : Multiset α), flip r b b_1 ∧ Rel (flip r) bs bs' ∧ as = b_1 ::ₘ bs') ↔
    ∃ (a : α), ∃ (as' : Multiset α), r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
⊢ Rel r as (b ::ₘ bs) ↔ ∃ (a : α), ∃ (as' : Multiset α), r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
rw [← rel_flip, rel_cons_left]

Premises used: Multiset.rel_flip, Multiset.rel_cons_left
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ (∃ (b_1 : α), ∃ (bs' : Multiset α), flip r b b_1 ∧ Rel (flip r) bs bs' ∧ as = b_1 ::ₘ bs') ↔
    ∃ (a : α), ∃ (as' : Multiset α), r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
exists₂_congr fun a as' => ?_

Premises used: exists₂_congr
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
refine :
  ∀ (a : α) (as' : Multiset α),
    flip r b a ∧ Rel (flip r) bs as' ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
⊢ (∃ (b_1 : α), ∃ (bs' : Multiset α), flip r b b_1 ∧ Rel (flip r) bs bs' ∧ as = b_1 ::ₘ bs') ↔
    ∃ (a : α), ∃ (as' : Multiset α), r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
refine exists₂_congr fun a as' => ?_

Premises used: exists₂_congr
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
a : α
as' : Multiset α
rw : flip r b a ∧ Rel r as' bs ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
rw₁ rw₂ : r a b ∧ Rel r as' bs ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
⊢ flip r b a ∧ Rel (flip r) bs as' ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
rw [rel_flip, flip]

Premises used: Multiset.rel_flip, flip
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
zero : card.{u_1} (α := α) 0 = card.{v} (α := β) 0
cons :
  ∀ {a : α} {b : β} {as : Multiset α} {bs : Multiset β},
    r a b → Rel r as bs → as.card = bs.card → (a ::ₘ as).card = (b ::ₘ bs).card
⊢ s.card = t.card

Tactic:
induction h
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
⊢ card.{u_1} (α := α) 0 = card.{v} (α := β) 0

Tactic:
simp [*]
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
a : α
b : β
as : Multiset α
bs : Multiset β
h : r a b
h_1 : Rel r as bs
a_ih : as.card = bs.card
⊢ (a ::ₘ as).card = (b ::ₘ bs).card

Tactic:
simp [*]
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
⊢ ∀ {a : α}, Membership.mem (γ := Multiset α) 0 a → ∃ (b : β), Membership.mem (γ := Multiset β) 0 b ∧ r a b

Tactic:
simp
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s_1 : Multiset α
t_1 : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
h : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ (b : β), b ∈ t ∧ r a b
a : α
ha : a ∈ x ::ₘ s
cons : ∀ (ha : a = x), ∃ (b : β), b ∈ y ::ₘ t ∧ r a b
cons₁ : ∀ (ha : a ∈ s), ∃ (b : β), b ∈ y ::ₘ t ∧ r a b
⊢ ∃ (b : β), b ∈ y ::ₘ t ∧ r a b

Tactic:
rcases mem_cons.1 ha with ha | ha

Premises used: Multiset.mem_cons, Iff.mp
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s_1 : Multiset α
t_1 : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
h : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ (b : β), b ∈ t ∧ r a b
a : α
ha_1 : a ∈ x ::ₘ s
ha : a = x
⊢ ∃ (b : β), b ∈ y ::ₘ t ∧ r a b

Tactic:
⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩

Premises used: Eq.rec, And.intro, Exists.intro, Multiset.mem_cons_self, Eq.symm
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s_1 : Multiset α
t_1 : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
h : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ (b : β), b ∈ t ∧ r a b
a : α
ha_1 : a ∈ x ::ₘ s
ha : a = x
⊢ ∃ (b : β), b ∈ y ::ₘ t ∧ r a b

Tactic:
exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s_1 : Multiset α
t_1 : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
h : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ (b : β), b ∈ t ∧ r a b
a : α
ha_1 : a ∈ x ::ₘ s
ha : a ∈ s
cons : ∀ (b : β) (hbt : b ∈ t) (hab : r a b), ∃ (b : β), b ∈ y ::ₘ t ∧ r a b
⊢ ∃ (b : β), b ∈ y ::ₘ t ∧ r a b

Tactic:
rcases ih ha with ⟨b, hbt, hab⟩
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s_1 : Multiset α
t_1 : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
h : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ (b : β), b ∈ t ∧ r a b
a : α
ha_1 : a ∈ x ::ₘ s
ha : a ∈ s
b : β
hbt : b ∈ t
hab : r a b
⊢ ∃ (b : β), b ∈ y ::ₘ t ∧ r a b

Tactic:
⟨b, mem_cons.2 (Or.inr hbt), hab⟩

Premises used: Iff.mpr, Multiset.mem_cons, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s_1 : Multiset α
t_1 : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
h : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ (b : β), b ∈ t ∧ r a b
a : α
ha_1 : a ∈ x ::ₘ s
ha : a ∈ s
b : β
hbt : b ∈ t
hab : r a b
⊢ ∃ (b : β), b ∈ y ::ₘ t ∧ r a b

Tactic:
exact ⟨b, mem_cons.2 (Or.inr hbt), hab⟩