awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Range
Goal:
a : ℕ
m : Multiset ℕ
c : ℕ
left : c ∈ m
hxa : a + c < a
hxb : Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) (a + c)
⊢ False

Tactic:
(Nat.le_add_right _ _).not_gt hxa

Premises used: Nat.le_add_right, LE.le.not_gt
-- Module: Mathlib.Data.Multiset.Range
Goal:
a : ℕ
m : Multiset ℕ
c : ℕ
left : c ∈ m
hxa : a + c < a
hxb : Membership.mem (γ := Multiset ℕ) (map (fun (x : ℕ) ↦ a + x) m) (a + c)
⊢ False

Tactic:
exact (Nat.le_add_right _ _).not_gt hxa

Premises used: Nat.le_add_right, LE.le.not_gt
-- Module: Mathlib.Data.Multiset.Range
Goal:
a b : ℕ
rw : _root_.Disjoint (range a) (map (fun (x : ℕ) ↦ a + x) (range b))
⊢ range (a + b) = range a ∪ map (fun (x : ℕ) ↦ a + x) (range b)

Tactic:
rw [range_add, add_eq_union_iff_disjoint]

Premises used: Multiset.add_eq_union_iff_disjoint, Multiset.range_add
-- Module: Mathlib.Data.Multiset.Range
Goal:
a b : ℕ
⊢ _root_.Disjoint (range a) (map (fun (x : ℕ) ↦ a + x) (range b))

Tactic:
apply range_disjoint_map_add

Premises used: Multiset.range_disjoint_map_add
-- Module: Mathlib.Data.Multiset.Range
Goal:
n : ℕ
⊢ (range n).Nodup

Tactic:
List.nodup_range

Premises used: Multiset.Nodup, List.nodup_range
-- Module: Mathlib.Data.Multiset.Range
Goal:
m n : ℕ
⊢ range m ≤ range n ↔ m ≤ n

Tactic:
(le_iff_subset (nodup_range _)).trans range_subset

Premises used: Multiset.le_iff_subset, Multiset.range_subset, Iff.trans, Multiset.nodup_range
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
n : ℕ
a : α
⊢ (↑(List.replicate n a) : Multiset α) = replicate n a

Tactic:
rfl

Premises used: Multiset.replicate, rfl
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a : α
⊢ replicate 0 a = 0

Tactic:
rfl

Premises used: List.replicate, Multiset.zero, Multiset.ofList, Multiset.replicate, rfl
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a : α
n : ℕ
⊢ replicate (n + 1) a = a ::ₘ replicate n a

Tactic:
rfl

Premises used: List.replicate, Multiset.cons, rfl
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
m n : ℕ
a : α
⊢ replicate (m + n) a = replicate m a + replicate n a

Tactic:
congr_arg _ <| List.replicate_add ..

Premises used: Multiset.add, congr_arg, Multiset.ofList, Multiset.replicate, List.replicate_add
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a : α
⊢ replicate 1 a = {a}

Tactic:
rfl

Premises used: List.replicate, Multiset.cons, Multiset.ofList, Multiset.replicate, rfl
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
n : ℕ
a : α
⊢ (replicate n a).card = n

Tactic:
length_replicate

Premises used: List.length_replicate, Multiset.card
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a b : α
n : ℕ
⊢ b ∈ replicate n a ↔ n ≠ 0 ∧ b = a

Tactic:
List.mem_replicate

Premises used: Multiset.Mem, List.mem_replicate
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a b : α
n : ℕ
⊢ b ∈ replicate n a → b = a

Tactic:
List.eq_of_mem_replicate

Premises used: Multiset.Mem, List.eq_of_mem_replicate
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a : α
s : Multiset α
⊢ s = replicate s.card a ↔ ∀ (b : α), b ∈ s → b = a

Tactic:
Quot.inductionOn s fun _l => coe_eq_coe.trans <| perm_replicate.trans eq_replicate_length

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a : α
n : ℕ
s : Multiset α
⊢ s = replicate n a ↔ s.card = n ∧ ∀ (b : α), b ∈ s → b = a

Tactic:
⟨fun h => h.symm ▸ ⟨card_replicate _ _, fun _b => eq_of_mem_replicate⟩,
    fun ⟨e, al⟩ => e ▸ eq_replicate_of_mem al⟩

Premises used: Multiset.card_replicate, Multiset.eq_replicate_of_mem, Eq.rec, And.intro, Iff.intro, _private.0.Multiset.eq_replicate.match_1, Multiset.replicate, Multiset.eq_of_mem_replicate, Eq.symm, Eq
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
n : ℕ
hn : n ≠ 0
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) (replicate n)

Tactic:
fun _ _ h => (eq_replicate.1 h).2 _ <| mem_replicate.2 ⟨hn, rfl⟩

Premises used: Iff.mpr, Multiset.mem_replicate, And.right, Multiset.eq_replicate, And.intro, Iff.mp, Function.Injective, rfl
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a b : α
n : ℕ
h : n ≠ 0
⊢ replicate n a = replicate n b ↔ a = b

Tactic:
(replicate_right_injective h).eq_iff

Premises used: Function.Injective.eq_iff, Multiset.replicate_right_injective
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a : α
⊢ Injective.{1, u_1 + 1} (β := Multiset α) fun (x : ℕ) ↦ replicate x a

Tactic:
LeftInverse.injective (card_replicate · a)

Premises used: Function.LeftInverse.injective, Multiset.card_replicate
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
n : ℕ
a : α
⊢ replicate n a ⊆ {a}

Tactic:
List.replicate_subset_singleton n a

Premises used: List.Subset, List.replicate_subset_singleton, Multiset.Mem, Multiset.Subset
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a : α
n : ℕ
l : List α
⊢ replicate n a ≤ (↑l : Multiset α) ↔ List.replicate n a <+ l

Tactic:
⟨fun ⟨_l', p, s⟩ => perm_replicate.1 p ▸ s, Sublist.subperm⟩

Premises used: List.replicate, Eq.rec, Iff.intro, Iff.mp, List.Sublist, List.perm_replicate, List.Sublist.subperm, _private.0.Multiset.replicate_le_coe.match_1
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a : α
k n : ℕ
rw : replicate k a ≤ replicate n a ↔ replicate k a ≤ (↑(List.replicate n a) : Multiset α)
rw₁ rw₂ : replicate k a ≤ replicate n a ↔ replicate k a ≤ replicate n a
⊢ replicate k a ≤ replicate n a ↔ List.replicate k a <+ List.replicate n a

Tactic:
rw [← replicate_le_coe, coe_replicate]

Premises used: Multiset.coe_replicate, Multiset.replicate_le_coe
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
a : α
k n : ℕ
h : k ≤ n
⊢ replicate k a ≤ replicate n a

Tactic:
(replicate_le_replicate a).2 h

Premises used: Iff.mpr, Multiset.replicate_le_replicate
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
m : Multiset α
a : α
n : ℕ
⊢ m ≤ replicate n a ↔ ∃ (k : ℕ), k ≤ n ∧ m = replicate k a

Tactic:
⟨fun h => ⟨card m, (card_mono h).trans_eq (card_replicate _ _),
      eq_replicate_card.2 fun _ hb => eq_of_mem_replicate <| subset_of_le h hb⟩,
    fun ⟨_, hkn, hm⟩ => hm.symm ▸ (replicate_le_replicate _).2 hkn⟩

Premises used: Iff.mpr, Multiset.subset_of_le, LE.le.trans_eq, Multiset.card_replicate, Eq.rec, Multiset.replicate_le_replicate, LE.le, Multiset.card_mono, _private.0.Multiset.le_replicate_iff.match_1, And.intro, Iff.intro, Exists.intro, Multiset.card, Multiset.replicate, Multiset.eq_replicate_card, Multiset.eq_of_mem_replicate, Eq.symm
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
rw : (∃ (a : α), a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x
⊢ m < replicate (n + 1) x ↔ m ≤ replicate n x

Tactic:
rw [lt_iff_cons_le]

Premises used: Multiset.lt_iff_cons_le
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
mp : (∃ (a : α), a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x
mpr : m ≤ replicate n x → ∃ (a : α), a ::ₘ m ≤ replicate (n + 1) x
⊢ (∃ (a : α), a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x

Tactic:
constructor
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
⊢ x' = x

Tactic:
have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
this : x' = x
mp : ∀ (hx' : x ::ₘ m ≤ replicate (n + 1) x) (this : x' = x), m ≤ replicate n x
mp₁ : ∀ (hx' : x ::ₘ m ≤ x ::ₘ replicate n x) (this : x' = x), m ≤ replicate n x
mp₂ mp₃ mp₄ mp₅ : ∀ (hx' : m ≤ replicate n x) (this : x' = x), m ≤ replicate n x
⊢ m ≤ replicate n x

Tactic:
rwa [this, replicate_succ, cons_le_cons_iff] at hx'

Premises used: Multiset.replicate_succ, Multiset.cons_le_cons_iff
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ (a : α), a ::ₘ m ≤ x ::ₘ replicate n x

Tactic:
⟨x, cons_le_cons _ h⟩

Premises used: Exists.intro, Multiset.cons_le_cons
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ (a : α), a ::ₘ m ≤ x ::ₘ replicate n x

Tactic:
exact ⟨x, cons_le_cons _ h⟩
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
⊢ List.count a (List.replicate n a) = n

Tactic:
List.count_replicate_self (a := a)

Premises used: List.count_replicate_self
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
h : count a (replicate n a) = List.count a (List.replicate n a)
⊢ count a (replicate n a) = n

Tactic:
convert! List.count_replicate_self (a := a)

Premises used: List.count_replicate_self
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
h : count a (replicate n a) = count a (↑(List.replicate n a) : Multiset α)
h₁ h₂ : count a (replicate n a) = count a (replicate n a)
⊢ count a (replicate n a) = List.count a (List.replicate n a)

Tactic:
rw [← coe_count, coe_replicate]

Premises used: Multiset.coe_count, Multiset.coe_replicate
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
n : ℕ
⊢ List.count a (List.replicate n b) = if (b == a) = true then n else 0

Tactic:
List.count_replicate (a := a)

Premises used: List.count_replicate
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
n : ℕ
h : count a (replicate n b) = List.count a (List.replicate n b)
h₁ : b = a ↔ (b == a) = true
convert_1 : α
⊢ count a (replicate n b) = if b = a then n else 0

Tactic:
convert! List.count_replicate (a := a)

Premises used: List.count_replicate
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
n : ℕ
h : count a (replicate n b) = count a (↑(List.replicate n b) : Multiset α)
h₁ : count a (replicate n b) = count a (replicate n b)
h₂ : α
h₃ : count a (replicate n b) = count a (replicate n b)
h₄ : α
⊢ count a (replicate n b) = List.count a (List.replicate n b)

Tactic:
rw [← coe_count, coe_replicate]

Premises used: Multiset.coe_count, Multiset.coe_replicate
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
n : ℕ
⊢ b = a ↔ (b == a) = true

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
simp : n ≤ List.count a _l ↔ replicate n a ≤ (↑_l : Multiset α)
⊢ n ≤ count a (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) ↔
    replicate n a ≤ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l

Tactic:
simp only [quot_mk_to_coe'', coe_count]

Premises used: Multiset.coe_count, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ List.count a _l ↔ replicate n a ≤ (↑_l : Multiset α)

Tactic:
replicate_sublist_iff.symm.trans replicate_le_coe.symm

Premises used: List.replicate_sublist_iff, Iff.trans, Multiset.replicate_le_coe, Iff.symm
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ List.count a _l ↔ replicate n a ≤ (↑_l : Multiset α)

Tactic:
exact replicate_sublist_iff.symm.trans replicate_le_coe.symm

Premises used: List.replicate_sublist_iff, Iff.trans, Multiset.replicate_le_coe, Iff.symm
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
obtain : ∀ (b : α) (hb1 : b ∈ replicate n a) (hb2 : flip r x b), r a x
⊢ r a x

Tactic:
obtain ⟨b, hb1, hb2⟩ := exists_mem_of_rel_of_mem (rel_flip.2 h) hx

Premises used: Iff.mpr, Multiset.rel_flip, Multiset.exists_mem_of_rel_of_mem
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x b
rwa rwa₁ rwa₂ rwa₃ : ∀ (hb2 : flip r x a), r a x
⊢ r a x

Tactic:
rwa [eq_of_mem_replicate hb1] at hb2

Premises used: Multiset.eq_of_mem_replicate
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
⊢ Rel r m (replicate n a) ↔ m.card = n ∧ ∀ (x : α), x ∈ m → r x a

Tactic:
rel_flip.trans rel_replicate_left

Premises used: Multiset.rel_flip, Multiset.rel_replicate_left, Iff.trans
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
s : Multiset α
⊢ s.Nodup ↔ ∀ (a : α), ¬a ::ₘ a ::ₘ 0 ≤ s

Tactic:
Quot.induction_on s fun _ =>
    nodup_iff_sublist.trans <| forall_congr' fun a => not_congr (@replicate_le_coe _ a 2 _).symm

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ 0 + t
rwa : ∀ (s_eq : s = a ::ₘ (a ::ₘ 0 + t)), s = a ::ₘ a ::ₘ t
rwa₁ : ∀ (s_eq : s = a ::ₘ a ::ₘ (0 + t)), s = a ::ₘ a ::ₘ t
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (s_eq : s = a ::ₘ a ::ₘ t), s = a ::ₘ a ::ₘ t
⊢ s = a ::ₘ a ::ₘ t

Tactic:
rwa [cons_add, cons_add, Multiset.zero_add] at s_eq

Premises used: Multiset.cons_add, Multiset.zero_add
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_3
s : Multiset α
⊢ s.Nodup ↔ Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) s

Tactic:
Quotient.inductionOn s fun _ => (pairwise_coe_iff_pairwise fun _ _ => Ne.symm).symm

Premises used: Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.Replicate
Goal:
α : Type u_1
r : α → α → Prop
s : Multiset α
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ≠ b → r a b) → s.Nodup → Pairwise r s

Tactic:
Quotient.inductionOn s fun l h hl => ⟨l, rfl, hl.imp_of_mem fun {a b} ha hb => h a ha b hb⟩

Premises used: Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
s : Multiset (Multiset α)
a₀ a₁ : Multiset α
x pi : Multiset (Multiset α)
⊢ HEq (α := Multiset (Multiset α)) (a₀.bind fun (a : α) ↦ map (cons a) (a₁.bind fun (a : α) ↦ map (cons a) pi)) (β :=
    Multiset (Multiset α)) (a₁.bind fun (a : α) ↦ map (cons a) (a₀.bind fun (a : α) ↦ map (cons a) pi))

Tactic:
simp [map_bind, bind_bind a₀ a₁, cons_swap]

Premises used: Multiset.bind_bind, Multiset.cons_swap, Multiset.map_bind
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
⊢ Eq (α := Multiset (Multiset α)) (Sections 0) {0}

Tactic:
rfl

Premises used: Multiset.zero, Multiset.recOn, Multiset.ofList, Multiset.rec, Multiset.Sections, rfl
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
s : Multiset (Multiset α)
m : Multiset α
⊢ (m ::ₘ s).Sections = m.bind fun (a : α) ↦ map (cons a) s.Sections

Tactic:
recOn_cons m s

Premises used: Multiset.recOn_cons, Multiset.Sections
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
a : List α
l : List (List α)
rw :
  Eq (α := Multiset (Multiset α))
    (bind (↑(List.map (fun (l : List α) ↦ (↑l : Multiset α)) l.sections) : Multiset (Multiset α)) fun (b : Multiset α) ↦
      map (fun (a : α) ↦ a ::ₘ b) (↑a : Multiset α))
    (↑(List.map (fun (l : List α) ↦ (↑l : Multiset α))
          (List.flatMap (fun (s : List α) ↦ List.map (fun (a : α) ↦ a :: s) a) l.sections)) :
      Multiset (Multiset α))
⊢ (↑((↑a : Multiset α) :: List.map (fun (l : List α) ↦ (↑l : Multiset α)) l) : Multiset (Multiset α)).Sections =
    (↑(List.map (fun (l : List α) ↦ (↑l : Multiset α))
          (List.flatMap (fun (s : List α) ↦ List.map (fun (a : α) ↦ a :: s) a) l.sections)) :
      Multiset (Multiset α))

Tactic:
rw [← cons_coe, sections_cons, bind_map_comm, coe_sections l]

Premises used: Multiset.bind_map_comm, Multiset.sections_cons, Multiset.cons_coe
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
a : List α
l : List (List α)
⊢ Eq (α := Multiset (Multiset α))
    (bind (↑(List.map (fun (l : List α) ↦ (↑l : Multiset α)) l.sections) : Multiset (Multiset α)) fun (b : Multiset α) ↦
      map (fun (a : α) ↦ a ::ₘ b) (↑a : Multiset α))
    (↑(List.map (fun (l : List α) ↦ (↑l : Multiset α))
          (List.flatMap (fun (s : List α) ↦ List.map (fun (a : α) ↦ a :: s) a) l.sections)) :
      Multiset (Multiset α))

Tactic:
simp [Function.comp_def, List.flatMap]

Premises used: Function.comp_def, List.flatMap
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
s t : Multiset (Multiset α)
⊢ (0 + t).Sections = bind (Sections 0) fun (m : Multiset α) ↦ map (fun (x : Multiset α) ↦ m + x) t.Sections

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
s_1 t : Multiset (Multiset α)
a : Multiset α
s : Multiset (Multiset α)
ih : (s + t).Sections = s.Sections.bind fun (m : Multiset α) ↦ map (fun (x : Multiset α) ↦ m + x) t.Sections
⊢ (a ::ₘ s + t).Sections = (a ::ₘ s).Sections.bind fun (m : Multiset α) ↦ map (fun (x : Multiset α) ↦ m + x) t.Sections

Tactic:
simp [ih, bind_assoc, map_bind, bind_map]

Premises used: Multiset.map_bind, Multiset.bind_assoc, Multiset.bind_map
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
⊢ ∀ {a : Multiset α},
    Membership.mem (γ := Multiset (Multiset α)) (Sections 0) a ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) 0 a

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
a : Multiset α
s : Multiset (Multiset α)
ih : ∀ {a : Multiset α}, a ∈ s.Sections ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) s a
⊢ ∀ {a_1 : Multiset α}, a_1 ∈ (a ::ₘ s).Sections ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) (a ::ₘ s) a_1

Tactic:
simp [ih, rel_cons_left, eq_comm]

Premises used: Multiset.rel_cons_left, eq_comm
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
s : Multiset (Multiset α)
empty :
  ∀ {a : Multiset α},
    Membership.mem (γ := Multiset (Multiset α)) (Sections 0) a ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) 0 a
cons :
  ∀ (a : Multiset α) (s : Multiset (Multiset α))
    (ih : ∀ {a : Multiset α}, a ∈ s.Sections ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) s a) {a_1 : Multiset α},
    a_1 ∈ (a ::ₘ s).Sections ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) (a ::ₘ s) a_1
⊢ ∀ {a : Multiset α}, a ∈ s.Sections ↔ Rel (fun (s : Multiset α) (a : α) ↦ a ∈ s) s a

Tactic:
induction s using Multiset.induction_on with
  | empty => simp
  | cons _ _ ih => simp [ih, rel_cons_left, eq_comm]

Premises used: Multiset.rel_cons_left, Multiset.cons, eq_comm
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
s : Multiset (Multiset α)
⊢ card.{u_1} (α := Multiset α) (Sections 0) = (map.{0, u_1} (α := Multiset α) card 0).prod

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Sections
Goal:
α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ (a : Multiset α) (s : Multiset (Multiset α)),
    s.Sections.card = (map card s).prod → (a ::ₘ s).Sections.card = (map card (a ::ₘ s)).prod

Tactic:
simp +contextual
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
l : List α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ (↑l : Multiset α).sort r = l.mergeSort fun (x1 x2 : α) ↦ decide (r x1 x2)

Tactic:
rfl

Premises used: Multiset.sort, rfl
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ List.Pairwise r (s.sort r)

Tactic:
Quot.inductionOn s (pairwise_mergeSort' _)

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ (↑(s.sort r) : Multiset α) = s

Tactic:
Quot.inductionOn s fun _ => Quot.sound <| mergeSort_perm _ _

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ sort 0 r = []

Tactic:
List.mergeSort_nil

Premises used: List.mergeSort_nil, Multiset.sort
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
a : α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ sort {a} r = [a]

Tactic:
List.mergeSort_singleton a

Premises used: Multiset.sort, List.mergeSort_singleton
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
r' : β → β → Prop
inst_4 : DecidableRel r'
inst_5 : IsTrans β r'
inst_6 : Std.Antisymm r'
inst_7 : Std.Total r'
hs : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → (r a b ↔ r' (f a) (f b))
revert :
  ∀ (s : Multiset α) (hs : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → (r a b ↔ r' (f a) (f b))),
    List.map f (s.sort r) = (map f s).sort r'
⊢ List.map f (s.sort r) = (map f s).sort r'

Tactic:
revert s
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
β : Type u_2
f : α → β
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
r' : β → β → Prop
inst_4 : DecidableRel r'
inst_5 : IsTrans β r'
inst_6 : Std.Antisymm r'
inst_7 : Std.Total r'
l : List α
h :
  ∀ (a : α),
    Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) a →
      ∀ (b : α),
        Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) b →
          (r a b ↔ r' (f a) (f b))
⊢ ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → decide (r a b) = decide (r' (f a) (f b))

Tactic:
simpa using h
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
β : Type u_2
f : α → β
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
r' : β → β → Prop
inst_4 : DecidableRel r'
inst_5 : IsTrans β r'
inst_6 : Std.Antisymm r'
inst_7 : Std.Total r'
⊢ ∀ (s : Multiset α) (hs : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → (r a b ↔ r' (f a) (f b))),
    List.map f (s.sort r) = (map f s).sort r'

Tactic:
exact Quot.ind fun l h => map_mergeSort (l := l) (by simpa using h)

Premises used: Quot.ind
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ (∀ (b : α), b ∈ s → r a b) → (a ::ₘ s).sort r = a :: s.sort r

Tactic:
Quot.inductionOn s fun l => ?_

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
refine :
  ∀ (l : List α),
    (∀ (b : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) b → r a b) →
      (a ::ₘ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l).sort r =
        a :: sort (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) r
⊢ (∀ (b : α), b ∈ s → r a b) → (a ::ₘ s).sort r = a :: s.sort r

Tactic:
refine Quot.inductionOn s fun l => ?_
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
l : List α
⊢ (∀ (b : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) b → r a b) →
    (a ::ₘ Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l).sort r =
      a :: sort (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l) r

Tactic:
simpa [mergeSort_eq_insertionSort] using insertionSort_cons_of_forall_rel r (a := a) (l := l)

Premises used: List.insertionSort_cons_of_forall_rel, List.mergeSort_eq_insertionSort
-- Module: Mathlib.Data.Multiset.Sort
Goal:
n : ℕ
⊢ ((range n).sort fun (a b : ℕ) ↦ a ≤ b) = List.range n

Tactic:
List.mergeSort_eq_self _ (sortedLT_range n).sortedLE.pairwise

Premises used: List.mergeSort_eq_self, List.SortedLE.pairwise, Multiset.sort, List.SortedLT.sortedLE, List.sortedLT_range
-- Module: Mathlib.Data.Multiset.Sort
Goal:
α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
rw : a ∈ (↑(s.sort r) : Multiset α) ↔ a ∈ s
rw₁ rw₂ : a ∈ s ↔ a ∈ s
⊢ a ∈ s.sort r ↔ a ∈ s

Tactic:
rw [← mem_coe, sort_eq]

Premises used: Multiset.mem_coe, Multiset.sort_eq