awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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

Tactic:
have has : a ∉ s := by simp only [nodup_cons] at hs; exact hs.1
-- 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
has : ¬a ∈ s
⊢ ¬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
has : ¬a ∈ s
hs : ¬a ∈ s ∧ s.Nodup
⊢ s.Nodup

Tactic:
hs.2

Premises used: And.right
-- 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
has : ¬a ∈ s
hs : ¬a ∈ s ∧ s.Nodup
⊢ s.Nodup

Tactic:
exact hs.2

Premises used: And.right
-- 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
has : ¬a ∈ s
⊢ s.Nodup

Tactic:
have hs : Nodup s := by simp only [nodup_cons] at hs; exact hs.2
-- 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_1 : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
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)
⊢ ((a ::ₘ s).pi (β := β) t).Nodup

Tactic:
simp only [pi_cons, nodup_bind]

Premises used: Multiset.pi_cons, Multiset.nodup_bind
-- 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_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)

Tactic:
⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),
          ?_⟩

Premises used: Multiset.Nodup.map, Multiset.mem_cons_of_mem, And.intro, Multiset.Pi.cons_injective
-- 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_1 : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
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)
⊢ (∀ (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:
refine
        ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),
          ?_⟩
-- 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_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)

Tactic:
(ht a <| mem_cons_self _ _).pairwise ?_

Premises used: Multiset.Nodup.pairwise, Multiset.mem_cons_self
-- 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_1 : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
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
⊢ 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 (ht a <| mem_cons_self _ _).pairwise ?_

Premises used: Multiset.Nodup.pairwise, Multiset.mem_cons_self
-- 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_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
rw rw₁ : Pi.cons (δ := β) s a b₂ g a ⋯ = Pi.cons (δ := β) s a b₂ g a ⋯
⊢ Pi.cons (δ := β) s a b₁ f a ⋯ = Pi.cons (δ := β) s a b₂ g a ⋯

Tactic:
rw [eq]
-- 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_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
this : Pi.cons (δ := β) s a b₁ f a ⋯ = Pi.cons (δ := β) s a b₂ g a ⋯
rwa : ∀ (this : b₁ = Pi.cons (δ := β) s a b₂ g a ⋯), b₁ = b₂
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : b₁ = b₂), b₁ = b₂
⊢ b₁ = b₂

Tactic:
rwa [Pi.cons_same, Pi.cons_same] at this

Premises used: Multiset.Pi.cons_same
-- 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_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 →
      ∀ (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:
exact fun b₁ _ b₂ _ neb =>
        disjoint_map_map.2 fun f _ g _ eq =>
          have : Pi.cons s a b₁ f a (mem_cons_self _ _) =
            Pi.cons s a b₂ g a (mem_cons_self _ _) := by rw [eq]
          neb <| show b₁ = b₂ by rwa [Pi.cons_same, Pi.cons_same] at this

Premises used: Iff.mpr, Multiset.disjoint_map_map
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → Membership.mem (γ := Multiset α) 0 a → β a
⊢ f = Pi.empty β

Tactic:
have : f = Pi.empty β := funext (fun _ => funext fun h => (notMem_zero _ h).elim)
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → Membership.mem (γ := Multiset α) 0 a → β a
this : f = Pi.empty β
empty : ∀ (a : α) (h : Membership.mem (γ := Multiset α) 0 a), Pi.empty β a h ∈ t a
⊢ Membership.mem (γ := Multiset ((a : α) → Membership.mem (γ := Multiset α) 0 a → β a)) (pi (β := β) 0 t) f ↔
    ∀ (a : α) (h : Membership.mem (γ := Multiset α) 0 a), f a h ∈ t a

Tactic:
simp only [this, pi_zero, mem_singleton, true_iff]

Premises used: true_iff, Multiset.mem_singleton, Multiset.pi_zero
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → Membership.mem (γ := Multiset α) 0 a → β a
this : f = Pi.empty β
a : α
h : Membership.mem (γ := Multiset α) 0 a
⊢ Pi.empty β a h ∈ t a

Tactic:
(notMem_zero _ h).elim

Premises used: Multiset.notMem_zero, False.elim
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → Membership.mem (γ := Multiset α) 0 a → β a
this : f = Pi.empty β
a : α
h : Membership.mem (γ := Multiset α) 0 a
⊢ Pi.empty β a h ∈ t a

Tactic:
exact (notMem_zero _ h).elim

Premises used: Multiset.notMem_zero, False.elim
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ f ∈ (a ::ₘ m).pi (β := β) t ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1

Tactic:
?_
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m → β a
cons :
  ∀ (a : α) (m : Multiset α)
    (ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a)
    (f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1),
    f ∈ (a ::ₘ m).pi (β := β) t ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a

Tactic:
induction m using Multiset.induction_on with
  | empty =>
    have : f = Pi.empty β := funext (fun _ => funext fun h => (notMem_zero _ h).elim)
    simp only [this, pi_zero, mem_singleton, true_iff]
    intro _ h; exact (notMem_zero _ h).elim
  | cons a m ih => ?_

Premises used: true_iff, Multiset.cons, Multiset.mem_singleton, Multiset.pi_zero
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
cons :
  (∃ (a_1 : β a),
      a_1 ∈ t a ∧
        ∃ (a_2 : (a : α) → a ∈ m → β a), (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons (δ := β) m a a_1 a_2 = f) ↔
    ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ f ∈ (a ::ₘ m).pi (β := β) t ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1

Tactic:
simp_rw [pi_cons, mem_bind, mem_map, ih]

Premises used: Multiset.pi_cons, Multiset.mem_map, Multiset.mem_bind
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
cons :
  (∃ (a_1 : β a),
      a_1 ∈ t a ∧
        ∃ (a_2 : (a : α) → a ∈ m → β a), (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons (δ := β) m a a_1 a_2 = f) →
    ∀ (a_2 : α) (h : a_2 ∈ a ::ₘ m), f a_2 h ∈ t a_2
cons₁ :
  (∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1) →
    ∃ (a_2 : β a),
      a_2 ∈ t a ∧
        ∃ (a_3 : (a : α) → a ∈ m → β a), (∀ (a : α) (h : a ∈ m), a_3 a h ∈ t a) ∧ Pi.cons (δ := β) m a a_2 a_3 = f
⊢ (∃ (a_1 : β a),
      a_1 ∈ t a ∧
        ∃ (a_2 : (a : α) → a ∈ m → β a), (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons (δ := β) m a a_1 a_2 = f) ↔
    ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1

Tactic:
constructor
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
pos : ∀ (h : a' = a), Pi.cons (δ := β) m a b f' a' ha' ∈ t a'
neg : ∀ (h : ¬a' = a), Pi.cons (δ := β) m a b f' a' ha' ∈ t a'
⊢ Pi.cons (δ := β) m a b f' a' ha' ∈ t a'

Tactic:
by_cases h : a' = a
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : a' = a
pos : ∀ (b : β a') (hb : b ∈ t a') (ha' : a' ∈ a' ::ₘ m), Pi.cons (δ := β) m a' b f' a' ha' ∈ t a'
⊢ Pi.cons (δ := β) m a b f' a' ha' ∈ t a'

Tactic:
subst h
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
b : β a'
hb : b ∈ t a'
ha' : a' ∈ a' ::ₘ m
pos pos₁ pos₂ pos₃ : b ∈ t a'
⊢ Pi.cons (δ := β) m a' b f' a' ha' ∈ t a'

Tactic:
rwa [Pi.cons_same]

Premises used: Multiset.Pi.cons_same
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
neg : f' a' ⋯ ∈ t a'
⊢ Pi.cons (δ := β) m a b f' a' ha' ∈ t a'

Tactic:
rw [Pi.cons_ne _ h]

Premises used: Multiset.Pi.cons_ne
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ f' a' ⋯ ∈ t a'

Tactic:
apply hf'
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ ∃ (a_1 : β a),
    a_1 ∈ t a ∧
      ∃ (a_2 : (a : α) → a ∈ m → β a), (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons (δ := β) m a a_1 a_2 = f

Tactic:
⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), ?_⟩

Premises used: Multiset.mem_cons_of_mem, And.intro, Exists.intro, Multiset.mem_cons_self
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
cons : (Pi.cons (δ := β) m a (f a ⋯) fun (a_1 : α) (ha : a_1 ∈ m) ↦ f a_1 ⋯) = f
⊢ ∃ (a_1 : β a),
    a_1 ∈ t a ∧
      ∃ (a_2 : (a : α) → a ∈ m → β a), (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons (δ := β) m a a_1 a_2 = f

Tactic:
refine ⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), ?_⟩
-- Module: Mathlib.Data.Multiset.Pi
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
cons cons₁ : f = f
⊢ (Pi.cons (δ := β) m a (f a ⋯) fun (a_1 : α) (ha : a_1 ∈ m) ↦ f a_1 ⋯) = f

Tactic:
rw [Pi.cons_eta]

Premises used: Multiset.Pi.cons_eta
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
⊢ powersetAux l = List.map ofList l.sublists

Tactic:
rfl

Premises used: Multiset.powersetAux, rfl
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
s : Multiset α
⊢ ∀ (a : List α), ⟦a⟧ ∈ powersetAux l ↔ ⟦a⟧ ≤ (↑l : Multiset α)

Tactic:
simp [powersetAux_eq_map_coe, Subperm, and_comm]

Premises used: and_comm, Multiset.powersetAux_eq_map_coe, List.Subperm
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
⊢ List.map ofList l.sublists ~ powersetAux' l

Tactic:
(sublists_perm_sublists' _).map _

Premises used: Multiset.powersetAux', List.sublists_perm_sublists', List.Perm.map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l : List α
⊢ List.map ofList l.sublists ~ powersetAux' l

Tactic:
exact (sublists_perm_sublists' _).map _

Premises used: List.sublists_perm_sublists', List.Perm.map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List (Multiset α)) (powersetAux' []) [0]

Tactic:
rfl

Premises used: Multiset.powersetAux', List.map, Multiset.zero, Multiset.ofList, rfl
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
a : α
l : List α
⊢ powersetAux' (a :: l) = powersetAux' l ++ List.map (cons a) (powersetAux' l)

Tactic:
simp [powersetAux']

Premises used: Multiset.powersetAux'
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
⊢ Perm.{u_1} (α := Multiset α) (powersetAux' []) (powersetAux' [])

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
x : α
l₁_1 l₂_1 : List α
h : l₁_1 ~ l₂_1
IH : powersetAux' l₁_1 ~ powersetAux' l₂_1
cons :
  powersetAux' l₁_1 ++ List.map (Multiset.cons x) (powersetAux' l₁_1) ~
    powersetAux' l₂_1 ++ List.map (Multiset.cons x) (powersetAux' l₂_1)
⊢ powersetAux' (x :: l₁_1) ~ powersetAux' (x :: l₂_1)

Tactic:
simp only [powersetAux'_cons]

Premises used: Multiset.powersetAux'_cons
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
x : α
l₁_1 l₂_1 : List α
h : l₁_1 ~ l₂_1
IH : powersetAux' l₁_1 ~ powersetAux' l₂_1
⊢ powersetAux' l₁_1 ++ List.map (cons x) (powersetAux' l₁_1) ~
    powersetAux' l₂_1 ++ List.map (cons x) (powersetAux' l₂_1)

Tactic:
IH.append (IH.map _)

Premises used: List.Perm.append, List.Perm.map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
x : α
l₁_1 l₂_1 : List α
h : l₁_1 ~ l₂_1
IH : powersetAux' l₁_1 ~ powersetAux' l₂_1
⊢ powersetAux' l₁_1 ++ List.map (cons x) (powersetAux' l₁_1) ~
    powersetAux' l₂_1 ++ List.map (cons x) (powersetAux' l₂_1)

Tactic:
exact IH.append (IH.map _)

Premises used: List.Perm.append, List.Perm.map
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
swap :
  powersetAux' l ++
      (List.map (cons a) (powersetAux' l) ++
        (List.map (cons b) (powersetAux' l) ++ List.map (cons b ∘ cons a) (powersetAux' l))) ~
    powersetAux' l ++
      (List.map (cons b) (powersetAux' l) ++
        (List.map (cons a) (powersetAux' l) ++ List.map (cons a ∘ cons b) (powersetAux' l)))
⊢ powersetAux' (b :: a :: l) ~ powersetAux' (a :: b :: l)

Tactic:
simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]

Premises used: List.append_assoc, List.map_map, Multiset.powersetAux'_cons, List.map_append
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
swap :
  List.map (cons a) (powersetAux' l) ++
      (List.map (cons b) (powersetAux' l) ++ List.map (cons b ∘ cons a) (powersetAux' l)) ~
    List.map (cons b) (powersetAux' l) ++
      (List.map (cons a) (powersetAux' l) ++ List.map (cons a ∘ cons b) (powersetAux' l))
⊢ powersetAux' l ++
      (List.map (cons a) (powersetAux' l) ++
        (List.map (cons b) (powersetAux' l) ++ List.map (cons b ∘ cons a) (powersetAux' l))) ~
    powersetAux' l ++
      (List.map (cons b) (powersetAux' l) ++
        (List.map (cons a) (powersetAux' l) ++ List.map (cons a ∘ cons b) (powersetAux' l)))

Tactic:
apply Perm.append_left

Premises used: List.Perm.append_left
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
h : ∀ (s : Multiset α), (cons b ∘ cons a) s = (cons a ∘ cons b) s
⊢ cons b ∘ cons a = cons a ∘ cons b

Tactic:
funext s
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
s : Multiset α
⊢ (cons b ∘ cons a) s = (cons a ∘ cons b) s

Tactic:
simp [cons_swap]

Premises used: Multiset.cons_swap
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
swap :
  List.map (cons a) (powersetAux' l) ++ List.map (cons b) (powersetAux' l) ++
      List.map (cons a ∘ cons b) (powersetAux' l) ~
    List.map (cons b) (powersetAux' l) ++ List.map (cons a) (powersetAux' l) ++
      List.map (cons a ∘ cons b) (powersetAux' l)
⊢ List.map (cons a) (powersetAux' l) ++
      (List.map (cons b) (powersetAux' l) ++ List.map (cons b ∘ cons a) (powersetAux' l)) ~
    List.map (cons b) (powersetAux' l) ++
      (List.map (cons a) (powersetAux' l) ++ List.map (cons a ∘ cons b) (powersetAux' l))

Tactic:
rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]

Premises used: List.append_assoc
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
⊢ List.map (cons a) (powersetAux' l) ++ List.map (cons b) (powersetAux' l) ++
      List.map (cons a ∘ cons b) (powersetAux' l) ~
    List.map (cons b) (powersetAux' l) ++ List.map (cons a) (powersetAux' l) ++
      List.map (cons a ∘ cons b) (powersetAux' l)

Tactic:
perm_append_comm.append_right _

Premises used: List.perm_append_comm, List.Perm.append_right
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
⊢ List.map (cons a) (powersetAux' l) ++ List.map (cons b) (powersetAux' l) ++
      List.map (cons a ∘ cons b) (powersetAux' l) ~
    List.map (cons b) (powersetAux' l) ++ List.map (cons a) (powersetAux' l) ++
      List.map (cons a ∘ cons b) (powersetAux' l)

Tactic:
exact perm_append_comm.append_right _

Premises used: List.perm_append_comm, List.Perm.append_right
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ l₁_1 l₂_1 l₃ : List α
h : l₁_1 ~ l₂_1
h_1 : l₂_1 ~ l₃
IH₁ : powersetAux' l₁_1 ~ powersetAux' l₂_1
IH₂ : powersetAux' l₂_1 ~ powersetAux' l₃
⊢ powersetAux' l₁_1 ~ powersetAux' l₃

Tactic:
IH₁.trans IH₂

Premises used: List.Perm.trans
-- Module: Mathlib.Data.Multiset.Powerset
Goal:
α : Type u_1
l₁ l₂ l₁_1 l₂_1 l₃ : List α
h : l₁_1 ~ l₂_1
h_1 : l₂_1 ~ l₃
IH₁ : powersetAux' l₁_1 ~ powersetAux' l₂_1
IH₂ : powersetAux' l₂_1 ~ powersetAux' l₃
⊢ powersetAux' l₁_1 ~ powersetAux' l₃

Tactic:
exact IH₁.trans IH₂

Premises used: List.Perm.trans