awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
l : List α
a : α
⊢ (↑l : Multiset α) = {a} ↔ l = [a]
have rw : (↑l : Multiset α) = (↑[a] : Multiset α) ↔ l = [a]
Tactic: rw [← coe_singleton, coe_eq_coe, List.perm_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
l : List α
a : α
rw : (↑l : Multiset α) = (↑[a] : Multiset α) ↔ l = [a]
⊢ (↑l : Multiset α) = {a} ↔ l = [a]
have rw₁ : l ~ [a] ↔ l = [a]
Tactic: rw [← coe_singleton, coe_eq_coe, List.perm_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
l : List α
a : α
rw : (↑l : Multiset α) = (↑[a] : Multiset α) ↔ l = [a]
rw₁ : l ~ [a] ↔ l = [a]
⊢ (↑l : Multiset α) = {a} ↔ l = [a]
have rw₂ : l = [a] ↔ l = [a]
Tactic: rw [← coe_singleton, coe_eq_coe, List.perm_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
m : Multiset α
⊢ {a} = b ::ₘ m ↔ a = b ∧ m = 0
have rw : (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ (cs : Multiset α), 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0
Tactic: rw [← cons_zero, cons_eq_cons]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t ↔ s ≤ t
have refine : s ≤ a ::ₘ t → s ≤ t
Tactic: refine ⟨?_, fun h => le_trans h <| le_cons_self _ _⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t → s ≤ t
have suffices : ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
Tactic: suffices ∀ {t'}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t' by
    exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
t' : Multiset α
h : s ≤ t'
⊢ a ∈ t' → a ::ₘ s ≤ t'
have revert : ∀ (m : ¬a ∈ s), a ∈ t' → a ::ₘ s ≤ t'
Tactic: revert m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ∀ (m : ¬a ∈ s), a ∈ t' → a ::ₘ s ≤ t'
have refine : ∀ {l₁ l₂ : List α},
  l₁ <+ l₂ → ∀ (m : ¬a ∈ (↑l₁ : Multiset α)), a ∈ (↑l₂ : Multiset α) → a ::ₘ (↑l₁ : Multiset α) ≤ (↑l₂ : Multiset α)
Tactic: refine leInductionOn h ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s_1 t : Multiset α
a : α
t' : Multiset α
h : s_1 ≤ t'
l₁ l₂ : List α
s : l₁ <+ l₂
m₁ : ¬a ∈ (↑l₁ : Multiset α)
m₂ : a ∈ (↑l₂ : Multiset α)
⊢ a ::ₘ (↑l₁ : Multiset α) ≤ (↑l₂ : Multiset α)
have rcases : ∀ (r₁ r₂ : List α) (s : l₁ <+ r₁ ++ a :: r₂) (m₂ : a ∈ (↑(r₁ ++ a :: r₂) : Multiset α)),
  a ::ₘ (↑l₁ : Multiset α) ≤ (↑(r₁ ++ a :: r₂) : Multiset α)
Tactic: rcases append_of_mem m₂ with ⟨r₁, r₂, rfl⟩
Cleared hypotheses: l₂, s, m₂
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
⊢ a ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t
have apply : a ∈ t ∧ s ≤ t → a ::ₘ s ≤ t
Tactic: apply Iff.intro (fun h ↦ ⟨subset_of_le h (mem_cons_self a s), le_trans (le_cons_self s a) h⟩)
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
h₁ : a ∈ t
h₂ : s ≤ t
⊢ a ::ₘ s ≤ t
have rcases : ∀ (w : Multiset α) (h₁ : a ∈ a ::ₘ w) (h₂ : s ≤ a ::ₘ w), a ::ₘ s ≤ a ::ₘ w
Tactic: rcases exists_cons_of_mem h₁ with ⟨_, rfl⟩
Cleared hypotheses: t, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s : Multiset α
a : α
⊢ s < {a} ↔ s = 0
have simp : s = 0 → ¬s = {a}
Tactic: simp only [lt_iff_le_and_ne, le_singleton, or_and_right, Ne, and_not_self, or_false,
    and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s : Multiset α
a : α
⊢ s ⊂ {a} ↔ s = 0
have refine_1 : ∀ (hs : s ⊂ {a}) (b : α) (hb : b ∈ s), {a} ⊆ s
Tactic: refine ⟨fun hs ↦ eq_zero_of_subset_zero fun b hb ↦ (hs.2 ?_).elim, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s : Multiset α
a : α
refine_1 : ∀ (hs : s ⊂ {a}) (b : α) (hb : b ∈ s), {a} ⊆ s
⊢ s ⊂ {a} ↔ s = 0
have refine_2 : s = 0 → s ⊂ {a}
Tactic: refine ⟨fun hs ↦ eq_zero_of_subset_zero fun b hb ↦ (hs.2 ?_).elim, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s : Multiset α
a : α
hs : s ⊂ {a}
b : α
hb : b ∈ s
⊢ {a} ⊆ s
have refine_1 : ∀ (hs : s ⊂ {b}), {b} ⊆ s
Tactic: obtain rfl := mem_singleton.1 (hs.1 hb)
Cleared hypotheses: a, hs
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
⊢ card (α := α) {a, b} = 2
have rw : (a ::ₘ {b}).card = 2
Tactic: rw [insert_eq_cons, card_cons, card_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
rw : (a ::ₘ {b}).card = 2
⊢ card (α := α) {a, b} = 2
have rw₁ : card (α := α) {b} + 1 = 2
Tactic: rw [insert_eq_cons, card_cons, card_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
a b : α
rw : (a ::ₘ {b}).card = 2
rw₁ : card (α := α) {b} + 1 = 2
⊢ card (α := α) {a, b} = 2
have rw₂ : HAdd.hAdd (α := ℕ) 1 1 = 2
Tactic: rw [insert_eq_cons, card_cons, card_singleton]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s : Multiset α
n : ℕ
⊢ s.card = n + 1 ↔ ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = s ∧ t.card = n
have refine : s.card = n + 1 → ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = s ∧ t.card = n
Tactic: refine ⟨?_, by aesop⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s : Multiset α
n : ℕ
⊢ s.card = n + 1 → ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = s ∧ t.card = n
have empty : ∀ {n : ℕ}, card.{u_1} (α := α) 0 = n + 1 → ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = 0 ∧ t.card = n
Tactic: induction s using Multiset.induction generalizing n with aesop
Cleared hypotheses: s, n
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s : Multiset α
n : ℕ
empty : ∀ {n : ℕ}, card.{u_1} (α := α) 0 = n + 1 → ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = 0 ∧ t.card = n
⊢ s.card = n + 1 → ∃ (a : α), ∃ (t : Multiset α), a ::ₘ t = s ∧ t.card = n
have 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
Tactic: induction s using Multiset.induction generalizing n with aesop
Cleared hypotheses: s, n
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ m → r x x) → Rel r m m
have refine_1 : (∀ (x : α), Membership.mem (γ := Multiset α) 0 x → r x x) → Rel r 0 0
Tactic: refine m.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m : Multiset α
r : α → α → Prop
refine_1 : (∀ (x : α), Membership.mem (γ := Multiset α) 0 x → r x x) → Rel r 0 0
⊢ (∀ (x : α), x ∈ m → r x x) → Rel r m m
have 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)
Tactic: refine m.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
⊢ Rel (fun (x1 x2 : α) ↦ x1 = x2) s t ↔ s = t
have mp : Rel (fun (x1 x2 : α) ↦ x1 = x2) s t → s = t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
mp : Rel (fun (x1 x2 : α) ↦ x1 = x2) s t → s = t
⊢ Rel (fun (x1 x2 : α) ↦ x1 = x2) s t ↔ s = t
have mpr : s = t → Rel (fun (x1 x2 : α) ↦ x1 = x2) s t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
h : Rel (fun (x1 x2 : α) ↦ x1 = x2) s t
⊢ s = t
have mp : Eq.{u_1 + 1} (α := Multiset α) 0 0
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
h : Rel (fun (x1 x2 : α) ↦ x1 = x2) s t
mp : Eq.{u_1 + 1} (α := Multiset α) 0 0
⊢ s = t
have mp₁ : ∀ {a b : α} {as bs : Multiset α}, a = b → Rel (fun (x1 x2 : α) ↦ x1 = x2) as bs → as = bs → a ::ₘ as = b ::ₘ bs
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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 (a ::ₘ s) (b ::ₘ t)
have cons : Rel p s t
Tactic: apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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
⊢ Rel p s t
have zero : ∀
  (h :
    ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → ∀ (b : β), Membership.mem (γ := Multiset β) 0 b → r a b → p a b),
  Rel p 0 0
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'
Cleared hypotheses: hst, h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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
⊢ Rel p s t
have 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)
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'
Cleared hypotheses: hst, h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
⊢ Rel (flip fun (x1 x2 : α) ↦ x1 = x2) s t ↔ s = t
have rw : Rel (fun (x1 x2 : α) ↦ x1 = x2) t s ↔ s = t
Tactic: rw [rel_flip, rel_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
rw : Rel (fun (x1 x2 : α) ↦ x1 = x2) t s ↔ s = t
⊢ Rel (flip fun (x1 x2 : α) ↦ x1 = x2) s t ↔ s = t
have rw₁ : t = s ↔ s = t
Tactic: rw [rel_flip, rel_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
s t : Multiset α
rw : Rel (fun (x1 x2 : α) ↦ x1 = x2) t s ↔ s = t
rw₁ : t = s ↔ s = t
⊢ Rel (flip fun (x1 x2 : α) ↦ x1 = x2) s t ↔ s = t
have rw₂ : s = t ↔ s = t
Tactic: rw [rel_flip, rel_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ Rel r 0 b ↔ b = 0
have 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
Tactic: rw [rel_iff]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ Rel r a 0 ↔ a = 0
have 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
Tactic: rw [rel_iff]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs ↔ ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
have mp : Rel r (a ::ₘ as) bs → ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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'
⊢ Rel r (a ::ₘ as) bs ↔ ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
have mpr : (∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs → ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
have mp : ∀ (m : Multiset α) (hm : a ::ₘ as = m),
  Rel r m bs → ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
Tactic: generalize hm : a ::ₘ as = m
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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'
⊢ ∃ (b_1 : β), ∃ (bs' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
have 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'
Tactic: rcases cons_eq_cons.1 hm with (⟨rfl, rfl⟩ | ⟨_h, cs, eq₁, eq₂⟩)
Cleared hypotheses: a', as', ha'b, h, ih, hm
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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'
⊢ ∃ (b_1 : β), ∃ (bs' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
have 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'
Tactic: rcases cons_eq_cons.1 hm with (⟨rfl, rfl⟩ | ⟨_h, cs, eq₁, eq₂⟩)
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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_1 : β), ∃ (bs' : Multiset β), r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
have 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'
Tactic: rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
h : Rel r m bs
⊢ ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
have mp : ∀ {as : Multiset α} (hm : a ::ₘ as = 0), ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ 0 = 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 _ _ _⟩
Cleared hypotheses: as, hm, h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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'
⊢ ∃ (b : β), ∃ (bs' : Multiset β), r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
have 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'
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 _ _ _⟩
Cleared hypotheses: as, hm, h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ Rel r as (b ::ₘ bs) ↔ ∃ (a : α), ∃ (as' : Multiset α), r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
have 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'
Tactic: rw [← rel_flip, rel_cons_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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'
have 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'
Tactic: refine exists₂_congr fun a as' => ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
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'
have rw : flip r b a ∧ Rel r as' bs ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
Tactic: rw [rel_flip, flip]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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'
⊢ flip r b a ∧ Rel (flip r) bs as' ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
have rw₁ : r a b ∧ Rel r as' bs ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
Tactic: rw [rel_flip, flip]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ s.card = t.card
have zero : card.{u_1} (α := α) 0 = card.{v} (α := β) 0
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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
⊢ s.card = t.card
have cons : ∀ {a : α} {b : β} {as : Multiset α} {bs : Multiset β},
  r a b → Rel r as bs → as.card = bs.card → (a ::ₘ as).card = (b ::ₘ bs).card
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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
⊢ ∃ (b : β), b ∈ y ::ₘ t ∧ r a b
have cons : ∀ (ha : a = x), ∃ (b : β), b ∈ y ::ₘ t ∧ r a b
Tactic: rcases mem_cons.1 ha with ha | ha
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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
⊢ ∃ (b : β), b ∈ y ::ₘ t ∧ r a b
have cons₁ : ∀ (ha : a ∈ s), ∃ (b : β), b ∈ y ::ₘ t ∧ r a b
Tactic: rcases mem_cons.1 ha with ha | ha
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
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 : β), b ∈ y ::ₘ t ∧ r a b
have cons : ∀ (b : β) (hbt : b ∈ t) (hab : r a b), ∃ (b : β), b ∈ y ::ₘ t ∧ r a b
Tactic: rcases ih ha with ⟨b, hbt, hab⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ ∀ {a : α}, a ∈ s → ∃ (b : β), b ∈ t ∧ r a b
have zero : ∀ {a : α}, Membership.mem (γ := Multiset α) 0 a → ∃ (b : β), Membership.mem (γ := Multiset β) 0 b ∧ r a b
Tactic: induction h with
  | zero => simp
  | @cons x y s t hxy _ ih =>
    intro a ha
    rcases mem_cons.1 ha with ha | ha
    · exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩
    · rcases ih ha with ⟨b, hbt, hab⟩
      exact ⟨b, mem_cons.2 (Or.inr hbt), hab⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
zero : ∀ {a : α}, Membership.mem (γ := Multiset α) 0 a → ∃ (b : β), Membership.mem (γ := Multiset β) 0 b ∧ r a b
⊢ ∀ {a : α}, a ∈ s → ∃ (b : β), b ∈ t ∧ r a b
have cons : ∀ {x : α} {y : β} {s : Multiset α} {t : Multiset β} (hxy : r x y),
  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
Tactic: induction h with
  | zero => simp
  | @cons x y s t hxy _ ih =>
    intro a ha
    rcases mem_cons.1 ha with ha | ha
    · exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩
    · rcases ih ha with ⟨b, hbt, hab⟩
      exact ⟨b, mem_cons.2 (Or.inr hbt), hab⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m1 m2 : Multiset α
r : α → α → Prop
h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b
hc : m1.card = m2.card
⊢ Rel r m1 m2
have revert : ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) (hc : m1.card = m2.card), Rel r m1 m2
Tactic: revert m1
Cleared hypotheses: m1, h, hc
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) (hc : m1.card = m2.card), Rel r m1 m2
have refine_1 : ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → Membership.mem (γ := Multiset α) 0 b → r a b)
  (hc : m1.card = card.{u_1} (α := α) 0), Rel r m1 0
Tactic: refine @(m2.induction_on ?_ ?_)