awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a' : α
f : (a'_1 : α) → a'_1 ∈ a' ::ₘ m → δ a'_1
h' : a' ∈ a' ::ₘ m
⊢ cons (δ := δ) m a' (f a' ⋯) (fun (a'_1 : α) (ha' : a'_1 ∈ m) ↦ f a'_1 ⋯) a' h' = f a' h'
have pos : f a' sorry = f a' h'
Tactic: rw [Pi.cons_same]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ cons (δ := δ) m a (f a ⋯) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) a' h' = f a' h'
have neg : f a' sorry = f a' h'
Tactic: rw [Pi.cons_ne _ h]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
⊢ (cons (δ := δ') m a (φ b) fun (a' : α) (ha' : a' ∈ m) ↦ φ (f a' ha')) = fun (a' : α) (ha' : a' ∈ a ::ₘ m) ↦
    φ (cons (δ := δ) m a b f a' ha')
have h : ∀ (a' : α) (ha' : a' ∈ a ::ₘ m),
  cons (δ := δ') m a (φ b) (fun (a' : α) (ha' : a' ∈ m) ↦ φ (f a' ha')) a' ha' = φ (cons (δ := δ) m a b f a' ha')
Tactic: ext a' ha'
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
ha' : a' ∈ a ::ₘ m
⊢ cons (δ := δ') m a (φ b) (fun (a' : α) (ha' : a' ∈ m) ↦ φ (f a' ha')) a' ha' = φ (cons (δ := δ) m a b f a' ha')
have h : Eq.{u_3} (α := (h : a' = a) → δ' a') (fun (h : a' = a) ↦ Eq.ndrec (motive := δ') (φ b) sorry) fun (h : a' = a) ↦
  φ (Eq.ndrec (motive := δ) b sorry)
Tactic: refine (congrArg₂ _ ?_ rfl).trans (apply_dite (@φ _) (a' = a) _ _).symm
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
ha' : a' ∈ a ::ₘ m
⊢ Eq.{u_3} (α := (h : a' = a) → δ' a') (fun (h : a' = a) ↦ Eq.ndrec (motive := δ') (φ b) ⋯) fun (h : a' = a) ↦
    φ (Eq.ndrec (motive := δ) b ⋯)
have h : ∀ (b : δ a') (ha' : a' ∈ a' ::ₘ m), Eq.ndrec (motive := δ') (φ b) sorry = φ (Eq.ndrec (motive := δ) b sorry)
Tactic: ext rfl
Cleared hypotheses: a, b, ha'
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a_1 : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a_1
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a_1 ::ₘ m
⊢ r (cons (δ := δ) m a_1 b₁ f₁ a ha) (cons (δ := δ) m a_1 b₂ f₂ a ha)
have dsimp : r (a := a) (if h : a = a_1 then Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₁ sorry else f₁ a sorry)
  (if h : a = a_1 then Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₂ sorry else f₂ a sorry)
Tactic: dsimp [cons]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a_1 : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a_1
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a_1 ::ₘ m
⊢ r (a := a) (if h : a = a_1 then Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₁ ⋯ else f₁ a ⋯)
    (if h : a = a_1 then Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₂ ⋯ else f₂ a ⋯)
have pos : ∀ (H : a = a_1),
  r (a := a) (Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₁ sorry)
    (Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₂ sorry)
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a_1 : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a_1
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a_1 ::ₘ m
pos :
  ∀ (H : a = a_1),
    r (a := a) (Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₁ ⋯)
      (Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₂ ⋯)
⊢ r (a := a) (if h : a = a_1 then Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₁ ⋯ else f₁ a ⋯)
    (if h : a = a_1 then Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₂ ⋯ else f₂ a ⋯)
have neg : ∀ (H : ¬a = a_1), r (f₁ a sorry) (f₂ a sorry)
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a_1 : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a_1
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a_1 ::ₘ m
H : a = a_1
⊢ r (a := a) (Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₁ ⋯)
    (Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₂ ⋯)
have pos : ∀ (ha : a_1 ∈ a_1 ::ₘ m),
  r (a := a_1) (Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₁ sorry)
    (Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₂ sorry)
Tactic: cases H
Cleared hypotheses: a, ha, H
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons (δ := δ) s a b f₁ = cons (δ := δ) s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ f₁ a' h' = cons (δ := δ) s a b f₁ a' this
have rw : f₁ a' h' = f₁ a' sorry
Tactic: rw [Pi.cons_ne this ne.symm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons (δ := δ) s a b f₁ = cons (δ := δ) s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ cons (δ := δ) s a b f₁ a' this = cons (δ := δ) s a b f₂ a' this
have rw : cons (δ := δ) s a b f₂ a' this = cons (δ := δ) s a b f₂ a' this
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons (δ := δ) s a b f₁ = cons (δ := δ) s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ cons (δ := δ) s a b f₂ a' this = f₂ a' h'
have rw : f₂ a' sorry = f₂ a' h'
Tactic: rw [Pi.cons_ne this ne.symm]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
⊢ HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    ((t a).bind fun (b : β a) ↦
      map (Pi.cons (δ := β) (a' ::ₘ m) a b) ((t a').bind fun (b : β a') ↦ map (Pi.cons (δ := β) m a' b) n))
    (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    ((t a').bind fun (b : β a') ↦
      map (Pi.cons (δ := β) (a ::ₘ m) a' b) ((t a).bind fun (b : β a) ↦ map (Pi.cons (δ := β) m a b) n))
have pos : ∀ (eq : a = a'),
  HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    ((t a).bind fun (b : β a) ↦
      map (Pi.cons (δ := β) (a' ::ₘ m) a b) ((t a').bind fun (b : β a') ↦ map (Pi.cons (δ := β) m a' b) n))
    (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    ((t a').bind fun (b : β a') ↦
      map (Pi.cons (δ := β) (a ::ₘ m) a' b) ((t a).bind fun (b : β a) ↦ map (Pi.cons (δ := β) m a b) n))
Tactic: by_cases eq : a = a'
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
pos :
  ∀ (eq : a = a'),
    HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
      ((t a).bind fun (b : β a) ↦
        map (Pi.cons (δ := β) (a' ::ₘ m) a b) ((t a').bind fun (b : β a') ↦ map (Pi.cons (δ := β) m a' b) n))
      (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
      ((t a').bind fun (b : β a') ↦
        map (Pi.cons (δ := β) (a ::ₘ m) a' b) ((t a).bind fun (b : β a) ↦ map (Pi.cons (δ := β) m a b) n))
⊢ HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    ((t a).bind fun (b : β a) ↦
      map (Pi.cons (δ := β) (a' ::ₘ m) a b) ((t a').bind fun (b : β a') ↦ map (Pi.cons (δ := β) m a' b) n))
    (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    ((t a').bind fun (b : β a') ↦
      map (Pi.cons (δ := β) (a ::ₘ m) a' b) ((t a).bind fun (b : β a) ↦ map (Pi.cons (δ := β) m a b) n))
have neg : ∀ (eq : ¬a = a'),
  HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    ((t a).bind fun (b : β a) ↦
      map (Pi.cons (δ := β) (a' ::ₘ m) a b) ((t a').bind fun (b : β a') ↦ map (Pi.cons (δ := β) m a' b) n))
    (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    ((t a').bind fun (b : β a') ↦
      map (Pi.cons (δ := β) (a ::ₘ m) a' b) ((t a).bind fun (b : β a) ↦ map (Pi.cons (δ := β) m a b) n))
Tactic: by_cases eq : a = a'
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : a = a'
⊢ HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    ((t a).bind fun (b : β a) ↦
      map (Pi.cons (δ := β) (a' ::ₘ m) a b) ((t a').bind fun (b : β a') ↦ map (Pi.cons (δ := β) m a' b) n))
    (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    ((t a').bind fun (b : β a') ↦
      map (Pi.cons (δ := β) (a ::ₘ m) a' b) ((t a).bind fun (b : β a) ↦ map (Pi.cons (δ := β) m a b) n))
have pos : HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a ::ₘ m → β a_1))
  ((t a).bind fun (b : β a) ↦
    map (Pi.cons (δ := β) (a ::ₘ m) a b) ((t a).bind fun (b : β a) ↦ map (Pi.cons (δ := β) m a b) n))
  (β := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a ::ₘ m → β a_1))
  ((t a).bind fun (b : β a) ↦
    map (Pi.cons (δ := β) (a ::ₘ m) a b) ((t a).bind fun (b : β a) ↦ map (Pi.cons (δ := β) m a b) n))
Tactic: subst eq
Cleared hypotheses: a', eq
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    ((t a).bind fun (b : β a) ↦
      map (Pi.cons (δ := β) (a' ::ₘ m) a b) ((t a').bind fun (b : β a') ↦ map (Pi.cons (δ := β) m a' b) n))
    (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    ((t a').bind fun (b : β a') ↦
      map (Pi.cons (δ := β) (a ::ₘ m) a' b) ((t a).bind fun (b : β a) ↦ map (Pi.cons (δ := β) m a b) n))
have neg : HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
  ((t a).bind fun (b : β a) ↦
    (t a').bind fun (a_1 : β a') ↦
      map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' a_1 x)) n)
  (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
  ((t a).bind fun (b : β a) ↦
    (t a').bind fun (a_1 : β a') ↦
      map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' a_1 (Pi.cons (δ := β) m a b x)) n)
Tactic: simp only [map_bind, map_map, comp_apply, bind_bind (t a') (t a)]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    ((t a).bind fun (b : β a) ↦
      (t a').bind fun (a_1 : β a') ↦
        map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' a_1 x)) n)
    (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    ((t a).bind fun (b : β a) ↦
      (t a').bind fun (a_1 : β a') ↦
        map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' a_1 (Pi.cons (δ := β) m a b x)) n)
have neg : Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
Tactic: apply bind_hcongr
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
neg : Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
⊢ HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    ((t a).bind fun (b : β a) ↦
      (t a').bind fun (a_1 : β a') ↦
        map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' a_1 x)) n)
    (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    ((t a).bind fun (b : β a) ↦
      (t a').bind fun (a_1 : β a') ↦
        map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' a_1 (Pi.cons (δ := β) m a b x)) n)
have neg₁ : ∀ (a_1 : β a),
  a_1 ∈ t a →
    HEq (α := Multiset ((a_3 : α) → a_3 ∈ a ::ₘ a' ::ₘ m → β a_3))
      ((t a').bind fun (a_3 : β a') ↦
        map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a a_1 (Pi.cons (δ := β) m a' a_3 x)) n)
      (β := Multiset ((a_3 : α) → a_3 ∈ a' ::ₘ a ::ₘ m → β a_3))
      ((t a').bind fun (a_3 : β a') ↦
        map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' a_3 (Pi.cons (δ := β) m a a_1 x)) n)
Tactic: apply bind_hcongr
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
have neg : Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
Tactic: rw [cons_swap a a']
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
h : b ∈ t a
⊢ HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    ((t a').bind fun (a_1 : β a') ↦
      map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' a_1 x)) n)
    (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    ((t a').bind fun (a_1 : β a') ↦
      map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' a_1 (Pi.cons (δ := β) m a b x)) n)
have neg : Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
Tactic: apply bind_hcongr
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
h : b ∈ t a
neg : Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
⊢ HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    ((t a').bind fun (a_1 : β a') ↦
      map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' a_1 x)) n)
    (β := Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    ((t a').bind fun (a_1 : β a') ↦
      map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' a_1 (Pi.cons (δ := β) m a b x)) n)
have neg₁ : ∀ (a_1 : β a'),
  a_1 ∈ t a' →
    HEq (α := Multiset ((a_3 : α) → a_3 ∈ a ::ₘ a' ::ₘ m → β a_3))
      (map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' a_1 x)) n) (β :=
      Multiset ((a_3 : α) → a_3 ∈ a' ::ₘ a ::ₘ m → β a_3))
      (map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' a_1 (Pi.cons (δ := β) m a b x)) n)
Tactic: apply bind_hcongr
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
h : b ∈ t a
⊢ Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
have neg : Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
Tactic: rw [cons_swap a a']
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
h : b ∈ t a
b' : β a'
h_1 : b' ∈ t a'
⊢ HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    (map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' b' x)) n) (β :=
    Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    (map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' b' (Pi.cons (δ := β) m a b x)) n)
have neg : Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
Tactic: apply map_hcongr
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
h : b ∈ t a
b' : β a'
h_1 : b' ∈ t a'
neg : Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
⊢ HEq (α := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1))
    (map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' b' x)) n) (β :=
    Multiset ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1))
    (map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' b' (Pi.cons (δ := β) m a b x)) n)
have neg₁ : ∀ (a_1 : (a : α) → a ∈ m → β a),
  a_1 ∈ n →
    Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' b' a_1) ≍
      Pi.cons (δ := β) (a ::ₘ m) a' b' (Pi.cons (δ := β) m a b a_1)
Tactic: apply map_hcongr
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
h : b ∈ t a
b' : β a'
h_1 : b' ∈ t a'
⊢ Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
have neg : Eq (α := Type (max u_1 u_2)) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1) ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
Tactic: rw [cons_swap a a']
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
s_1 : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi (β := β) t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
⊢ ¬a ∈ s
have hs₁ : ¬a ∈ s ∧ s.Nodup
Tactic: simp only [nodup_cons] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
s_1 : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi (β := β) t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
⊢ ((a ::ₘ s).pi (β := β) t).Nodup
have has : ¬a ∈ s
Tactic: have has : a ∉ s := by simp only [nodup_cons] at hs; exact hs.1
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
s_1 : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi (β := β) t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
⊢ s.Nodup
have hs₁ : ¬a ∈ s ∧ s.Nodup
Tactic: simp only [nodup_cons] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
s_1 : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi (β := β) t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
⊢ ((a ::ₘ s).pi (β := β) t).Nodup
have hs₁ : s.Nodup
Tactic: have hs : Nodup s := by simp only [nodup_cons] at hs; exact hs.2
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
s_1 : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi (β := β) t).Nodup
hs_1 : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
⊢ ((a ::ₘ s).pi (β := β) t).Nodup
have simp : (∀ (a_1 : β a), a_1 ∈ t a → (Multiset.map (Pi.cons (δ := β) s a a_1) (s.pi (β := β) t)).Nodup) ∧
  Pairwise
    (onFun (β := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s → β a_1)) Disjoint fun (b : β a) ↦
      Multiset.map (Pi.cons (δ := β) s a b) (s.pi (β := β) t))
    (t a)
Tactic: simp only [pi_cons, nodup_bind]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
s_1 : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi (β := β) t).Nodup
hs_1 : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
⊢ (∀ (a_1 : β a), a_1 ∈ t a → (Multiset.map (Pi.cons (δ := β) s a a_1) (s.pi (β := β) t)).Nodup) ∧
    Pairwise
      (onFun (β := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s → β a_1)) Disjoint fun (b : β a) ↦
        Multiset.map (Pi.cons (δ := β) s a b) (s.pi (β := β) t))
      (t a)
have b : Pairwise
  (onFun (β := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s → β a_1)) Disjoint fun (b : β a) ↦
    Multiset.map (Pi.cons (δ := β) s a b) (s.pi (β := β) t))
  (t a)
Tactic: refine
        ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),
          ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
s_1 : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi (β := β) t).Nodup
hs_1 : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
⊢ Pairwise
    (onFun (β := Multiset ((a_1 : α) → a_1 ∈ a ::ₘ s → β a_1)) Disjoint fun (b : β a) ↦
      Multiset.map (Pi.cons (δ := β) s a b) (s.pi (β := β) t))
    (t a)
have refine : ∀ (a_1 : β a),
  a_1 ∈ t a →
    ∀ (b : β a),
      b ∈ t a →
        a_1 ≠ b →
          onFun (β := Multiset ((a_5 : α) → a_5 ∈ a ::ₘ s → β a_5)) Disjoint
            (fun (b : β a) ↦ Multiset.map (Pi.cons (δ := β) s a b) (s.pi (β := β) t)) a_1 b
Tactic: refine (ht a <| mem_cons_self _ _).pairwise ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
s_1 : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi (β := β) t).Nodup
hs_1 : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
b₁ : β a
h : b₁ ∈ t a
b₂ : β a
h_1 : b₂ ∈ t a
neb : b₁ ≠ b₂
f : (a : α) → a ∈ s → β a
h_2 : f ∈ s.pi (β := β) t
g : (a : α) → a ∈ s → β a
h_3 : g ∈ s.pi (β := β) t
eq : Pi.cons (δ := β) s a b₁ f = Pi.cons (δ := β) s a b₂ g
⊢ Pi.cons (δ := β) s a b₁ f a ⋯ = Pi.cons (δ := β) s a b₂ g a ⋯
have rw : Pi.cons (δ := β) s a b₂ g a sorry = Pi.cons (δ := β) s a b₂ g a sorry
Tactic: rw [eq]