awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have pos : map f ((x ::ₘ s).erase x) = (map f (x ::ₘ s)).erase (f x)
Tactic: cases hxy
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have neg : 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have neg₁ : f y ::ₘ map f (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]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have neg₂ : f y ::ₘ map f (s.erase x) = (f y ::ₘ map f 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have neg₃ : f y ::ₘ map f (s.erase x) = f y ::ₘ (map f 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have neg₄ : f y ::ₘ (map f s).erase (f x) = f y ::ₘ (map f 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s : Multiset α
x : α
h : x ∈ s
⊢ map f (s.erase x) = (map f s).erase (f x)
have 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)
Tactic: induction s using Multiset.induction_on with | empty => simp | cons y s ih => ?_
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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)
have 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)
Tactic: rcases eq_or_ne y x with rfl | hxy
Cleared hypotheses: x, ih, h
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have cons₁ : ∀ (hxy : y ≠ x), map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
Tactic: rcases eq_or_ne y x with rfl | hxy
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (hypothesis)
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
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have h₁ : x ∈ s
Tactic: replace h : x ∈ s := by simpa [hxy.symm] using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have cons : 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)]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have cons₁ : f y ::ₘ map f (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)]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have cons₂ : f y ::ₘ map f (s.erase x) = (f y ::ₘ map f 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)]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have cons₃ : f y ::ₘ (map f s).erase (f x) = (f y ::ₘ map f 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)]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
have cons₄ : f y ::ₘ (map f s).erase (f x) = f y ::ₘ (map f 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)]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
x : β
s : Multiset β
ih : ∃ (a : Multiset α), map f a = s
⊢ ∃ (a : Multiset α), map f a = x ::ₘ s
have cons : ∀ (y : α), ∃ (a : Multiset α), map f a = f y ::ₘ s
Tactic: obtain ⟨y, rfl⟩ := hf x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
ih : ∃ (a : Multiset α), map f a = s
y : α
⊢ ∃ (a : Multiset α), map f a = f y ::ₘ s
have cons : ∀ (t : Multiset α), ∃ (a : Multiset α), map f a = f y ::ₘ map f t
Tactic: obtain ⟨t, rfl⟩ := ih
Cleared hypotheses: s, ih
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
⊢ ∃ (a : Multiset α), map f a = s
have empty : ∃ (a : Multiset α), map f a = 0
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 _ _ _⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
empty : ∃ (a : Multiset α), map f a = 0
⊢ ∃ (a : Multiset α), map f a = s
have cons : ∀ (x : β) (s : Multiset β) (ih : ∃ (a : Multiset α), map f a = s), ∃ (a : Multiset α), map f a = x ::ₘ 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 _ _ _⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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
⊢ p (foldr f x (a ::ₘ s))
have cons : ∀ (q_s : q a ∧ ∀ (x : α), x ∈ s → q x), p (f a (foldr f x s))
Tactic: simp only [forall_mem_cons, foldr_cons] at q_s ⊢
Cleared hypotheses: q_s
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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
⊢ p (foldr f x s)
have empty : ∀ (q_s : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → q a), p (foldr f x 0)
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)
Cleared hypotheses: s, q_s
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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)
⊢ p (foldr f x s)
have 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))
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)
Cleared hypotheses: s, q_s
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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 (foldl f x s)
have rw : p (foldr (fun (x : α) (y : β) ↦ f y x) x s)
Tactic: rw [foldl_swap]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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.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 ⋯)
have rw : List.pmap (P := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧) (mk (p := fun (x : α) ↦ x ∈ a ::ₘ ⟦l⟧)) l sorry =
  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) : α) sorry)
    l sorry
Tactic: rw [List.map_pmap]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
x : { x : α // x ∈ s }
⊢ map (val (p := fun (x : α) ↦ x ∈ s)) (s.attach.erase x) = s.erase (↑x : α)
have rw : (map (val (p := fun (x : α) ↦ x ∈ s)) s.attach).erase (↑x : α) = s.erase (↑x : α)
Tactic: rw [Multiset.map_erase _ val_injective, attach_map_val]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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 : α)
⊢ map (val (p := fun (x : α) ↦ x ∈ s)) (s.attach.erase x) = s.erase (↑x : α)
have rw₁ : s.erase (↑x : α) = s.erase (↑x : α)
Tactic: rw [Multiset.map_erase _ val_injective, attach_map_val]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
s : Multiset α
f : α → β
x : { x : α // x ∈ s }
⊢ map (fun (j : { x : α // x ∈ s }) ↦ f (↑j : α)) (s.attach.erase x) = map f (s.erase (↑x : α))
have simp : map (fun (x : { x : α // x ∈ s }) ↦ (f ∘ val (p := fun (x : α) ↦ x ∈ s)) x) (s.attach.erase x) =
  map f (s.erase (↑x : α))
Tactic: simp only [← Function.comp_apply (f := f)]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
inst : DecidableEq α
s : Multiset α
f : α → β
x : { x : α // x ∈ s }
⊢ map (fun (x : { x : α // x ∈ s }) ↦ (f ∘ val (p := fun (x : α) ↦ x ∈ s)) x) (s.attach.erase x) =
    map f (s.erase (↑x : α))
have rw : map f (map (val (p := fun (x : α) ↦ x ∈ s)) (s.attach.erase x)) = map f (s.erase (↑x : α))
Tactic: rw [← map_map, erase_attach_map_val]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
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 : α))
⊢ map (fun (x : { x : α // x ∈ s }) ↦ (f ∘ val (p := fun (x : α) ↦ x ∈ s)) x) (s.attach.erase x) =
    map f (s.erase (↑x : α))
have rw₁ : map f (s.erase (↑x : α)) = map f (s.erase (↑x : α))
Tactic: rw [← map_map, erase_attach_map_val]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ (↑(l₁.diff l₂) : Multiset α) = foldl erase (↑l₁ : Multiset α) (↑l₂ : Multiset α)
have rw : (↑(List.foldl List.erase l₁ l₂) : Multiset α) = foldl erase (↑l₁ : Multiset α) (↑l₂ : Multiset α)
Tactic: rw [diff_eq_foldl l₁ l₂]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ (↑(List.foldl List.erase l₁ l₂) : Multiset α) = foldl erase (↑l₁ : Multiset α) (↑l₂ : Multiset α)
have symm : foldl erase (↑l₁ : Multiset α) (↑l₂ : Multiset α) = (↑(List.foldl List.erase l₁ l₂) : Multiset α)
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel r s (map f t) ↔ Rel (fun (a : α) (b : γ) ↦ r a (f b)) s t
have rw : Rel (flip fun (a : γ) (b : α) ↦ flip r (f a) b) s t ↔ Rel (fun (a : α) (b : γ) ↦ r a (f b)) s t
Tactic: rw [← rel_flip, rel_map_left, ← rel_flip]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s = map f t ↔ s = t
have rw : Rel (fun (a b : α) ↦ f a = f b) s t ↔ Rel (fun (x1 x2 : α) ↦ x1 = x2) s t
Tactic: rw [← rel_eq, ← rel_eq, rel_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
have rw : ∀ (a : β), a ∈ t ↔ Membership.mem (γ := Multiset β) (map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) sorry) s.attach) a
Tactic: rw [ht.ext]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
rw : ∀ (a : β), a ∈ t ↔ Membership.mem (γ := Multiset β) (map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach) a
⊢ t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
have rw₁ : Nodup.{v} (α := β) (map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) sorry) s.attach)
Tactic: rw [ht.ext]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (hypothesis)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ map f s = map g t
have this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) sorry) s.attach
Tactic: have : t = s.attach.map fun x => i x.1 x.2 := by
    rw [ht.ext]
    · aesop
    · exact hs.attach.map fun x y hxy ↦ Subtype.ext <| i_inj _ x.2 _ y.2 hxy
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
⊢ map f s = pmap (p := Membership.mem s) (fun (x : α) (x_1 : x ∈ s) ↦ f x) s ⋯
have rw : map f s = map f s
Tactic: rw [pmap_eq_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
⊢ Eq.{u_2 + 1} (α := Multiset γ) (pmap (p := Membership.mem s) (fun (x : α) (x_1 : x ∈ s) ↦ f x) s ⋯)
    (map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach)
have rw : Eq.{u_2 + 1} (α := Multiset γ) (map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach)
  (map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach)
Tactic: rw [pmap_eq_map_attach]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
⊢ map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach = map g t
have rw : map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach =
  map (g ∘ fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) sorry) s.attach
Tactic: rw [this, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
⊢ map f s = map g t
have f₁ : map f s = pmap (p := Membership.mem s) (fun (x : α) (x_1 : x ∈ s) ↦ f x) s sorry
Tactic: calc
    s.map f = s.pmap (fun x _ => f x) fun _ => id := by rw [pmap_eq_map]
    _ = s.attach.map fun x => f x.1 := by rw [pmap_eq_map_attach]
    _ = t.map g := by rw [this, Multiset.map_map]; exact map_congr rfl fun x _ => h _ _
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
f₁ : map f s = pmap (p := Membership.mem s) (fun (x : α) (x_1 : x ∈ s) ↦ f x) s ⋯
⊢ map f s = map g t
have f₂ : Eq.{u_2 + 1} (α := Multiset γ) (pmap (p := Membership.mem s) (fun (x : α) (x_1 : x ∈ s) ↦ f x) s sorry)
  (map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach)
Tactic: calc
    s.map f = s.pmap (fun x _ => f x) fun _ => id := by rw [pmap_eq_map]
    _ = s.attach.map fun x => f x.1 := by rw [pmap_eq_map_attach]
    _ = t.map g := by rw [this, Multiset.map_map]; exact map_congr rfl fun x _ => h _ _
-- Lean 4 proof step from Mathlib.Data.Multiset.MapFold (goal)
Goal:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ (a : α), ∃ (ha : a ∈ s), i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun (x : { x : α // x ∈ s }) ↦ i (↑x : α) ⋯) s.attach
f₁ : map f s = pmap (p := Membership.mem s) (fun (x : α) (x_1 : x ∈ s) ↦ f x) s ⋯
f₂ :
  Eq.{u_2 + 1} (α := Multiset γ) (pmap (p := Membership.mem s) (fun (x : α) (x_1 : x ∈ s) ↦ f x) s ⋯)
    (map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach)
⊢ map f s = map g t
have f₃ : map (fun (x : { x : α // x ∈ s }) ↦ f (↑x : α)) s.attach = map g t
Tactic: calc
    s.map f = s.pmap (fun x _ => f x) fun _ => id := by rw [pmap_eq_map]
    _ = s.attach.map fun x => f x.1 := by rw [pmap_eq_map_attach]
    _ = t.map g := by rw [this, Multiset.map_map]; exact map_congr rfl fun x _ => h _ _
-- Lean 4 proof step from Mathlib.Data.Multiset.NatAntidiagonal (goal)
Goal:
n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.1 + x.2 = n
have rw : x ∈ (↑(List.Nat.antidiagonal n) : Multiset (ℕ × ℕ)) ↔ x.1 + x.2 = n
Tactic: rw [antidiagonal, mem_coe, List.Nat.mem_antidiagonal]