awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
pos : ∀ (hxy : y = x), map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
neg : ∀ (hxy : ¬y = x), map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
by_cases hxy : y = x
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
hxy : y = x
pos : map f ((x ::ₘ s).erase x) = (map f (x ::ₘ s)).erase (f x)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
cases hxy
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
⊢ map f ((x ::ₘ s).erase x) = (map f (x ::ₘ s)).erase (f x)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
hxy : ¬y = x
neg : map f (y ::ₘ s.erase x) = (map f (y ::ₘ s)).erase (f x)
neg₁ : f y ::ₘ map f (s.erase x) = (map f (y ::ₘ s)).erase (f x)
neg₂ : f y ::ₘ map f (s.erase x) = (f y ::ₘ map f s).erase (f x)
neg₃ : f y ::ₘ map f (s.erase x) = f y ::ₘ (map f s).erase (f x)
neg₄ neg₅ : f y ::ₘ (map f s).erase (f x) = f y ::ₘ (map f s).erase (f x)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
rw [s.erase_cons_tail hxy, map_cons, map_cons, (s.map f).erase_cons_tail (hf.ne hxy), ih]

Premises used: Multiset.map_cons, Multiset.map, Function.Injective.ne, Multiset.erase_cons_tail
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
x : α
h : Membership.mem (γ := Multiset α) 0 x
⊢ map f (erase 0 x) = (map f 0).erase (f x)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : ∀ (h : x ∈ s), map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
?_
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
x : α
h : x ∈ s
cons :
  ∀ (y : α) (s : Multiset α) (ih : ∀ (h : x ∈ s), map f (s.erase x) = (map f s).erase (f x)) (h : x ∈ y ::ₘ s),
    map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
⊢ map f (s.erase x) = (map f s).erase (f x)

Tactic:
induction s using Multiset.induction_on with | empty => simp | cons y s ih => ?_

Premises used: Multiset.cons
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : ∀ (h : x ∈ s), map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
cons :
  ∀ (ih : ∀ (h : y ∈ s), map f (s.erase y) = (map f s).erase (f y)) (h : y ∈ y ::ₘ s),
    map f ((y ::ₘ s).erase y) = (map f (y ::ₘ s)).erase (f y)
cons₁ : ∀ (hxy : y ≠ x), map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
rcases eq_or_ne y x with rfl | hxy

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
y : α
s : Multiset α
ih : ∀ (h : y ∈ s), map f (s.erase y) = (map f s).erase (f y)
h : y ∈ y ::ₘ s
⊢ map f ((y ::ₘ s).erase y) = (map f (y ::ₘ s)).erase (f y)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : ∀ (h : x ∈ s), map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
hxy : y ≠ x
⊢ x ∈ s

Tactic:
simpa [hxy.symm] using h

Premises used: Ne.symm
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : ∀ (h : x ∈ s), map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
hxy : y ≠ x
⊢ x ∈ s

Tactic:
replace h : x ∈ s := by simpa [hxy.symm] using h
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : ∀ (h : x ∈ s), map f (s.erase x) = (map f s).erase (f x)
hxy : y ≠ x
h : x ∈ s
cons : map f (y ::ₘ s.erase x) = (map f (y ::ₘ s)).erase (f x)
cons₁ : f y ::ₘ map f (s.erase x) = (map f (y ::ₘ s)).erase (f x)
cons₂ : f y ::ₘ map f (s.erase x) = (f y ::ₘ map f s).erase (f x)
cons₃ : f y ::ₘ (map f s).erase (f x) = (f y ::ₘ map f s).erase (f x)
cons₄ cons₅ : f y ::ₘ (map f s).erase (f x) = f y ::ₘ (map f s).erase (f x)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
rw [s.erase_cons_tail hxy, map_cons, map_cons, ih h, erase_cons_tail_of_mem (mem_map_of_mem f h)]

Premises used: Multiset.map_cons, Multiset.mem_map_of_mem, Multiset.erase_cons_tail, Multiset.erase_cons_tail_of_mem
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
⊢ ∃ (a : Multiset α), map f a = 0

Tactic:
⟨0, map_zero _⟩

Premises used: Multiset.map_zero, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
⊢ ∃ (a : Multiset α), map f a = 0

Tactic:
exact ⟨0, map_zero _⟩
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
x : β
s : Multiset β
ih : ∃ (a : Multiset α), map f a = s
cons : ∀ (y : α), ∃ (a : Multiset α), map f a = f y ::ₘ s
⊢ ∃ (a : Multiset α), map f a = x ::ₘ s

Tactic:
obtain ⟨y, rfl⟩ := hf x

Premises used: rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
ih : ∃ (a : Multiset α), map f a = s
y : α
cons : ∀ (t : Multiset α), ∃ (a : Multiset α), map f a = f y ::ₘ map f t
⊢ ∃ (a : Multiset α), map f a = f y ::ₘ s

Tactic:
obtain ⟨t, rfl⟩ := ih

Premises used: rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
y : α
t : Multiset α
⊢ ∃ (a : Multiset α), map f a = f y ::ₘ map f t

Tactic:
⟨y ::ₘ t, map_cons _ _ _⟩

Premises used: Multiset.map_cons, Multiset.cons, Exists.intro
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
y : α
t : Multiset α
⊢ ∃ (a : Multiset α), map f a = f y ::ₘ map f t

Tactic:
exact ⟨y ::ₘ t, map_cons _ _ _⟩
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
empty : ∃ (a : Multiset α), map f a = 0
cons : ∀ (x : β) (s : Multiset β) (ih : ∃ (a : Multiset α), map f a = s), ∃ (a : Multiset α), map f a = x ::ₘ s
⊢ ∃ (a : Multiset α), map f a = s

Tactic:
induction s using Multiset.induction_on with
  | empty => exact ⟨0, map_zero _⟩
  | cons x s ih =>
    obtain ⟨y, rfl⟩ := hf x
    obtain ⟨t, rfl⟩ := ih
    exact ⟨y ::ₘ t, map_cons _ _ _⟩

Premises used: Multiset.cons, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : β → α → β
inst : RightCommutative f
b : β
⊢ foldl f b 0 = b

Tactic:
rfl

Premises used: List.foldl, Multiset.foldl, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : β → α → β
inst : RightCommutative f
b : β
a : α
s : Multiset α
⊢ foldl f b (a ::ₘ s) = foldl f (f b a) s

Tactic:
Quot.inductionOn s fun _l => rfl

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : β → α → β
inst : RightCommutative f
b : β
s t : Multiset α
⊢ foldl f b (s + t) = foldl f (foldl f b s) t

Tactic:
Quotient.inductionOn₂ s t fun _ _ => foldl_append

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
b : β
⊢ foldr f b 0 = b

Tactic:
rfl

Premises used: Multiset.foldr, List.foldr, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
b : β
a : α
s : Multiset α
⊢ foldr f b (a ::ₘ s) = f a (foldr f b s)

Tactic:
Quot.inductionOn s fun _l => rfl

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
b : β
a : α
⊢ foldr f b {a} = f a b

Tactic:
rfl

Premises used: Multiset.foldr, List.foldr, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
b : β
s t : Multiset α
⊢ foldr f b (s + t) = foldr f (foldr f b t) s

Tactic:
Quotient.inductionOn₂ s t fun _ _ => foldr_append

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
b : β
l : List α
⊢ foldr f b (↑l : Multiset α) = List.foldr f b l

Tactic:
rfl

Premises used: Multiset.foldr, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : β → α → β
inst : RightCommutative f
b : β
l : List α
⊢ foldl f b (↑l : Multiset α) = List.foldl f b l

Tactic:
rfl

Premises used: Multiset.foldl, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
b : β
l : List α
⊢ foldr f b (↑l : Multiset α) = List.foldl (fun (x : β) (y : α) ↦ f y x) b l

Tactic:
(congr_arg (foldr f b) (coe_reverse l)).symm.trans foldr_reverse

Premises used: Multiset.foldr, List.foldr_reverse, congr_arg, Multiset.coe_reverse, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
b : β
s : Multiset α
⊢ foldr f b s = foldl (fun (x : β) (y : α) ↦ f y x) b s

Tactic:
Quot.inductionOn s fun _l => coe_foldr_swap _ _ _

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : β → α → β
inst : RightCommutative f
b : β
s : Multiset α
⊢ foldl f b s = foldr (fun (x : α) (y : β) ↦ f y x) b s

Tactic:
(foldr_swap _ _ _).symm

Premises used: Multiset.foldr_swap, Eq.symm
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
q_s : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → q a
⊢ p (foldr f x 0)

Tactic:
simpa
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
ihs : ∀ (q_s : ∀ (a : α), a ∈ s → q a), p (foldr f x s)
q_s : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
cons : ∀ (q_s : q a ∧ ∀ (x : α), x ∈ s → q x), p (f a (foldr f x s))
⊢ p (foldr f x (a ::ₘ s))

Tactic:
simp only [forall_mem_cons, foldr_cons] at q_s ⊢

Premises used: Multiset.foldr_cons, Multiset.forall_mem_cons
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
ihs : ∀ (q_s : ∀ (a : α), a ∈ s → q a), p (foldr f x s)
q_s : q a ∧ ∀ (x : α), x ∈ s → q x
⊢ p (f a (foldr f x s))

Tactic:
hpqf _ _ q_s.1 (ihs q_s.2)

Premises used: And.right, And.left
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
ihs : ∀ (q_s : ∀ (a : α), a ∈ s → q a), p (foldr f x s)
q_s : q a ∧ ∀ (x : α), x ∈ s → q x
⊢ p (f a (foldr f x s))

Tactic:
exact hpqf _ _ q_s.1 (ihs q_s.2)

Premises used: And.right, And.left
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β → β
inst : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
empty : ∀ (q_s : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → q a), p (foldr f x 0)
cons :
  ∀ (a : α) (s : Multiset α) (ihs : ∀ (q_s : ∀ (a : α), a ∈ s → q a), p (foldr f x s))
    (q_s : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1), p (foldr f x (a ::ₘ s))
⊢ p (foldr f x s)

Tactic:
induction s using Multiset.induction with
  | empty => simpa
  | cons a s ihs =>
    simp only [forall_mem_cons, foldr_cons] at q_s ⊢
    exact hpqf _ _ q_s.1 (ihs q_s.2)

Premises used: Multiset.cons, Multiset.foldr_cons, Multiset.forall_mem_cons
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
f : α → α → α
inst : LeftCommutative f
x : α
p : α → Prop
s : Multiset α
p_f : ∀ (a b : α), p a → p b → p (f a b)
px : p x
p_s : ∀ (a : α), a ∈ s → p a
⊢ p (foldr f x s)

Tactic:
foldr_induction' f x p p s p_f px p_s

Premises used: Multiset.foldr_induction'
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : β → α → β
inst : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
rw : p (foldr (fun (x : α) (y : β) ↦ f y x) x s)
⊢ p (foldl f x s)

Tactic:
rw [foldl_swap]

Premises used: Multiset.foldl_swap
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : β → α → β
inst : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr (fun (x : α) (y : β) ↦ f y x) x s)

Tactic:
foldr_induction' (fun x y => f y x) x q p s hpqf px q_s

Premises used: Multiset.foldr_induction'
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : β → α → β
inst : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr (fun (x : α) (y : β) ↦ f y x) x s)

Tactic:
exact foldr_induction' (fun x y => f y x) x q p s hpqf px q_s

Premises used: Multiset.foldr_induction'
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
f : α → α → α
inst : RightCommutative f
x : α
p : α → Prop
s : Multiset α
p_f : ∀ (a b : α), p a → p b → p (f b a)
px : p x
p_s : ∀ (a : α), a ∈ s → p a
⊢ p (foldl f x s)

Tactic:
foldl_induction' f x p p s p_f px p_s

Premises used: Multiset.foldl_induction'
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
p : α → Prop
f : α → β
s : Multiset α
⊢ ∀ (H : ∀ (a : α), a ∈ s → p a), pmap (p := p) (fun (a : α) (x : p a) ↦ f a) s H = map f s

Tactic:
Quot.inductionOn s fun _ H => congr_arg _ <| List.pmap_eq_map H

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
g : β → γ
f : (a : α) → p a → β
s : Multiset α
⊢ ∀ (H : ∀ (a : α), a ∈ s → p a), map g (pmap (p := p) f s H) = pmap (p := p) (fun (a : α) (h : p a) ↦ g (f a h)) s H

Tactic:
Quot.inductionOn s fun _ H => congr_arg _ <| List.map_pmap H

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
⊢ ∀ (H : ∀ (a : α), a ∈ s → p a), pmap (p := p) f s H = map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α) ⋯) s.attach

Tactic:
Quot.inductionOn s fun _ H => congr_arg _ <| List.pmap_eq_map_attach H

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ map (fun (i : { x : α // x ∈ s }) ↦ f (↑i : α)) s.attach = map f s

Tactic:
Quot.inductionOn s fun _ => congr_arg _ List.attach_map_val

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
s : Multiset α
⊢ map (val (p := fun (x : α) ↦ x ∈ s)) s.attach = s

Tactic:
(attach_map_val' _ _).trans s.map_id

Premises used: Multiset.map_id, Multiset.attach_map_val', Eq.trans
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
a : α
m : Multiset α
l : List α
rw :
  List.pmap (P := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧) (mk (p := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧)) l ⋯ =
    List.pmap (P := fun (x : α) ↦ x ∈ ⟦l⟧)
      (fun (a_1 : α) (h : a_1 ∈ ⟦l⟧) ↦
        mk (p := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧) (↑(mk (p := fun (x : α) ↦ x ∈ ⟦l⟧) a_1 h) : α) ⋯)
      l ⋯
⊢ List.pmap (P := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧) (mk (p := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧)) l ⋯ =
    List.map (fun (p : { x : α // x ∈ ⟦l⟧ }) ↦ mk (p := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧) (↑p : α) ⋯)
      (List.pmap (P := fun (x : α) ↦ x ∈ ⟦l⟧) (mk (p := fun (x : α) ↦ x ∈ ⟦l⟧)) l ⋯)

Tactic:
rw [List.map_pmap]

Premises used: List.map_pmap
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
a : α
m : Multiset α
l : List α
⊢ List.pmap (P := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧) (mk (p := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧)) l ⋯ =
    List.pmap (P := fun (x : α) ↦ x ∈ ⟦l⟧)
      (fun (a_1 : α) (h : a_1 ∈ ⟦l⟧) ↦
        mk (p := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧) (↑(mk (p := fun (x : α) ↦ x ∈ ⟦l⟧) a_1 h) : α) ⋯)
      l ⋯

Tactic:
List.pmap_congr_left _ fun _ _ _ _ => Subtype.ext rfl

Premises used: List.pmap_congr_left, rfl, Subtype.ext
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
a : α
m : Multiset α
l : List α
⊢ List.pmap (P := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧) (mk (p := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧)) l ⋯ =
    List.pmap (P := fun (x : α) ↦ x ∈ ⟦l⟧)
      (fun (a_1 : α) (h : a_1 ∈ ⟦l⟧) ↦
        mk (p := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧) (↑(mk (p := fun (x : α) ↦ x ∈ ⟦l⟧) a_1 h) : α) ⋯)
      l ⋯

Tactic:
exact List.pmap_congr_left _ fun _ _ _ _ => Subtype.ext rfl

Premises used: List.pmap_congr_left, rfl, Subtype.ext
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
x : { x : α // x ∈ s }
rw : (map (val (p := fun (x : α) ↦ x ∈ s)) s.attach).erase (↑x : α) = s.erase (↑x : α)
rw₁ rw₂ : s.erase (↑x : α) = s.erase (↑x : α)
⊢ map (val (p := fun (x : α) ↦ x ∈ s)) (s.attach.erase x) = s.erase (↑x : α)

Tactic:
rw [Multiset.map_erase _ val_injective, attach_map_val]

Premises used: Subtype.val_injective, Multiset.map_erase, Multiset.attach_map_val
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
s : Multiset α
f : α → β
x : { x : α // x ∈ s }
simp :
  map (fun (x : { x : α // x ∈ s }) ↦ (f ∘ val (p := fun (x : α) ↦ x ∈ s)) x) (s.attach.erase x) =
    map f (s.erase (↑x : α))
⊢ map (fun (j : { x : α // x ∈ s }) ↦ f (↑j : α)) (s.attach.erase x) = map f (s.erase (↑x : α))

Tactic:
simp only [← Function.comp_apply (f := f)]

Premises used: Function.comp_apply
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
s : Multiset α
f : α → β
x : { x : α // x ∈ s }
rw : map f (map (val (p := fun (x : α) ↦ x ∈ s)) (s.attach.erase x)) = map f (s.erase (↑x : α))
rw₁ rw₂ : map f (s.erase (↑x : α)) = map f (s.erase (↑x : α))
⊢ map (fun (x : { x : α // x ∈ s }) ↦ (f ∘ val (p := fun (x : α) ↦ x ∈ s)) x) (s.attach.erase x) =
    map f (s.erase (↑x : α))

Tactic:
rw [← map_map, erase_attach_map_val]

Premises used: Multiset.map_map, Multiset.erase_attach_map_val
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
rw : (↑(List.foldl List.erase l₁ l₂) : Multiset α) = foldl erase (↑l₁ : Multiset α) (↑l₂ : Multiset α)
⊢ (↑(l₁.diff l₂) : Multiset α) = foldl erase (↑l₁ : Multiset α) (↑l₂ : Multiset α)

Tactic:
rw [diff_eq_foldl l₁ l₂]

Premises used: List.diff_eq_foldl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
symm : foldl erase (↑l₁ : Multiset α) (↑l₂ : Multiset α) = (↑(List.foldl List.erase l₁ l₂) : Multiset α)
⊢ (↑(List.foldl List.erase l₁ l₂) : Multiset α) = foldl erase (↑l₁ : Multiset α) (↑l₂ : Multiset α)

Tactic:
symm
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ foldl erase (↑l₁ : Multiset α) (↑l₂ : Multiset α) = (↑(List.foldl List.erase l₁ l₂) : Multiset α)

Tactic:
foldl_hom _ fun x y => rfl

Premises used: List.foldl_hom, Multiset.foldl, rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ foldl erase (↑l₁ : Multiset α) (↑l₂ : Multiset α) = (↑(List.foldl List.erase l₁ l₂) : Multiset α)

Tactic:
exact foldl_hom _ fun x y => rfl

Premises used: List.foldl_hom
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset γ
f : γ → α
⊢ ∀ {t : Multiset β}, Rel r (map f 0) t ↔ Rel (fun (a : γ) (b : β) ↦ r (f a) b) 0 t

Tactic:
simp
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset γ
f : γ → α
⊢ ∀ (a : γ) (s : Multiset γ),
    (∀ {t : Multiset β}, Rel r (map f s) t ↔ Rel (fun (a : γ) (b : β) ↦ r (f a) b) s t) →
      ∀ {t : Multiset β}, Rel r (map f (a ::ₘ s)) t ↔ Rel (fun (a : γ) (b : β) ↦ r (f a) b) (a ::ₘ s) t

Tactic:
simp +contextual [rel_cons_left]

Premises used: Multiset.rel_cons_left
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
rw : Rel (flip fun (a : γ) (b : α) ↦ flip r (f a) b) s t ↔ Rel (fun (a : α) (b : γ) ↦ r a (f b)) s t
⊢ Rel r s (map f t) ↔ Rel (fun (a : α) (b : γ) ↦ r a (f b)) s t

Tactic:
rw [← rel_flip, rel_map_left, ← rel_flip]

Premises used: Multiset.rel_flip, Multiset.rel_map_left
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip fun (a : γ) (b : α) ↦ flip r (f a) b) s t ↔ Rel (fun (a : α) (b : γ) ↦ r a (f b)) s t

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → γ
g : β → δ
⊢ Rel p (map f s) (map g t) ↔ Rel (fun (a : α) (b : β) ↦ p (f a) (g b)) s t

Tactic:
rel_map_left.trans rel_map_right

Premises used: Multiset.rel_map_left, Multiset.rel_map_right, Iff.trans
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
rw : Rel (fun (a b : α) ↦ f a = f b) s t ↔ Rel (fun (x1 x2 : α) ↦ x1 = x2) s t
⊢ map f s = map f t ↔ s = t

Tactic:
rw [← rel_eq, ← rel_eq, rel_map]

Premises used: Multiset.rel_eq, Multiset.rel_map
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun (a b : α) ↦ f a = f b) s t ↔ Rel (fun (x1 x2 : α) ↦ x1 = x2) s t

Tactic:
simp only [hf.eq_iff]

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
⊢ Injective (map f)

Tactic:
fun _x _y => (map_eq_map hf).1

Premises used: Multiset.map_eq_map, Iff.mp, Function.Injective
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
r : α → α → Prop
s t : Multiset α
hst : Rel r s t
a b : α
as bs : Multiset α
hab : r a b
_hst : Rel r as bs
ih : map (Quot.mk r) as = map (Quot.mk r) bs
⊢ map (Quot.mk r) (a ::ₘ as) = map (Quot.mk r) (b ::ₘ bs)

Tactic:
simp [ih, Quot.sound hab]

Premises used: Quot.sound
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
r : α → α → Prop
s : Multiset (Quot r)
⊢ ∃ (t : Multiset α), s = map (Quot.mk r) t

Tactic:
Multiset.induction_on s ⟨0, rfl⟩ fun a _s ⟨t, ht⟩ =>
    Quot.inductionOn a fun a => ht.symm ▸ ⟨a ::ₘ t, (map_cons _ _ _).symm⟩

Premises used: Multiset.induction_on
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
r : α → α → Prop
p : Multiset (Quot r) → Prop
s : Multiset (Quot r)
⊢ (∀ (s : Multiset α), p (map (Quot.mk r) s)) → p s

Tactic:
match s, exists_multiset_eq_map_quot_mk s with
  | _, ⟨_t, rfl⟩ => fun h => h _

Premises used: _private.0.Multiset.induction_on_multiset_quot.match_1, Multiset.exists_multiset_eq_map_quot_mk
-- Module: Mathlib.Data.Multiset.MapFold
Goal:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ (map f s).Nodup → s.Nodup

Tactic:
Quot.induction_on s fun _ => List.Nodup.of_map f

Premises used: Quot.induction_on