awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
this : x' = x
mp : ∀ (hx' : x ::ₘ m ≤ replicate (n + 1) x) (this : x' = x), m ≤ replicate n x
⊢ m ≤ replicate n x
have mp₁ : ∀ (hx' : x ::ₘ m ≤ x ::ₘ replicate n x) (this : x' = x), m ≤ replicate n x
Tactic: rwa [this, replicate_succ, cons_le_cons_iff] at hx'
Cleared hypotheses: hx', this
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
this : x' = x
mp : ∀ (hx' : x ::ₘ m ≤ replicate (n + 1) x) (this : x' = x), m ≤ replicate n x
mp₁ : ∀ (hx' : x ::ₘ m ≤ x ::ₘ replicate n x) (this : x' = x), m ≤ replicate n x
⊢ m ≤ replicate n x
have mp₂ : ∀ (hx' : m ≤ replicate n x) (this : x' = x), m ≤ replicate n x
Tactic: rwa [this, replicate_succ, cons_le_cons_iff] at hx'
Cleared hypotheses: hx', this
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = n
have h : count a (replicate n a) = List.count a (List.replicate n a)
Tactic: convert! List.count_replicate_self (a := a)
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
⊢ count a (replicate n a) = List.count a (List.replicate n a)
have h : count a (replicate n a) = count a (↑(List.replicate n a) : Multiset α)
Tactic: rw [← coe_count, coe_replicate]
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
h : count a (replicate n a) = count a (↑(List.replicate n a) : Multiset α)
⊢ count a (replicate n a) = List.count a (List.replicate n a)
have h₁ : count a (replicate n a) = count a (replicate n a)
Tactic: rw [← coe_count, coe_replicate]
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = if b = a then n else 0
have h : count a (replicate n b) = List.count a (List.replicate n b)
Tactic: convert! List.count_replicate (a := a)
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
n : ℕ
h : count a (replicate n b) = List.count a (List.replicate n b)
⊢ count a (replicate n b) = if b = a then n else 0
have h₁ : b = a ↔ (b == a) = true
Tactic: convert! List.count_replicate (a := a)
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = List.count a (List.replicate n b)
have h : count a (replicate n b) = count a (↑(List.replicate n b) : Multiset α)
Tactic: rw [← coe_count, coe_replicate]
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
n : ℕ
h : count a (replicate n b) = count a (↑(List.replicate n b) : Multiset α)
⊢ count a (replicate n b) = List.count a (List.replicate n b)
have h₁ : count a (replicate n b) = count a (replicate n b)
Tactic: rw [← coe_count, coe_replicate]
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ count a (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) ↔
    replicate n a ≤ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l
have simp : n ≤ List.count a _l ↔ replicate n a ≤ (↑_l : Multiset α)
Tactic: simp only [quot_mk_to_coe'', coe_count]
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
⊢ r a x
have obtain : ∀ (b : α) (hb1 : b ∈ replicate n a) (hb2 : flip r x b), r a x
Tactic: obtain ⟨b, hb1, hb2⟩ := exists_mem_of_rel_of_mem (rel_flip.2 h) hx
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x b
⊢ r a x
have rwa : ∀ (hb2 : flip r x a), r a x
Tactic: rwa [eq_of_mem_replicate hb1] at hb2
Cleared hypotheses: hb2
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ 0 + t
⊢ s = a ::ₘ a ::ₘ t
have rwa : ∀ (s_eq : s = a ::ₘ (a ::ₘ 0 + t)), s = a ::ₘ a ::ₘ t
Tactic: rwa [cons_add, cons_add, Multiset.zero_add] at s_eq
Cleared hypotheses: s_eq
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ 0 + t
rwa : ∀ (s_eq : s = a ::ₘ (a ::ₘ 0 + t)), s = a ::ₘ a ::ₘ t
⊢ s = a ::ₘ a ::ₘ t
have rwa₁ : ∀ (s_eq : s = a ::ₘ a ::ₘ (0 + t)), s = a ::ₘ a ::ₘ t
Tactic: rwa [cons_add, cons_add, Multiset.zero_add] at s_eq
Cleared hypotheses: s_eq
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ 0 + t
rwa : ∀ (s_eq : s = a ::ₘ (a ::ₘ 0 + t)), s = a ::ₘ a ::ₘ t
rwa₁ : ∀ (s_eq : s = a ::ₘ a ::ₘ (0 + t)), s = a ::ₘ a ::ₘ t
⊢ s = a ::ₘ a ::ₘ t
have rwa₂ : ∀ (s_eq : s = a ::ₘ a ::ₘ t), s = a ::ₘ a ::ₘ t
Tactic: rwa [cons_add, cons_add, Multiset.zero_add] at s_eq
Cleared hypotheses: s_eq
-- Lean 4 proof step from Mathlib.Data.Multiset.Sections (goal)
Goal:
α : Type u_1
a : List α
l : List (List α)
⊢ (↑((↑a : Multiset α) :: List.map (fun (l : List α) ↦ (↑l : Multiset α)) l) : Multiset (Multiset α)).Sections =
    (↑(List.map (fun (l : List α) ↦ (↑l : Multiset α))
          (List.flatMap (fun (s : List α) ↦ List.map (fun (a : α) ↦ a :: s) a) l.sections)) :
      Multiset (Multiset α))
have rw : Eq (α := Multiset (Multiset α))
  (bind (↑(List.map (fun (l : List α) ↦ (↑l : Multiset α)) l.sections) : Multiset (Multiset α)) fun (b : Multiset α) ↦
    map (fun (a : α) ↦ a ::ₘ b) (↑a : Multiset α))
  (↑(List.map (fun (l : List α) ↦ (↑l : Multiset α))
        (List.flatMap (fun (s : List α) ↦ List.map (fun (a : α) ↦ a :: s) a) l.sections)) :
    Multiset (Multiset α))
Tactic: rw [← cons_coe, sections_cons, bind_map_comm, coe_sections l]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sections (goal)
Goal:
α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ {a : Multiset α}, a ∈ s.Sections ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) s a
have empty : ∀ {a : Multiset α},
  Membership.mem (γ := Multiset (Multiset α)) (Sections 0) a ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) 0 a
Tactic: induction s using Multiset.induction_on with
  | empty => simp
  | cons _ _ ih => simp [ih, rel_cons_left, eq_comm]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Sections (goal)
Goal:
α : Type u_1
s : Multiset (Multiset α)
empty :
  ∀ {a : Multiset α},
    Membership.mem (γ := Multiset (Multiset α)) (Sections 0) a ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) 0 a
⊢ ∀ {a : Multiset α}, a ∈ s.Sections ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) s a
have cons : ∀ (a : Multiset α) (s : Multiset (Multiset α))
  (ih : ∀ {a : Multiset α}, a ∈ s.Sections ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) s a) {a_1 : Multiset α},
  a_1 ∈ (a ::ₘ s).Sections ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) (a ::ₘ s) a_1
Tactic: induction s using Multiset.induction_on with
  | empty => simp
  | cons _ _ ih => simp [ih, rel_cons_left, eq_comm]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
r' : β → β → Prop
inst_4 : DecidableRel r'
inst_5 : IsTrans β r'
inst_6 : Std.Antisymm r'
inst_7 : Std.Total r'
hs : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → (r a b ↔ r' (f a) (f b))
⊢ List.map f (s.sort r) = (map f s).sort r'
have revert : ∀ (s : Multiset α) (hs : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → (r a b ↔ r' (f a) (f b))),
  List.map f (s.sort r) = (map f s).sort r'
Tactic: revert s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Multiset.Sort (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ (∀ (b : α), b ∈ s → r a b) → (a ::ₘ s).sort r = a :: s.sort r
have refine : ∀ (l : List α),
  (∀ (b : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) b → r a b) →
    (a ::ₘ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l).sort r =
      a :: sort (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) r
Tactic: refine Quot.inductionOn s fun l => ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Sort (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ a ∈ s.sort r ↔ a ∈ s
have rw : a ∈ (↑(s.sort r) : Multiset α) ↔ a ∈ s
Tactic: rw [← mem_coe, sort_eq]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sort (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
rw : a ∈ (↑(s.sort r) : Multiset α) ↔ a ∈ s
⊢ a ∈ s.sort r ↔ a ∈ s
have rw₁ : a ∈ s ↔ a ∈ s
Tactic: rw [← mem_coe, sort_eq]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ (s.disjSum t).card = s.card + t.card
have rw : (map inl s + map inr t).card = s.card + t.card
Tactic: rw [disjSum, card_add, card_map, card_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
rw : (map inl s + map inr t).card = s.card + t.card
⊢ (s.disjSum t).card = s.card + t.card
have rw₁ : card (α := α ⊕ β) (map inl s) + card (α := α ⊕ β) (map inr t) = s.card + t.card
Tactic: rw [disjSum, card_add, card_map, card_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
rw : (map inl s + map inr t).card = s.card + t.card
rw₁ : card (α := α ⊕ β) (map inl s) + card (α := α ⊕ β) (map inr t) = s.card + t.card
⊢ (s.disjSum t).card = s.card + t.card
have rw₂ : s.card + card (α := α ⊕ β) (map inr t) = s.card + t.card
Tactic: rw [disjSum, card_add, card_map, card_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
rw : (map inl s + map inr t).card = s.card + t.card
rw₁ : card (α := α ⊕ β) (map inl s) + card (α := α ⊕ β) (map inr t) = s.card + t.card
rw₂ : s.card + card (α := α ⊕ β) (map inr t) = s.card + t.card
⊢ (s.disjSum t).card = s.card + t.card
have rw₃ : s.card + t.card = s.card + t.card
Tactic: rw [disjSum, card_add, card_map, card_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
⊢ x ∈ s.disjSum t ↔ (∃ (a : α), a ∈ s ∧ inl a = x) ∨ ∃ (b : β), b ∈ t ∧ inr b = x
have simp_rw : x ∈ map inl s + map inr t ↔ (∃ (a : α), a ∈ s ∧ inl a = x) ∨ ∃ (b : β), b ∈ t ∧ inr b = x
Tactic: simp_rw [disjSum, mem_add, mem_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
simp_rw : x ∈ map inl s + map inr t ↔ (∃ (a : α), a ∈ s ∧ inl a = x) ∨ ∃ (b : β), b ∈ t ∧ inr b = x
⊢ x ∈ s.disjSum t ↔ (∃ (a : α), a ∈ s ∧ inl a = x) ∨ ∃ (b : β), b ∈ t ∧ inr b = x
have simp_rw₁ : Membership.mem (γ := Multiset (α ⊕ β)) (map inl s) x ∨ Membership.mem (γ := Multiset (α ⊕ β)) (map inr t) x ↔
  (∃ (a : α), a ∈ s ∧ inl a = x) ∨ ∃ (b : β), b ∈ t ∧ inr b = x
Tactic: simp_rw [disjSum, mem_add, mem_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ inl a ∈ s.disjSum t ↔ a ∈ s
have rw : (∃ (a_1 : α), a_1 ∈ s ∧ Eq (α := α ⊕ β) (inl a_1) (inl a)) ↔ a ∈ s
Tactic: rw [mem_disjSum, or_iff_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
rw : (∃ (a_1 : α), a_1 ∈ s ∧ Eq (α := α ⊕ β) (inl a_1) (inl a)) ↔ a ∈ s
⊢ inl a ∈ s.disjSum t ↔ a ∈ s
have rw₁ : ¬∃ (b : β), b ∈ t ∧ inr b = inl a
Tactic: rw [mem_disjSum, or_iff_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ inr b ∈ s.disjSum t ↔ b ∈ t
have rw : (∃ (b_1 : β), b_1 ∈ t ∧ Eq (α := α ⊕ β) (inr b_1) (inr b)) ↔ b ∈ t
Tactic: rw [mem_disjSum, or_iff_right]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
rw : (∃ (b_1 : β), b_1 ∈ t ∧ Eq (α := α ⊕ β) (inr b_1) (inr b)) ↔ b ∈ t
⊢ inr b ∈ s.disjSum t ↔ b ∈ t
have rw₁ : ¬∃ (a : α), a ∈ s ∧ inl a = inr b
Tactic: rw [mem_disjSum, or_iff_right]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ (s.disjSum t).Nodup
have refine : Disjoint (Multiset.map inl s) (Multiset.map inr t)
Tactic: refine ((hs.map inl_injective).add_iff <| ht.map inr_injective).2 ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ Disjoint (Multiset.map inl s) (Multiset.map inr t)
have rw : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → inl a ≠ inr b
Tactic: rw [disjoint_map_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
⊢ map f (s.disjSum t) = HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
have simp_rw : map f (map inl s + map inr t) =
  HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
Tactic: simp_rw [disjSum, map_add, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
simp_rw :
  map f (map inl s + map inr t) =
    HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
⊢ map f (s.disjSum t) = HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
have simp_rw₁ : map f (map inl s) + map f (map inr t) =
  HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
Tactic: simp_rw [disjSum, map_add, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
simp_rw :
  map f (map inl s + map inr t) =
    HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
simp_rw₁ :
  map f (map inl s) + map f (map inr t) =
    HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
⊢ map f (s.disjSum t) = HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
have simp_rw₂ : map (f ∘ inl) s + map (f ∘ inr) t =
  HAdd.hAdd (α := Multiset γ) (map (fun (x : α) ↦ f (inl x)) s) (map (fun (x : β) ↦ f (inr x)) t)
Tactic: simp_rw [disjSum, map_add, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
m : Multiset α
x x_1 : List α
h : x ≈ x_1
⊢ Eq.{u_1 + 1} (α := Multiset (Sym2 α)) ((fun (xs : List α) ↦ (↑xs.sym2 : Multiset (Sym2 α))) x)
    ((fun (xs : List α) ↦ (↑xs.sym2 : Multiset (Sym2 α))) x_1)
have rw : x.sym2.Perm x_1.sym2
Tactic: rw [coe_eq_coe]
-- Lean 4 proof step from Mathlib.Data.Multiset.Sym (goal)
Goal:
α : Type u_1
m m' : Multiset α
h : m ≤ m'
⊢ m.sym2 ≤ m'.sym2
have h₁ : ∀ (xs ys : List α) (h : ⟦xs⟧ ≤ ⟦ys⟧), Multiset.sym2 ⟦xs⟧ ≤ Multiset.sym2 ⟦ys⟧
Tactic: induction m, m' using Quotient.inductionOn₂ with | _ xs ys
Cleared hypotheses: m, m', h
-- Lean 4 proof step from Mathlib.Data.Multiset.Sym (goal)
Goal:
α : Type u_1
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ Multiset.sym2 ⟦xs⟧ ≤ Multiset.sym2 ⟦ys⟧
have h₁ : xs <+~ ys
Tactic: suffices xs <+~ ys from this.sym2
-- Lean 4 proof step from Mathlib.Data.Multiset.Sym (goal)
Goal:
α : Type u_1
m : Multiset α
⊢ m.sym2.card = (m.card + 1).choose 2
have refine : ∀ (xs : List α), (Multiset.sym2 ⟦xs⟧).card = (card ⟦xs⟧ + 1).choose 2
Tactic: refine m.inductionOn fun xs => ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u
have rw : s ∪ t ≤ u ∪ t
Tactic: rw [← eq_union_left h₂]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
finj : Injective f
s t : Multiset α
l₁ l₂ : List α
⊢ List.map f (l₁.diff l₂ ++ l₂) = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂
have rw : List.map f (l₁.diff l₂) ++ List.map f l₂ = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂
Tactic: rw [List.map_append, List.map_diff finj]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
finj : Injective f
s t : Multiset α
l₁ l₂ : List α
rw : List.map f (l₁.diff l₂) ++ List.map f l₂ = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂
⊢ List.map f (l₁.diff l₂ ++ l₂) = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂
have rw₁ : (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂ = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂
Tactic: rw [List.map_append, List.map_diff finj]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
⊢ (a ::ₘ s) ∩ t ≤ t
have pos : ∀ (h : a ∈ t), (a ::ₘ s) ∩ t ≤ t
Tactic: by_cases h : a ∈ t
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
pos : ∀ (h : a ∈ t), (a ::ₘ s) ∩ t ≤ t
⊢ (a ::ₘ s) ∩ t ≤ t
have neg : ∀ (h : ¬a ∈ t), (a ::ₘ s) ∩ t ≤ t
Tactic: by_cases h : a ∈ t
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s ∩ t ≤ t
have empty : ∀ {t : Multiset α}, 0 ∩ t ≤ t
Tactic: induction s using Multiset.induction_on generalizing t with
  | empty => exact (zero_inter t).symm ▸ zero_le _
  | cons a s IH =>
    by_cases h : a ∈ t
    · simpa [h] using cons_le_cons a (IH (t := t.erase a))
    · simp [h, IH]
Cleared hypotheses: s, t
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
empty : ∀ {t : Multiset α}, 0 ∩ t ≤ t
⊢ s ∩ t ≤ t
have cons : ∀ (a : α) (s : Multiset α) (IH : ∀ {t : Multiset α}, s ∩ t ≤ t) {t : Multiset α}, (a ::ₘ s) ∩ t ≤ t
Tactic: induction s using Multiset.induction_on generalizing t with
  | empty => exact (zero_inter t).symm ▸ zero_le _
  | cons a s IH =>
    by_cases h : a ∈ t
    · simpa [h] using cons_le_cons a (IH (t := t.erase a))
    · simp [h, IH]
Cleared hypotheses: s, t
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
h₁ : s ≤ t
h₂ : s ≤ u
⊢ s ≤ t ∩ u
have revert : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
Tactic: revert s u
Cleared hypotheses: s, u, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
⊢ ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
have refine_1 : ∀ {s u : Multiset α} (h₁ : s ≤ 0) (h₂ : s ≤ u), s ≤ 0 ∩ u
Tactic: refine @(Multiset.induction_on t ?_ fun a t IH => ?_)
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t : Multiset α
refine_1 : ∀ {s u : Multiset α} (h₁ : s ≤ 0) (h₂ : s ≤ u), s ≤ 0 ∩ u
⊢ ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
have refine_2 : ∀ (a : α) (t : Multiset α) (IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u) {s u : Multiset α}
  (h₁ : s ≤ a ::ₘ t) (h₂ : s ≤ u), s ≤ (a ::ₘ t) ∩ u
Tactic: refine @(Multiset.induction_on t ?_ fun a t IH => ?_)
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
⊢ s ≤ (a ::ₘ t) ∩ u
have pos : ∀ (h : a ∈ u), s ≤ (a ::ₘ t) ∩ u
Tactic: by_cases h : a ∈ u
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
pos : ∀ (h : a ∈ u), s ≤ (a ::ₘ t) ∩ u
⊢ s ≤ (a ::ₘ t) ∩ u
have neg : ∀ (h : ¬a ∈ u), s ≤ (a ::ₘ t) ∩ u
Tactic: by_cases h : a ∈ u
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u
have pos : s.erase a ≤ t ∩ u.erase a
Tactic: rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t_1 : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u), s ≤ t ∩ u
s u : Multiset α
h₁ : s ≤ a ::ₘ t
h₂ : s ≤ u
h : ¬a ∈ u
⊢ s ≤ (a ::ₘ t) ∩ u
have neg : s ≤ t ∩ u
Tactic: rw [cons_inter_of_neg _ h]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
h : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ s ∩ t
have rw : a ∈ a ::ₘ s.erase a ∩ t.erase a
Tactic: rw [← cons_erase h₁, cons_inter_of_pos _ h₂]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s ≤ t
⊢ s ∪ t = t
have rw : t ∪ s = t
Tactic: rw [union_comm, eq_union_left h]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
h : s ≤ t
rw : t ∪ s = t
⊢ s ∪ t = t
have rw₁ : t = t
Tactic: rw [union_comm, eq_union_left h]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ s + u - (t + u) = s - t
have rw : s + u - (u + t) = s - t
Tactic: rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : s + u - (u + t) = s - t
⊢ s + u - (t + u) = s - t
have rw₁ : s + u - u - t = s - t
Tactic: rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : s + u - (u + t) = s - t
rw₁ : s + u - u - t = s - t
⊢ s + u - (t + u) = s - t
have rw₂ : s - t = s - t
Tactic: rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
⊢ s + (t ∪ u) = s + t ∪ (s + u)
have rw : t ∪ u + s = s + t ∪ (s + u)
Tactic: rw [Multiset.add_comm, union_add_distrib, s.add_comm, s.add_comm]
-- Lean 4 proof step from Mathlib.Data.Multiset.UnionInter (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t u : Multiset α
rw : t ∪ u + s = s + t ∪ (s + u)
⊢ s + (t ∪ u) = s + t ∪ (s + u)
have rw₁ : t + s ∪ (u + s) = s + t ∪ (s + u)
Tactic: rw [Multiset.add_comm, union_add_distrib, s.add_comm, s.add_comm]