awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Pi
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
pos :
  ∀ (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'
⊢ cons (δ := δ) m a (f a ⋯) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) a' h' = f a' h'

Tactic:
subst h
-- Module: Mathlib.Data.Multiset.Pi
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
pos pos₁ : f a' ⋯ = f a' h'
⊢ cons (δ := δ) m a' (f a' ⋯) (fun (a'_1 : α) (ha' : a'_1 ∈ m) ↦ f a'_1 ⋯) a' h' = f a' h'

Tactic:
rw [Pi.cons_same]

Premises used: Multiset.Pi.cons_same
-- Module: Mathlib.Data.Multiset.Pi
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
neg neg₁ : f a' ⋯ = f a' h'
⊢ cons (δ := δ) m a (f a ⋯) (fun (a' : α) (ha' : a' ∈ m) ↦ f a' ⋯) a' h' = f a' h'

Tactic:
rw [Pi.cons_ne _ h]

Premises used: Multiset.Pi.cons_ne
-- Module: Mathlib.Data.Multiset.Pi
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'
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')
⊢ (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')

Tactic:
ext a' ha'
-- Module: Mathlib.Data.Multiset.Pi
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')

Tactic:
(congrArg₂ _ ?_ rfl).trans (apply_dite (@φ _) (a' = a) _ _).symm

Premises used: apply_dite, congrArg₂, Multiset.Pi.cons, Eq.symm, Eq, rfl, Eq.trans
-- Module: Mathlib.Data.Multiset.Pi
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
h :
  Eq.{u_3} (α := (h : a' = a) → δ' a') (fun (h : a' = a) ↦ Eq.ndrec (motive := δ') (φ b) ⋯) fun (h : a' = a) ↦
    φ (Eq.ndrec (motive := δ) b ⋯)
⊢ cons (δ := δ') m a (φ b) (fun (a' : α) (ha' : a' ∈ m) ↦ φ (f a' ha')) a' ha' = φ (cons (δ := δ) m a b f a' ha')

Tactic:
refine (congrArg₂ _ ?_ rfl).trans (apply_dite (@φ _) (a' = a) _ _).symm

Premises used: apply_dite, congrArg₂, Eq.symm, Eq, rfl, Eq.trans
-- Module: Mathlib.Data.Multiset.Pi
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
h : ∀ (b : δ a') (ha' : a' ∈ a' ::ₘ m), Eq.ndrec (motive := δ') (φ b) ⋯ = φ (Eq.ndrec (motive := δ) b ⋯)
⊢ Eq.{u_3} (α := (h : a' = a) → δ' a') (fun (h : a' = a) ↦ Eq.ndrec (motive := δ') (φ b) ⋯) fun (h : a' = a) ↦
    φ (Eq.ndrec (motive := δ) b ⋯)

Tactic:
ext rfl

Premises used: rfl
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
b : δ a'
ha' : a' ∈ a' ::ₘ m
⊢ Eq.ndrec (motive := δ') (φ b) ⋯ = φ (Eq.ndrec (motive := δ) b ⋯)

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Pi
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
dsimp :
  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 ⋯)
⊢ r (cons (δ := δ) m a_1 b₁ f₁ a ha) (cons (δ := δ) m a_1 b₂ f₂ a ha)

Tactic:
dsimp [cons]

Premises used: Multiset.Pi.cons
-- Module: Mathlib.Data.Multiset.Pi
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₂ ⋯)
neg : ∀ (H : ¬a = a_1), r (f₁ a ⋯) (f₂ a ⋯)
⊢ 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 ⋯)

Tactic:
split_ifs with H
-- Module: Mathlib.Data.Multiset.Pi
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
pos :
  ∀ (ha : a_1 ∈ a_1 ::ₘ m),
    r (a := a_1) (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) (Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₁ ⋯)
    (Eq.rec (motive := fun (x : α) (x_1 : a_1 = x) ↦ δ x) b₂ ⋯)

Tactic:
cases H
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
ha : a ∈ a ::ₘ m
⊢ r (a := a) (Eq.rec (motive := fun (x : α) (x_1 : a = x) ↦ δ x) b₁ ⋯)
    (Eq.rec (motive := fun (x : α) (x_1 : a = x) ↦ δ x) b₂ ⋯)

Tactic:
hb
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
ha : a ∈ a ::ₘ m
⊢ r (a := a) (Eq.rec (motive := fun (x : α) (x_1 : a = x) ↦ δ x) b₁ ⋯)
    (Eq.rec (motive := fun (x : α) (x_1 : a = x) ↦ δ x) b₂ ⋯)

Tactic:
exact hb
-- Module: Mathlib.Data.Multiset.Pi
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 (f₁ a ⋯) (f₂ a ⋯)

Tactic:
hf _ _
-- Module: Mathlib.Data.Multiset.Pi
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 (f₁ a ⋯) (f₂ a ⋯)

Tactic:
exact hf _ _
-- Module: Mathlib.Data.Multiset.Pi
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
rw rw₁ : f₁ a' h' = f₁ a' ⋯
⊢ f₁ a' h' = cons (δ := δ) s a b f₁ a' this

Tactic:
rw [Pi.cons_ne this ne.symm]

Premises used: Ne.symm, Multiset.Pi.cons_ne
-- Module: Mathlib.Data.Multiset.Pi
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
rw rw₁ : cons (δ := δ) s a b f₂ a' this = cons (δ := δ) s a b f₂ a' this
⊢ cons (δ := δ) s a b f₁ a' this = cons (δ := δ) s a b f₂ a' this

Tactic:
rw [eq]
-- Module: Mathlib.Data.Multiset.Pi
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
rw rw₁ : f₂ a' ⋯ = f₂ a' h'
⊢ cons (δ := δ) s a b f₂ a' this = f₂ a' h'

Tactic:
rw [Pi.cons_ne this ne.symm]

Premises used: Ne.symm, Multiset.Pi.cons_ne
-- Module: Mathlib.Data.Multiset.Pi
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))
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))
⊢ 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'
-- Module: Mathlib.Data.Multiset.Pi
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'
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))
⊢ 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
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m_1 : Multiset α
t : (a : α) → Multiset (β 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))

Tactic:
rfl
-- Module: Mathlib.Data.Multiset.Pi
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 :
  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)
⊢ 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:
simp only [map_bind, map_map, comp_apply, bind_bind (t a') (t a)]

Premises used: Multiset.bind_bind, Multiset.map_bind, Multiset.map_map, Function.comp_apply
-- Module: Mathlib.Data.Multiset.Pi
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)
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)
⊢ 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:
apply bind_hcongr

Premises used: Multiset.bind_hcongr
-- Module: Mathlib.Data.Multiset.Pi
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 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)
⊢ 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']

Premises used: Multiset.cons_swap
-- Module: Mathlib.Data.Multiset.Pi
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
neg :
  b ∈ t a →
    HEq (α := Multiset ((a_2 : α) → a_2 ∈ a ::ₘ a' ::ₘ m → β a_2))
      ((t a').bind fun (a_2 : β a') ↦
        map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' a_2 x)) n)
      (β := Multiset ((a_2 : α) → a_2 ∈ a' ::ₘ a ::ₘ m → β a_2))
      ((t a').bind fun (a_2 : β a') ↦
        map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' a_2 (Pi.cons (δ := β) m a b x)) n)
⊢ b ∈ t a →
    HEq (α := Multiset ((a_2 : α) → a_2 ∈ a ::ₘ a' ::ₘ m → β a_2))
      ((t a').bind fun (a_2 : β a') ↦
        map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' a_2 x)) n)
      (β := Multiset ((a_2 : α) → a_2 ∈ a' ::ₘ a ::ₘ m → β a_2))
      ((t a').bind fun (a_2 : β a') ↦
        map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' a_2 (Pi.cons (δ := β) m a b x)) n)

Tactic:
_
-- Module: Mathlib.Data.Multiset.Pi
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)
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)
⊢ 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)

Tactic:
apply bind_hcongr

Premises used: Multiset.bind_hcongr
-- Module: Mathlib.Data.Multiset.Pi
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 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)
⊢ 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']

Premises used: Multiset.cons_swap
-- Module: Mathlib.Data.Multiset.Pi
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'
neg :
  b' ∈ t a' →
    HEq (α := Multiset ((a_2 : α) → a_2 ∈ a ::ₘ a' ::ₘ m → β a_2))
      (map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' b' x)) n) (β :=
      Multiset ((a_2 : α) → a_2 ∈ a' ::ₘ a ::ₘ m → β a_2))
      (map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' b' (Pi.cons (δ := β) m a b x)) n)
⊢ b' ∈ t a' →
    HEq (α := Multiset ((a_2 : α) → a_2 ∈ a ::ₘ a' ::ₘ m → β a_2))
      (map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' b' x)) n) (β :=
      Multiset ((a_2 : α) → a_2 ∈ a' ::ₘ a ::ₘ m → β a_2))
      (map (fun (x : (a : α) → a ∈ m → β a) ↦ Pi.cons (δ := β) (a ::ₘ m) a' b' (Pi.cons (δ := β) m a b x)) n)

Tactic:
_
-- Module: Mathlib.Data.Multiset.Pi
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)
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)
⊢ 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)

Tactic:
apply map_hcongr

Premises used: Multiset.map_hcongr
-- Module: Mathlib.Data.Multiset.Pi
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 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)
⊢ 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']

Premises used: Multiset.cons_swap
-- Module: Mathlib.Data.Multiset.Pi
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'
f : (a : α) → a ∈ m → β a
neg :
  f ∈ n →
    Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' b' f) ≍
      Pi.cons (δ := β) (a ::ₘ m) a' b' (Pi.cons (δ := β) m a b f)
⊢ f ∈ n →
    Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' b' f) ≍
      Pi.cons (δ := β) (a ::ₘ m) a' b' (Pi.cons (δ := β) m a b f)

Tactic:
_
-- Module: Mathlib.Data.Multiset.Pi
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'
f : (a : α) → a ∈ m → β a
h_2 : f ∈ n
⊢ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' b' f) ≍
    Pi.cons (δ := β) (a ::ₘ m) a' b' (Pi.cons (δ := β) m a b f)

Tactic:
Pi.cons_swap eq

Premises used: Multiset.Pi.cons_swap
-- Module: Mathlib.Data.Multiset.Pi
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'
f : (a : α) → a ∈ m → β a
h_2 : f ∈ n
⊢ Pi.cons (δ := β) (a' ::ₘ m) a b (Pi.cons (δ := β) m a' b' f) ≍
    Pi.cons (δ := β) (a ::ₘ m) a' b' (Pi.cons (δ := β) m a b f)

Tactic:
exact Pi.cons_swap eq

Premises used: Multiset.Pi.cons_swap
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
⊢ Eq (α := Multiset ((a : α) → Membership.mem (γ := Multiset α) 0 a → β a)) (pi (β := β) 0 t) {Pi.empty β}

Tactic:
rfl

Premises used: Multiset.zero, Multiset.recOn, Multiset.ofList, Multiset.rec, Multiset.pi, rfl
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
a : α
⊢ (a ::ₘ m).pi (β := β) t = (t a).bind fun (b : β a) ↦ map (Pi.cons (δ := β) m a b) (m.pi (β := β) t)

Tactic:
recOn_cons a m

Premises used: Multiset.recOn_cons, Multiset.pi
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ card (α := (a : α) → Membership.mem (γ := Multiset α) 0 a → β a) (pi (β := β) 0 t) =
    prod (map (fun (a : α) ↦ (t a).card) 0)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a : α) (s : Multiset α),
    (s.pi (β := β) t).card = prod (map (fun (a : α) ↦ (t a).card) s) →
      ((a ::ₘ s).pi (β := β) t).card = prod (map (fun (a : α) ↦ (t a).card) (a ::ₘ s))

Tactic:
simp +contextual
-- Module: Mathlib.Data.Multiset.Pi
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 ∧ s.Nodup

Tactic:
simp only [nodup_cons] at hs

Premises used: Multiset.nodup_cons
-- Module: Mathlib.Data.Multiset.Pi
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
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
hs : ¬a ∈ s ∧ s.Nodup
⊢ ¬a ∈ s

Tactic:
hs.1

Premises used: And.left
-- Module: Mathlib.Data.Multiset.Pi
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
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
hs : ¬a ∈ s ∧ s.Nodup
⊢ ¬a ∈ s

Tactic:
exact hs.1

Premises used: And.left