awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rw₁ : List.map ofList (sublistsLen n l) ++ [] = 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]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
l : List α
s : Multiset α
⊢ ∀ (a : List α), ⟦a⟧ ∈ powersetCardAux n l ↔ ⟦a⟧ ≤ (↑l : Multiset α) ∧ card ⟦a⟧ = n
have simp : ∀ (a : List α),
  (∃ (a_1 : List α), (a_1 <+ l ∧ a_1.length = n) ∧ a_1 ~ a) ↔ (∃ (l_1 : List α), l_1 ~ a ∧ l_1 <+ l) ∧ a.length = n
Tactic: simp only [quot_mk_to_coe, powersetCardAux_eq_map_coe, List.mem_map, mem_sublistsLen,
      coe_eq_coe, coe_le, Subperm, coe_card]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux n l₁ ~ powersetCardAux n l₂
have succ : ∀ (n : ℕ) (IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂) {l₁ l₂ : List α}
  (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
Tactic: induction n generalizing l₁ l₂ with | zero => simp | succ n IHn => ?_
Cleared hypotheses: n, l₁, l₂, p
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
x : α
l₁_1 l₂_1 : List α
p : l₁_1 ~ l₂_1
IH : powersetCardAux (n + 1) l₁_1 ~ powersetCardAux (n + 1) l₂_1
⊢ powersetCardAux (n + 1) (x :: l₁_1) ~ powersetCardAux (n + 1) (x :: l₂_1)
have succ : powersetCardAux (n + 1) l₁_1 ++ List.map (cons x) (powersetCardAux n l₁_1) ~
  powersetCardAux (n + 1) l₂_1 ++ List.map (cons x) (powersetCardAux n l₂_1)
Tactic: simp only [powersetCardAux_cons]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l : List α
⊢ powersetCardAux (n + 1) (b :: a :: l) ~ powersetCardAux (n + 1) (a :: b :: l)
have succ : powersetCardAux (n + 1) l ++
    (List.map (cons a) (powersetCardAux n l) ++ List.map (cons b) (powersetCardAux n (a :: l))) ~
  powersetCardAux (n + 1) l ++
    (List.map (cons b) (powersetCardAux n l) ++ List.map (cons a) (powersetCardAux n (b :: l)))
Tactic: simp only [powersetCardAux_cons, append_assoc]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l : List α
⊢ powersetCardAux (n + 1) l ++
      (List.map (cons a) (powersetCardAux n l) ++ List.map (cons b) (powersetCardAux n (a :: l))) ~
    powersetCardAux (n + 1) l ++
      (List.map (cons b) (powersetCardAux n l) ++ List.map (cons a) (powersetCardAux n (b :: l)))
have succ : List.map (cons a) (powersetCardAux n l) ++ List.map (cons b) (powersetCardAux n (a :: l)) ~
  List.map (cons b) (powersetCardAux n l) ++ List.map (cons a) (powersetCardAux n (b :: l))
Tactic: apply Perm.append_left
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l : List α
⊢ List.map (cons a) (powersetCardAux n l) ++ List.map (cons b) (powersetCardAux n (a :: l)) ~
    List.map (cons b) (powersetCardAux n l) ++ List.map (cons a) (powersetCardAux n (b :: l))
have succ : ∀ (IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂),
  List.map (cons a) (powersetCardAux 0 l) ++ List.map (cons b) (powersetCardAux 0 (a :: l)) ~
    List.map (cons b) (powersetCardAux 0 l) ++ List.map (cons a) (powersetCardAux 0 (b :: l))
Tactic: cases n
Cleared hypotheses: n, IHn
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l : List α
succ :
  ∀ (IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂),
    List.map (cons a) (powersetCardAux 0 l) ++ List.map (cons b) (powersetCardAux 0 (a :: l)) ~
      List.map (cons b) (powersetCardAux 0 l) ++ List.map (cons a) (powersetCardAux 0 (b :: l))
⊢ List.map (cons a) (powersetCardAux n l) ++ List.map (cons b) (powersetCardAux n (a :: l)) ~
    List.map (cons b) (powersetCardAux n l) ++ List.map (cons a) (powersetCardAux n (b :: l))
have succ₁ : ∀ (n : ℕ) (IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂),
  List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons b) (powersetCardAux (n + 1) (a :: l)) ~
    List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons a) (powersetCardAux (n + 1) (b :: l))
Tactic: cases n
Cleared hypotheses: n, IHn
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons b) (powersetCardAux (n + 1) (a :: l)) ~
    List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons a) (powersetCardAux (n + 1) (b :: l))
have succ : List.map (cons a) (powersetCardAux (n + 1) l) ++
    (List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons b ∘ cons a) (powersetCardAux n l)) ~
  List.map (cons b) (powersetCardAux (n + 1) l) ++
    (List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons a ∘ cons b) (powersetCardAux n l))
Tactic: simp only [powersetCardAux_cons, map_append, List.map_map]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
a b : α
l : List α
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
⊢ 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 α
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n + 1) l) ++
      (List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons b ∘ cons a) (powersetCardAux n l)) ~
    List.map (cons b) (powersetCardAux (n + 1) l) ++
      (List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons a ∘ cons b) (powersetCardAux n l))
have succ : List.map (cons a) (powersetCardAux (n + 1) l) ++ List.map (cons b) (powersetCardAux (n + 1) l) ++
    List.map (cons a ∘ cons b) (powersetCardAux n l) ~
  List.map (cons b) (powersetCardAux (n + 1) l) ++ List.map (cons a) (powersetCardAux (n + 1) l) ++
    List.map (cons a ∘ cons b) (powersetCardAux n 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
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
have succ : Perm.{u_1} (α := Multiset α) (powersetCardAux (n + 1) []) (powersetCardAux (n + 1) [])
Tactic: induction p with
  | nil => rfl
  | cons _ p IH =>
    simp only [powersetCardAux_cons]
    exact IH.append ((IHn p).map _)
  | swap a b =>
    simp only [powersetCardAux_cons, append_assoc]
    apply Perm.append_left
    cases n
    · simp [Perm.swap]
    simp only [powersetCardAux_cons, map_append, List.map_map]
    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
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
p : l₁ ~ l₂
succ : Perm.{u_1} (α := Multiset α) (powersetCardAux (n + 1) []) (powersetCardAux (n + 1) [])
⊢ powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
have succ₁ : ∀ (x : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) (IH : powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂),
  powersetCardAux (n + 1) (x :: l₁) ~ powersetCardAux (n + 1) (x :: l₂)
Tactic: induction p with
  | nil => rfl
  | cons _ p IH =>
    simp only [powersetCardAux_cons]
    exact IH.append ((IHn p).map _)
  | swap a b =>
    simp only [powersetCardAux_cons, append_assoc]
    apply Perm.append_left
    cases n
    · simp [Perm.swap]
    simp only [powersetCardAux_cons, map_append, List.map_map]
    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
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
p : l₁ ~ l₂
succ : Perm.{u_1} (α := Multiset α) (powersetCardAux (n + 1) []) (powersetCardAux (n + 1) [])
succ₁ :
  ∀ (x : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) (IH : powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂),
    powersetCardAux (n + 1) (x :: l₁) ~ powersetCardAux (n + 1) (x :: l₂)
⊢ powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
have succ₂ : ∀ (a b : α) (l : List α), powersetCardAux (n + 1) (b :: a :: l) ~ powersetCardAux (n + 1) (a :: b :: l)
Tactic: induction p with
  | nil => rfl
  | cons _ p IH =>
    simp only [powersetCardAux_cons]
    exact IH.append ((IHn p).map _)
  | swap a b =>
    simp only [powersetCardAux_cons, append_assoc]
    apply Perm.append_left
    cases n
    · simp [Perm.swap]
    simp only [powersetCardAux_cons, map_append, List.map_map]
    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
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (p : l₁ ~ l₂), powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
p : l₁ ~ l₂
succ : Perm.{u_1} (α := Multiset α) (powersetCardAux (n + 1) []) (powersetCardAux (n + 1) [])
succ₁ :
  ∀ (x : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) (IH : powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂),
    powersetCardAux (n + 1) (x :: l₁) ~ powersetCardAux (n + 1) (x :: l₂)
succ₂ : ∀ (a b : α) (l : List α), powersetCardAux (n + 1) (b :: a :: l) ~ powersetCardAux (n + 1) (a :: b :: l)
⊢ powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂
have succ₃ : ∀ {l₁ l₂ l₃ : List α},
  l₁ ~ l₂ →
    l₂ ~ l₃ →
      ∀ (IH₁ : powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₂)
        (IH₂ : powersetCardAux (n + 1) l₂ ~ powersetCardAux (n + 1) l₃),
        powersetCardAux (n + 1) l₁ ~ powersetCardAux (n + 1) l₃
Tactic: induction p with
  | nil => rfl
  | cons _ p IH =>
    simp only [powersetCardAux_cons]
    exact IH.append ((IHn p).map _)
  | swap a b =>
    simp only [powersetCardAux_cons, append_assoc]
    apply Perm.append_left
    cases n
    · simp [Perm.swap]
    simp only [powersetCardAux_cons, map_append, List.map_map]
    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
n : ℕ
s : Multiset α
l : List α
⊢ powersetCard n ⟦l⟧ ≤ powerset ⟦l⟧
have simp : List.map ofList (sublistsLen n l) <+~ List.map ofList l.sublists'
Tactic: simp only [quot_mk_to_coe, powersetCard_coe, powerset_coe', coe_le]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
n : ℕ
s t : Multiset α
h_1 : s ≤ t
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ powersetCard n (↑l₁ : Multiset α) ≤ powersetCard n (↑l₂ : Multiset α)
have simp : List.map ofList (sublistsLen n l₁) <+~ List.map ofList (sublistsLen n l₂)
Tactic: simp only [powersetCard_coe, coe_le]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
s : Multiset α
⊢ powersetCard s.card s = {s}
have empty : Eq (α := Multiset (Multiset α)) (powersetCard (card.{u_1} (α := α) 0) 0) {0}
Tactic: induction s using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
s : Multiset α
empty : Eq (α := Multiset (Multiset α)) (powersetCard (card.{u_1} (α := α) 0) 0) {0}
⊢ powersetCard s.card s = {s}
have cons : ∀ (a : α) (s : Multiset α) (ih : powersetCard s.card s = {s}), powersetCard (a ::ₘ s).card (a ::ₘ s) = {a ::ₘ s}
Tactic: induction s using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
⊢ powersetCard n (map f 0) = map (map f) (powersetCard n 0)
have empty : powersetCard 0 (map f 0) = map (map f) (powersetCard 0 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
empty : powersetCard 0 (map f 0) = map (map f) (powersetCard 0 0)
⊢ powersetCard n (map f 0) = map (map f) (powersetCard n 0)
have empty₁ : ∀ (n : ℕ), powersetCard (n + 1) (map f 0) = map (map f) (powersetCard (n + 1) 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
n : ℕ
⊢ powersetCard n (map f (t ::ₘ s)) = map (map f) (powersetCard n (t ::ₘ s))
have cons : powersetCard 0 (map f (t ::ₘ s)) = map (map f) (powersetCard 0 (t ::ₘ s))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
n : ℕ
cons : powersetCard 0 (map f (t ::ₘ s)) = map (map f) (powersetCard 0 (t ::ₘ s))
⊢ powersetCard n (map f (t ::ₘ s)) = map (map f) (powersetCard n (t ::ₘ s))
have cons₁ : ∀ (n : ℕ), powersetCard (n + 1) (map f (t ::ₘ s)) = map (map f) (powersetCard (n + 1) (t ::ₘ s))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
s : Multiset α
⊢ powersetCard n (map f s) = map (map f) (powersetCard n s)
have empty : ∀ (n : ℕ), powersetCard n (map f 0) = map (map f) (powersetCard n 0)
Tactic: induction s using Multiset.induction generalizing n with
  | empty => cases n <;> simp [powersetCard_zero_left]
  | cons t s ih => cases n <;> simp [ih]
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
s : Multiset α
empty : ∀ (n : ℕ), powersetCard n (map f 0) = map (map f) (powersetCard n 0)
⊢ powersetCard n (map f s) = map (map f) (powersetCard n s)
have cons : ∀ (t : α) (s : Multiset α) (ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)) (n : ℕ),
  powersetCard n (map f (t ::ₘ s)) = map (map f) (powersetCard n (t ::ₘ s))
Tactic: induction s using Multiset.induction generalizing n with
  | empty => cases n <;> simp [powersetCard_zero_left]
  | cons t s ih => cases n <;> simp [ih]
Cleared hypotheses: n, s
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_2
S : Multiset α
⊢ ((range (S.card + 1)).bind fun (k : ℕ) ↦ powersetCard k S) = S.powerset
have h : ∀ (a : List α), ((range (card ⟦a⟧ + 1)).bind fun (k : ℕ) ↦ powersetCard k ⟦a⟧) = powerset ⟦a⟧
Tactic: induction S using Quotient.inductionOn
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_2
a : List α
⊢ ((range (card ⟦a⟧ + 1)).bind fun (k : ℕ) ↦ powersetCard k ⟦a⟧) = powerset ⟦a⟧
have h : (↑(List.map ofList (flatMap (fun (a_1 : ℕ) ↦ sublistsLen a_1 a) (List.range (a.length + 1)))) : Multiset (Multiset α)) =
  (↑(List.map ofList a.sublists') : Multiset (Multiset α))
Tactic: simp_rw [quot_mk_to_coe, powerset_coe', powersetCard_coe, ← coe_range, coe_bind,
    ← List.map_flatMap, coe_card]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ (powerset ⟦l⟧).Nodup
have simp : (List.map ofList l.sublists').Nodup
Tactic: simp only [quot_mk_to_coe, powerset_coe', coe_nodup]
-- Lean 4 proof step from Mathlib.Data.Multiset.Powerset (goal)
Goal:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ (List.map ofList l.sublists').Nodup
have refine : ∀ (x : List α), x ∈ l.sublists' → ∀ (y : List α), y ∈ l.sublists' → (↑x : Multiset α) = (↑y : Multiset α) → x = y
Tactic: refine (nodup_sublists'.2 h).map_on ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.Range (goal)
Goal:
n : ℕ
⊢ range n.succ = n ::ₘ range n
have rw : (↑(List.range n.succ) : Multiset ℕ) = n ::ₘ range n
Tactic: rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Range (goal)
Goal:
n : ℕ
rw : (↑(List.range n.succ) : Multiset ℕ) = n ::ₘ range n
⊢ range n.succ = n ::ₘ range n
have rw₁ : (↑(List.range n ++ [n]) : Multiset ℕ) = n ::ₘ range n
Tactic: rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Range (goal)
Goal:
n : ℕ
rw : (↑(List.range n.succ) : Multiset ℕ) = n ::ₘ range n
rw₁ : (↑(List.range n ++ [n]) : Multiset ℕ) = n ::ₘ range n
⊢ range n.succ = n ::ₘ range n
have rw₂ : (↑(List.range n) : Multiset ℕ) + (↑[n] : Multiset ℕ) = n ::ₘ range n
Tactic: rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Range (goal)
Goal:
n : ℕ
rw : (↑(List.range n.succ) : Multiset ℕ) = n ::ₘ range n
rw₁ : (↑(List.range n ++ [n]) : Multiset ℕ) = n ::ₘ range n
rw₂ : (↑(List.range n) : Multiset ℕ) + (↑[n] : Multiset ℕ) = n ::ₘ range n
⊢ range n.succ = n ::ₘ range n
have rw₃ : (↑[n] : Multiset ℕ) + (↑(List.range n) : Multiset ℕ) = n ::ₘ range n
Tactic: rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Range (goal)
Goal:
n : ℕ
rw : (↑(List.range n.succ) : Multiset ℕ) = n ::ₘ range n
rw₁ : (↑(List.range n ++ [n]) : Multiset ℕ) = n ::ₘ range n
rw₂ : (↑(List.range n) : Multiset ℕ) + (↑[n] : Multiset ℕ) = n ::ₘ range n
rw₃ : (↑[n] : Multiset ℕ) + (↑(List.range n) : Multiset ℕ) = n ::ₘ range n
⊢ range n.succ = n ::ₘ range n
have rw₄ : (↑[n] : Multiset ℕ) + (↑(List.range n) : Multiset ℕ) = n ::ₘ (↑(List.range n) : Multiset ℕ)
Tactic: rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Range (goal)
Goal:
n : ℕ
rw : (↑(List.range n.succ) : Multiset ℕ) = n ::ₘ range n
rw₁ : (↑(List.range n ++ [n]) : Multiset ℕ) = n ::ₘ range n
rw₂ : (↑(List.range n) : Multiset ℕ) + (↑[n] : Multiset ℕ) = n ::ₘ range n
rw₃ : (↑[n] : Multiset ℕ) + (↑(List.range n) : Multiset ℕ) = n ::ₘ range n
rw₄ : (↑[n] : Multiset ℕ) + (↑(List.range n) : Multiset ℕ) = n ::ₘ (↑(List.range n) : Multiset ℕ)
⊢ range n.succ = n ::ₘ range n
have rw₅ : {n} + (↑(List.range n) : Multiset ℕ) = n ::ₘ (↑(List.range n) : Multiset ℕ)
Tactic: rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Range (goal)
Goal:
n : ℕ
rw : (↑(List.range n.succ) : Multiset ℕ) = n ::ₘ range n
rw₁ : (↑(List.range n ++ [n]) : Multiset ℕ) = n ::ₘ range n
rw₂ : (↑(List.range n) : Multiset ℕ) + (↑[n] : Multiset ℕ) = n ::ₘ range n
rw₃ : (↑[n] : Multiset ℕ) + (↑(List.range n) : Multiset ℕ) = n ::ₘ range n
rw₄ : (↑[n] : Multiset ℕ) + (↑(List.range n) : Multiset ℕ) = n ::ₘ (↑(List.range n) : Multiset ℕ)
rw₅ : {n} + (↑(List.range n) : Multiset ℕ) = n ::ₘ (↑(List.range n) : Multiset ℕ)
⊢ range n.succ = n ::ₘ range n
have rw₆ : n ::ₘ (↑(List.range n) : Multiset ℕ) = n ::ₘ (↑(List.range n) : Multiset ℕ)
Tactic: rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Range (goal)
Goal:
a : ℕ
m : Multiset ℕ
⊢ _root_.Disjoint (range a) (map (fun (x : ℕ) ↦ a + x) m)
have rw : ∀ {a_1 : ℕ}, a_1 ∈ range a → ¬Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) a_1
Tactic: rw [disjoint_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.Range (hypothesis)
Goal:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
hxb : Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) x
⊢ False
have hxa₁ : x < a
Tactic: rw [range, mem_coe, List.mem_range] at hxa
Cleared hypotheses: hxa, hxb
-- Lean 4 proof step from Mathlib.Data.Multiset.Range (goal)
Goal:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x < a
hxb : Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) x
⊢ False
have obtain : ∀ (c : ℕ),
  c ∈ m → ∀ (hxa : a + c < a) (hxb : Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) (a + c)), False
Tactic: obtain ⟨c, _, rfl⟩ := mem_map.1 hxb
Cleared hypotheses: x, hxa, hxb
-- Lean 4 proof step from Mathlib.Data.Multiset.Range (goal)
Goal:
a b : ℕ
⊢ range (a + b) = range a ∪ map (fun (x : ℕ) ↦ a + x) (range b)
have rw : _root_.Disjoint (range a) (map (fun (x : ℕ) ↦ a + x) (range b))
Tactic: rw [range_add, add_eq_union_iff_disjoint]
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
a : α
k n : ℕ
⊢ replicate k a ≤ replicate n a ↔ List.replicate k a <+ List.replicate n a
have rw : replicate k a ≤ replicate n a ↔ replicate k a ≤ (↑(List.replicate n a) : Multiset α)
Tactic: rw [← replicate_le_coe, coe_replicate]
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
a : α
k n : ℕ
rw : replicate k a ≤ replicate n a ↔ replicate k a ≤ (↑(List.replicate n a) : Multiset α)
⊢ replicate k a ≤ replicate n a ↔ List.replicate k a <+ List.replicate n a
have rw₁ : replicate k a ≤ replicate n a ↔ replicate k a ≤ replicate n a
Tactic: rw [← replicate_le_coe, coe_replicate]
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m < replicate (n + 1) x ↔ m ≤ replicate n x
have rw : (∃ (a : α), a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x
Tactic: rw [lt_iff_cons_le]
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ (∃ (a : α), a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x
have mp : (∃ (a : α), a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
mp : (∃ (a : α), a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x
⊢ (∃ (a : α), a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x
have mpr : m ≤ replicate n x → ∃ (a : α), a ::ₘ m ≤ replicate (n + 1) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (hypothesis)
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
⊢ m ≤ replicate n x
have this : x' = x
Tactic: have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))
-- Lean 4 proof step from Mathlib.Data.Multiset.Replicate (goal)
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
this : x' = x
⊢ m ≤ replicate n x
have mp : ∀ (hx' : x ::ₘ m ≤ replicate (n + 1) x) (this : x' = x), m ≤ replicate n x
Tactic: rwa [this, replicate_succ, cons_le_cons_iff] at hx'
Cleared hypotheses: hx', this