awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : Pi.cons (δ := β) s a b₁ f a ⋯ = Pi.cons (δ := β) s a b₂ g a ⋯
⊢ b₁ = b₂
have rwa : ∀ (this : b₁ = Pi.cons (δ := β) s a b₂ g a sorry), b₁ = b₂
Tactic: rwa [Pi.cons_same, Pi.cons_same] at this
Cleared hypotheses: this
-- 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
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₂
⊢ b₁ = b₂
have rwa₁ : ∀ (this : b₁ = b₂), b₁ = b₂
Tactic: rwa [Pi.cons_same, Pi.cons_same] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → Membership.mem (γ := Multiset α) 0 a → β 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
have this : f = Pi.empty β
Tactic: have : f = Pi.empty β := funext (fun _ => funext fun h => (notMem_zero _ h).elim)
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
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 β
⊢ 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
have empty : ∀ (a : α) (h : Membership.mem (γ := Multiset α) 0 a), Pi.empty β a h ∈ t a
Tactic: simp only [this, pi_zero, mem_singleton, true_iff]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m → β a
⊢ f ∈ m.pi (β := β) t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
have 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
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 => ?_
Cleared hypotheses: m, f
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
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
have 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
Tactic: simp_rw [pi_cons, mem_bind, mem_map, ih]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
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
⊢ Pi.cons (δ := β) m a b f' a' ha' ∈ t a'
have pos : ∀ (h : a' = a), Pi.cons (δ := β) m a b f' a' ha' ∈ t a'
Tactic: by_cases h : a' = a
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
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'
⊢ Pi.cons (δ := β) m a b f' a' ha' ∈ t a'
have neg : ∀ (h : ¬a' = a), Pi.cons (δ := β) m a b f' a' ha' ∈ t a'
Tactic: by_cases h : a' = a
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
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
⊢ Pi.cons (δ := β) m a b f' a' ha' ∈ t a'
have pos : ∀ (b : β a') (hb : b ∈ t a') (ha' : a' ∈ a' ::ₘ m), Pi.cons (δ := β) m a' b f' a' ha' ∈ t a'
Tactic: subst h
Cleared hypotheses: a, b, hb, ha', h
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
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
⊢ Pi.cons (δ := β) m a b f' a' ha' ∈ t a'
have neg : f' a' sorry ∈ t a'
Tactic: rw [Pi.cons_ne _ h]
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
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
have cons : (Pi.cons (δ := β) m a (f a sorry) fun (a_1 : α) (ha : a_1 ∈ m) ↦ f a_1 sorry) = f
Tactic: refine ⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), ?_⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.Pi (goal)
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
⊢ (Pi.cons (δ := β) m a (f a ⋯) fun (a_1 : α) (ha : a_1 ∈ m) ↦ f a_1 ⋯) = f
have cons : f = f
Tactic: rw [Pi.cons_eta]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
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' (x :: l₁_1) ~ powersetAux' (x :: l₂_1)
have cons : powersetAux' l₁_1 ++ List.map (cons x) (powersetAux' l₁_1) ~ powersetAux' l₂_1 ++ List.map (cons x) (powersetAux' l₂_1)
Tactic: simp only [powersetAux'_cons]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
⊢ powersetAux' (b :: a :: l) ~ powersetAux' (a :: b :: l)
have 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)))
Tactic: simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
⊢ 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)))
have 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))
Tactic: apply Perm.append_left
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
⊢ cons b ∘ cons a = cons a ∘ cons b
have h : ∀ (s : Multiset α), (cons b ∘ cons a) s = (cons a ∘ cons b) s
Tactic: funext s
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
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 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))
have 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)
Tactic: rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetAux' l₁ ~ powersetAux' l₂
have nil : Perm.{u_1} (α := Multiset α) (powersetAux' []) (powersetAux' [])
Tactic: induction p with
  | nil => simp
  | cons _ _ IH =>
    simp only [powersetAux'_cons]
    exact IH.append (IH.map _)
  | swap a b =>
    simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]
    apply Perm.append_left
    rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
    exact perm_append_comm.append_right _
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
nil : Perm.{u_1} (α := Multiset α) (powersetAux' []) (powersetAux' [])
⊢ powersetAux' l₁ ~ powersetAux' l₂
have cons : ∀ (x : α) {l₁ l₂ : List α},
  l₁ ~ l₂ → ∀ (IH : powersetAux' l₁ ~ powersetAux' l₂), powersetAux' (x :: l₁) ~ powersetAux' (x :: l₂)
Tactic: induction p with
  | nil => simp
  | cons _ _ IH =>
    simp only [powersetAux'_cons]
    exact IH.append (IH.map _)
  | swap a b =>
    simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]
    apply Perm.append_left
    rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
    exact perm_append_comm.append_right _
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
nil : Perm.{u_1} (α := Multiset α) (powersetAux' []) (powersetAux' [])
cons :
  ∀ (x : α) {l₁ l₂ : List α},
    l₁ ~ l₂ → ∀ (IH : powersetAux' l₁ ~ powersetAux' l₂), powersetAux' (x :: l₁) ~ powersetAux' (x :: l₂)
⊢ powersetAux' l₁ ~ powersetAux' l₂
have swap : ∀ (a b : α) (l : List α), powersetAux' (b :: a :: l) ~ powersetAux' (a :: b :: l)
Tactic: induction p with
  | nil => simp
  | cons _ _ IH =>
    simp only [powersetAux'_cons]
    exact IH.append (IH.map _)
  | swap a b =>
    simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]
    apply Perm.append_left
    rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
    exact perm_append_comm.append_right _
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
nil : Perm.{u_1} (α := Multiset α) (powersetAux' []) (powersetAux' [])
cons :
  ∀ (x : α) {l₁ l₂ : List α},
    l₁ ~ l₂ → ∀ (IH : powersetAux' l₁ ~ powersetAux' l₂), powersetAux' (x :: l₁) ~ powersetAux' (x :: l₂)
swap : ∀ (a b : α) (l : List α), powersetAux' (b :: a :: l) ~ powersetAux' (a :: b :: l)
⊢ powersetAux' l₁ ~ powersetAux' l₂
have trans : ∀ {l₁ l₂ l₃ : List α},
  l₁ ~ l₂ →
    l₂ ~ l₃ →
      ∀ (IH₁ : powersetAux' l₁ ~ powersetAux' l₂) (IH₂ : powersetAux' l₂ ~ powersetAux' l₃),
        powersetAux' l₁ ~ powersetAux' l₃
Tactic: induction p with
  | nil => simp
  | cons _ _ IH =>
    simp only [powersetAux'_cons]
    exact IH.append (IH.map _)
  | swap a b =>
    simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]
    apply Perm.append_left
    rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
    exact perm_append_comm.append_right _
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
s : Multiset α
l : List α
⊢ List.map (ofList ∘ pure) l <+~ List.map ofList l.sublists
have rw : List.map ofList (List.map pure l) <+~ List.map ofList l.sublists
Tactic: rw [← List.map_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (hypothesis)
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux l).revzip
⊢ x.1 + x.2 = (↑l : Multiset α)
have h₁ : ∃ (a : List α × List α), a ∈ l.sublists.revzip ∧ Prod.map ofList ofList a = x
Tactic: rw [revzip, powersetAux_eq_map_coe, ← map_reverse, zip_map, ← revzip, List.mem_map] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (hypothesis)
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ (a : List α × List α), a ∈ l.sublists.revzip ∧ Prod.map ofList ofList a = x
⊢ x.1 + x.2 = (↑l : Multiset α)
have h₁ : ∃ (a : List α), ∃ (b : List α), (a, b) ∈ l.sublists.revzip ∧ ((↑a : Multiset α), (↑b : Multiset α)) = x
Tactic: simp only [Prod.map_apply, Prod.exists] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ (a : List α), ∃ (b : List α), (a, b) ∈ l.sublists.revzip ∧ ((↑a : Multiset α), (↑b : Multiset α)) = x
⊢ x.1 + x.2 = (↑l : Multiset α)
have rcases : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists.revzip),
  ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).1 + ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).2 = (↑l : Multiset α)
Tactic: rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (hypothesis)
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux' l).revzip
⊢ x.1 + x.2 = (↑l : Multiset α)
have h₁ : ∃ (a : List α × List α), a ∈ l.sublists'.revzip ∧ Prod.map ofList ofList a = x
Tactic: rw [revzip, powersetAux', ← map_reverse, zip_map, ← revzip, List.mem_map] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (hypothesis)
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ (a : List α × List α), a ∈ l.sublists'.revzip ∧ Prod.map ofList ofList a = x
⊢ x.1 + x.2 = (↑l : Multiset α)
have h₁ : ∃ (a : List α), ∃ (b : List α), (a, b) ∈ l.sublists'.revzip ∧ ((↑a : Multiset α), (↑b : Multiset α)) = x
Tactic: simp only [Prod.map_apply, Prod.exists] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ (a : List α), ∃ (b : List α), (a, b) ∈ l.sublists'.revzip ∧ ((↑a : Multiset α), (↑b : Multiset α)) = x
⊢ x.1 + x.2 = (↑l : Multiset α)
have rcases : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.revzip),
  ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).1 + ((↑l₁ : Multiset α), (↑l₂ : Multiset α)).2 = (↑l : Multiset α)
Tactic: rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
⊢ Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) ↦ p = (s, (↑l : Multiset α) - s)) l'.revzip
    (List.map Prod.fst l'.revzip)
have rw : ∀ (x : Multiset α × Multiset α), x ∈ l'.revzip → x = (x.1, (↑l : Multiset α) - x.1)
Tactic: rw [forall₂_map_right_iff, forall₂_same]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
s t : Multiset α
h : (s, t) ∈ l'.revzip
⊢ (s, t) = ((s, t).1, (↑l : Multiset α) - (s, t).1)
have dsimp : (s, t) = (s, (↑l : Multiset α) - s)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
s t : Multiset α
h : (s, t) ∈ l'.revzip
⊢ (s, t) = (s, (↑l : Multiset α) - s)
have rw : (s, t) = (s, (s, t).1 + (s, t).2 - s)
Tactic: rw [← H h, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
s t : Multiset α
h : (s, t) ∈ l'.revzip
rw : (s, t) = (s, (s, t).1 + (s, t).2 - s)
⊢ (s, t) = (s, (↑l : Multiset α) - s)
have rw₁ : (s, t) = (s, (s, t).2)
Tactic: rw [← H h, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
⊢ l'.revzip = List.map (fun (x : Multiset α) ↦ (x, (↑l : Multiset α) - x)) l'
have this : Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) ↦ p = (s, (↑l : Multiset α) - s)) l'.revzip
  (List.map Prod.fst l'.revzip)
Tactic: have :
    Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) => p = (s, ↑l - s)) (revzip l')
      ((revzip l').map Prod.fst) := by
    rw [forall₂_map_right_iff, forall₂_same]
    rintro ⟨s, t⟩ h
    dsimp
    rw [← H h, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = (↑l : Multiset α)
this :
  Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) ↦ p = (s, (↑l : Multiset α) - s)) l'.revzip
    (List.map Prod.fst l'.revzip)
⊢ l'.revzip = List.map (fun (x : Multiset α) ↦ (x, (↑l : Multiset α) - x)) l'
have rw : Forall₂ (fun (a : Multiset α × Multiset α) (c : Multiset α) ↦ a = (c, (↑l : Multiset α) - c)) l'.revzip l'
Tactic: rw [← forall₂_eq_eq_eq, forall₂_map_right_iff]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l : List α
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip
have haveI : ∀ (this : DecidableEq α), (powersetAux l).revzip ~ (powersetAux' l).revzip
Tactic: haveI := Classical.decEq α
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l : List α
this : DecidableEq α
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip
have rw : Perm (α := Multiset α × Multiset α) (List.map (fun (x : Multiset α) ↦ (x, (↑l : Multiset α) - x)) (powersetAux l))
  (List.map (fun (x : Multiset α) ↦ (x, (↑l : Multiset α) - x)) (powersetAux' l))
Tactic: rw [revzip_powersetAux_lemma l revzip_powersetAux, revzip_powersetAux_lemma l revzip_powersetAux']
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip
have haveI : ∀ (this : DecidableEq α), (powersetAux l₁).revzip ~ (powersetAux l₂).revzip
Tactic: haveI := Classical.decEq α
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip
have simp : Perm (α := Multiset α × Multiset α) (List.map (fun (x : Multiset α) ↦ (x, (↑l₂ : Multiset α) - x)) (powersetAux l₁))
  (List.map (fun (x : Multiset α) ↦ (x, (↑l₂ : Multiset α) - x)) (powersetAux l₂))
Tactic: simp only [fun l : List α => revzip_powersetAux_lemma l revzip_powersetAux, coe_eq_coe.2 p]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁ l₂ : List α
hsub : l₁ <+ l₂
⊢ (↑l₁ : Multiset α).powerset ≤ (↑l₂ : Multiset α).powerset
have rw : List.map ofList l₁.sublists' <+~ List.map ofList l₂.sublists'
Tactic: rw [powerset_coe', powerset_coe', coe_le]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁ l₂ : List α
hsub : l₁ <+ l₂
⊢ List.map ofList l₁.sublists' <+~ List.map ofList l₂.sublists'
have s₁ : List.map ofList l₁.sublists' <+ List.map ofList l₂.sublists'
Tactic: apply Sublist.subperm
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁ l₂ : List α
hsub : l₁ <+ l₂
⊢ List.map ofList l₁.sublists' <+ List.map ofList l₂.sublists'
have s₁ : l₁.sublists' <+ l₂.sublists'
Tactic: apply Sublist.map
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
l : List α
⊢ powersetCardAux n l = List.map ofList (sublistsLen n l)
have rw : sublistsLenAux n l ofList [] = List.map ofList (sublistsLen n l)
Tactic: rw [powersetCardAux, sublistsLenAux_eq, append_nil]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
l : List α
rw : sublistsLenAux n l ofList [] = List.map ofList (sublistsLen n l)
⊢ powersetCardAux n l = List.map ofList (sublistsLen n l)
have rw₁ : List.map ofList (sublistsLen n l) ++ [] = List.map ofList (sublistsLen n l)
Tactic: rw [powersetCardAux, sublistsLenAux_eq, append_nil]