awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : a ∈ l₁.keys (β := β)
nil :
  ∀ {l₂ : List (Sigma β)} (h : Membership.mem (γ := List α) (keys (β := β) []) a),
    dlookup (β := β) a (kunion (β := β) [] l₂) = dlookup (β := β) a []
cons :
  ∀ (s : Sigma β) (tail : List (Sigma β))
    (ih :
      ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
        dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail)
    {l₂ : List (Sigma β)} (h : a ∈ (s :: tail).keys (β := β)),
    dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) a (s :: tail)
⊢ dlookup (β := β) a (l₁.kunion (β := β) l₂) = dlookup (β := β) a l₁

Tactic:
induction l₁ generalizing l₂ with
  | nil => simp at h
  | cons s _ ih =>
    simp only [keys_cons, mem_cons] at h
    rcases h with rfl | h <;> obtain ⟨a'⟩ := s
    · simp
    · rw [kunion_cons]
      by_cases h' : a = a'
      · subst h'
        simp
      · simp [h', ih h]

Premises used: List.keys_cons, List.cons, List.kunion_cons, List.mem_cons, rfl, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₂ : List (Sigma β)
h : ¬Membership.mem (γ := List α) (keys (β := β) []) a
⊢ dlookup (β := β) a (kunion (β := β) [] l₂) = dlookup (β := β) a l₂

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
head : Sigma β
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : ¬a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a l₂
l₂ : List (Sigma β)
h : ¬a ∈ (head :: tail).keys (β := β)
⊢ dlookup (β := β) a ((head :: tail).kunion (β := β) l₂) = dlookup (β := β) a l₂

Tactic:
simp_all [not_or]

Premises used: not_or
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : ¬a ∈ l₁.keys (β := β)
nil :
  ∀ {l₂ : List (Sigma β)} (h : ¬Membership.mem (γ := List α) (keys (β := β) []) a),
    dlookup (β := β) a (kunion (β := β) [] l₂) = dlookup (β := β) a l₂
cons :
  ∀ (head : Sigma β) (tail : List (Sigma β))
    (ih :
      ∀ {l₂ : List (Sigma β)} (h : ¬a ∈ tail.keys (β := β)),
        dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a l₂)
    {l₂ : List (Sigma β)} (h : ¬a ∈ (head :: tail).keys (β := β)),
    dlookup (β := β) a ((head :: tail).kunion (β := β) l₂) = dlookup (β := β) a l₂
⊢ dlookup (β := β) a (l₁.kunion (β := β) l₂) = dlookup (β := β) a l₂

Tactic:
induction l₁ generalizing l₂ with
  | nil => simp
  | cons _ _ ih => simp_all [not_or]

Premises used: not_or, List.cons, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₂ : List (Sigma β)
⊢ b ∈ dlookup (β := β) a (kunion (β := β) [] l₂) ↔
    Membership.mem (γ := Option (β a)) (dlookup (β := β) a []) b ∨
      ¬Membership.mem (γ := List α) (keys (β := β) []) a ∧ b ∈ dlookup (β := β) a l₂

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Sigma β
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a (tail.kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a tail ∨ ¬a ∈ tail.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
l₂ : List (Sigma β)
cons :
  ∀ (a' : α) (snd : β a'),
    b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
        ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
⊢ b ∈ dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (s :: tail) ∨ ¬a ∈ (s :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂

Tactic:
obtain ⟨a'⟩ := s
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a (tail.kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a tail ∨ ¬a ∈ tail.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
l₂ : List (Sigma β)
a' : α
snd : β a'
pos :
  ∀ (h₁ : a = a'),
    b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
        ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
neg :
  ∀ (h₁ : ¬a = a'),
    b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
        ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
⊢ b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
      ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂

Tactic:
by_cases h₁ : a = a'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a (tail.kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a tail ∨ ¬a ∈ tail.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
l₂ : List (Sigma β)
a' : α
snd : β a'
h₁ : a = a'
pos :
  ∀ (snd : β a),
    b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a snd :: tail).kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a (Sigma.mk (β := β) a snd :: tail) ∨
        ¬a ∈ (Sigma.mk (β := β) a snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
⊢ b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
      ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂

Tactic:
subst h₁
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a (tail.kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a tail ∨ ¬a ∈ tail.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
l₂ : List (Sigma β)
snd : β a
⊢ b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a snd :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (Sigma.mk (β := β) a snd :: tail) ∨
      ¬a ∈ (Sigma.mk (β := β) a snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a (tail.kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a tail ∨ ¬a ∈ tail.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
l₂ : List (Sigma β)
a' : α
snd : β a'
h₁ : ¬a = a'
⊢ b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
      ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂

Tactic:
simp [h₁, @ih (kerase a' l₂)]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nil :
  ∀ {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a (kunion (β := β) [] l₂) ↔
      Membership.mem (γ := Option (β a)) (dlookup (β := β) a []) b ∨
        ¬Membership.mem (γ := List α) (keys (β := β) []) a ∧ b ∈ dlookup (β := β) a l₂
cons :
  ∀ (s : Sigma β) (tail : List (Sigma β))
    (ih :
      ∀ {l₂ : List (Sigma β)},
        b ∈ dlookup (β := β) a (tail.kunion (β := β) l₂) ↔
          b ∈ dlookup (β := β) a tail ∨ ¬a ∈ tail.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂)
    {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a (s :: tail) ∨ ¬a ∈ (s :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
⊢ b ∈ dlookup (β := β) a (l₁.kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a l₁ ∨ ¬a ∈ l₁.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂

Tactic:
induction l₁ generalizing l₂ with
  | nil => simp
  | cons s _ ih =>
    obtain ⟨a'⟩ := s
    by_cases h₁ : a = a'
    · subst h₁
      simp
    · simp [h₁, @ih (kerase a' l₂)]

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
⊢ dlookup (β := β) a (l₁.kunion (β := β) l₂) = some b ↔
    dlookup (β := β) a l₁ = some b ∨ ¬a ∈ l₁.keys (β := β) ∧ dlookup (β := β) a l₂ = some b

Tactic:
mem_dlookup_kunion

Premises used: List.mem_dlookup_kunion
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ l₃ : List (Sigma β)
h₁ : b ∈ dlookup (β := β) a (l₁.kunion (β := β) l₃)
h₂ : ¬a ∈ l₂.keys (β := β)
⊢ b ∈ dlookup (β := β) a ((l₁.kunion (β := β) l₂).kunion (β := β) l₃)

Tactic:
match mem_dlookup_kunion.mp h₁ with
  | Or.inl h => mem_dlookup_kunion.mpr (Or.inl (mem_dlookup_kunion.mpr (Or.inl h)))
  | Or.inr h => mem_dlookup_kunion.mpr <| Or.inr ⟨mt mem_keys_kunion.mp (not_or.mpr ⟨h.1, h₂⟩), h.2⟩

Premises used: Iff.mpr, List.kunion, List.mem_dlookup_kunion, Membership.mem, mt, List.mem_keys_kunion, not_or, And.right, And.left, And.intro, Iff.mp, Or.inl, List.dlookup, Or.inr, _private.0.List.mem_dlookup_kunion_middle.match_1
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
⊢ orderedInsert r a [] = [a]

Tactic:
.refl _

Premises used: List.orderedInsert, Eq.refl
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
⊢ orderedInsert r a (b :: l) = if r a b then a :: b :: l else b :: orderedInsert r a l

Tactic:
.refl _

Premises used: List.orderedInsert, Eq.refl
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
h : r a b
⊢ orderedInsert r a (b :: l) = a :: b :: l

Tactic:
dif_pos h

Premises used: dif_pos, List.orderedInsert, ite
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
h : ¬r a b
⊢ orderedInsert r a (b :: l) = b :: orderedInsert r a l

Tactic:
dif_neg h

Premises used: List.orderedInsert, dif_neg, ite
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
⊢ insertionSort r [] = []

Tactic:
.refl _

Premises used: Eq.refl, List.foldr, List.insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
⊢ insertionSort r (a :: l) = orderedInsert r a (insertionSort r l)

Tactic:
.refl _

Premises used: Eq.refl, List.foldr, List.insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
⊢ Eq (α := List ℕ) (insertionSort (fun (m n : ℕ) ↦ m / 10 ≤ n / 10) [5, 27, 221, 95, 17, 43, 7, 2, 98, 567, 23, 12])
    [5, 7, 2, 17, 12, 27, 23, 43, 95, 98, 221, 567]

Tactic:
rfl

Premises used: List.orderedInsert, List.foldr, rfl, List.insertionSort, ite
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
L : List α
a : α
nil : (orderedInsert r a []).length = length.{u_1} (α := α) [] + 1
cons :
  ∀ (head : α) (tail : List α),
    (orderedInsert r a tail).length = tail.length + 1 →
      (orderedInsert r a (head :: tail)).length = (head :: tail).length + 1
⊢ (orderedInsert r a L).length = L.length + 1

Tactic:
induction L
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
⊢ (orderedInsert r a []).length = length.{u_1} (α := α) [] + 1

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a head : α
tail : List α
tail_ih : (orderedInsert r a tail).length = tail.length + 1
⊢ (orderedInsert r a (head :: tail)).length = (head :: tail).length + 1

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
nil :
  orderedInsert r a [] = takeWhile (fun (b : α) ↦ decide ¬r a b) [] ++ a :: dropWhile (fun (b : α) ↦ decide ¬r a b) []
cons :
  ∀ (head : α) (tail : List α),
    orderedInsert r a tail =
        takeWhile (fun (b : α) ↦ decide ¬r a b) tail ++ a :: dropWhile (fun (b : α) ↦ decide ¬r a b) tail →
      orderedInsert r a (head :: tail) =
        takeWhile (fun (b : α) ↦ decide ¬r a b) (head :: tail) ++
          a :: dropWhile (fun (b : α) ↦ decide ¬r a b) (head :: tail)
⊢ orderedInsert r a l = takeWhile (fun (b : α) ↦ decide ¬r a b) l ++ a :: dropWhile (fun (b : α) ↦ decide ¬r a b) l

Tactic:
induction l
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
⊢ orderedInsert r a [] = takeWhile (fun (b : α) ↦ decide ¬r a b) [] ++ a :: dropWhile (fun (b : α) ↦ decide ¬r a b) []

Tactic:
grind [takeWhile, dropWhile]

Premises used: List.dropWhile, List.takeWhile
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a head : α
tail : List α
tail_ih :
  orderedInsert r a tail =
    takeWhile (fun (b : α) ↦ decide ¬r a b) tail ++ a :: dropWhile (fun (b : α) ↦ decide ¬r a b) tail
⊢ orderedInsert r a (head :: tail) =
    takeWhile (fun (b : α) ↦ decide ¬r a b) (head :: tail) ++
      a :: dropWhile (fun (b : α) ↦ decide ¬r a b) (head :: tail)

Tactic:
grind [takeWhile, dropWhile]

Premises used: List.dropWhile, List.takeWhile
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
⊢ insertionSort r (a :: l) =
    takeWhile (fun (b : α) ↦ decide ¬r a b) (insertionSort r l) ++
      a :: dropWhile (fun (b : α) ↦ decide ¬r a b) (insertionSort r l)

Tactic:
orderedInsert_eq_take_drop r a _

Premises used: List.orderedInsert_eq_take_drop, List.foldr, List.insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
nil : a ∈ orderedInsert r b [] ↔ a = b ∨ Membership.mem (γ := List α) [] a
cons :
  ∀ (head : α) (tail : List α),
    (a ∈ orderedInsert r b tail ↔ a = b ∨ a ∈ tail) → (a ∈ orderedInsert r b (head :: tail) ↔ a = b ∨ a ∈ head :: tail)
⊢ a ∈ orderedInsert r b l ↔ a = b ∨ a ∈ l

Tactic:
induction l
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
⊢ a ∈ orderedInsert r b [] ↔ a = b ∨ Membership.mem (γ := List α) [] a

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b head : α
tail : List α
tail_ih : a ∈ orderedInsert r b tail ↔ a = b ∨ a ∈ tail
⊢ a ∈ orderedInsert r b (head :: tail) ↔ a = b ∨ a ∈ head :: tail

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
l : List α
x : α
hl₁ : ∀ (a : α), a ∈ l → (r a x ↔ s (f a) (f x))
hl₂ : ∀ (a : α), a ∈ l → (r x a ↔ s (f x) (f a))
nil :
  ∀ (hl₁ : ∀ (a : α), Membership.mem (γ := List α) [] a → (r a x ↔ s (f a) (f x)))
    (hl₂ : ∀ (a : α), Membership.mem (γ := List α) [] a → (r x a ↔ s (f x) (f a))),
    map f (orderedInsert r x []) = orderedInsert s (f x) (map f [])
cons :
  ∀ (head : α) (tail : List α),
    (∀ (hl₁ : ∀ (a : α), a ∈ tail → (r a x ↔ s (f a) (f x))) (hl₂ : ∀ (a : α), a ∈ tail → (r x a ↔ s (f x) (f a))),
        map f (orderedInsert r x tail) = orderedInsert s (f x) (map f tail)) →
      ∀ (hl₁ : ∀ (a : α), a ∈ head :: tail → (r a x ↔ s (f a) (f x)))
        (hl₂ : ∀ (a : α), a ∈ head :: tail → (r x a ↔ s (f x) (f a))),
        map f (orderedInsert r x (head :: tail)) = orderedInsert s (f x) (map f (head :: tail))
⊢ map f (orderedInsert r x l) = orderedInsert s (f x) (map f l)

Tactic:
induction l
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
x : α
hl₁ : ∀ (a : α), Membership.mem (γ := List α) [] a → (r a x ↔ s (f a) (f x))
hl₂ : ∀ (a : α), Membership.mem (γ := List α) [] a → (r x a ↔ s (f x) (f a))
⊢ map f (orderedInsert r x []) = orderedInsert s (f x) (map f [])

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
x head : α
tail : List α
tail_ih :
  ∀ (hl₁ : ∀ (a : α), a ∈ tail → (r a x ↔ s (f a) (f x))) (hl₂ : ∀ (a : α), a ∈ tail → (r x a ↔ s (f x) (f a))),
    map f (orderedInsert r x tail) = orderedInsert s (f x) (map f tail)
hl₁ : ∀ (a : α), a ∈ head :: tail → (r a x ↔ s (f a) (f x))
hl₂ : ∀ (a : α), a ∈ head :: tail → (r x a ↔ s (f x) (f a))
⊢ map f (orderedInsert r x (head :: tail)) = orderedInsert s (f x) (map f (head :: tail))

Tactic:
grind
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
pos : ∀ (h : r a b), orderedInsert r a (b :: l) ~ a :: b :: l
neg : ∀ (h : ¬r a b), orderedInsert r a (b :: l) ~ a :: b :: l
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
by_cases h : a ≼ b
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
h : r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
simp [h]
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
h : ¬r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
simpa [h] using ((perm_orderedInsert a l).cons _).trans (Perm.swap _ _ _)

Premises used: List.Perm.cons, List.Perm.swap, List.Perm.trans
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
L : List α
a b : α
rw : (count a L + if (b == a) = true then 1 else 0) = count a L + if b = a then 1 else 0
⊢ count a (orderedInsert r b L) = count a L + if b = a then 1 else 0

Tactic:
rw [(L.perm_orderedInsert r b).count_eq, count_cons]

Premises used: List.perm_orderedInsert, List.count_cons, List.Perm.count_eq
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
L : List α
a b : α
⊢ (count a L + if (b == a) = true then 1 else 0) = count a L + if b = a then 1 else 0

Tactic:
simp
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
nil : insertionSort r [] ~ []
cons : ∀ (head : α) (tail : List α), insertionSort r tail ~ tail → insertionSort r (head :: tail) ~ head :: tail
⊢ insertionSort r l ~ l

Tactic:
induction l
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
⊢ insertionSort r [] ~ []

Tactic:
grind [List.Perm, perm_orderedInsert]

Premises used: List.perm_orderedInsert, List.Perm
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
head : α
tail : List α
tail_ih : insertionSort r tail ~ tail
⊢ insertionSort r (head :: tail) ~ head :: tail

Tactic:
grind [List.Perm, perm_orderedInsert]

Premises used: List.perm_orderedInsert, List.Perm
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
x : α
⊢ x ∈ insertionSort r l ↔ x ∈ l

Tactic:
(perm_insertionSort r l).mem_iff

Premises used: List.Perm.mem_iff, List.perm_insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
⊢ (insertionSort r l).length = l.length

Tactic:
(perm_insertionSort r _).length_eq

Premises used: List.Perm.length_eq, List.perm_insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
rw : orderedInsert r a (insertionSort r l) = a :: insertionSort r l
⊢ insertionSort r (a :: l) = a :: insertionSort r l

Tactic:
rw [insertionSort_cons]

Premises used: List.insertionSort_cons
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
hi : insertionSort r l = []
⊢ orderedInsert r a [] = [a]

Tactic:
rfl
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
cons : r a b
⊢ orderedInsert r a (b :: m) = a :: b :: m

Tactic:
rw [orderedInsert_cons_of_le]

Premises used: List.orderedInsert_cons_of_le
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
apply : b ∈ insertionSort r l
⊢ r a b

Tactic:
apply h b <| (mem_insertionSort r).1 _

Premises used: Iff.mp, List.mem_insertionSort
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
rw : b ∈ b :: m
⊢ b ∈ insertionSort r l

Tactic:
rw [hi]
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ b :: m

Tactic:
mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ b :: m

Tactic:
exact mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
cases : ∀ (x : List α) (hi : insertionSort r l = x), orderedInsert r a x = a :: x
⊢ orderedInsert r a (insertionSort r l) = a :: insertionSort r l

Tactic:
cases hi : insertionSort r l with
  | nil => rfl
  | cons b m =>
    rw [orderedInsert_cons_of_le]
    apply h b <| (mem_insertionSort r).1 _
    rw [hi]
    exact mem_cons_self

Premises used: List.orderedInsert_cons_of_le, List.cons, Iff.mp, List.mem_cons_self, List.insertionSort, List.mem_insertionSort, List.nil
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
hl :
  ∀ (a : α), Membership.mem (γ := List α) [] a → ∀ (b : α), Membership.mem (γ := List α) [] b → (r a b ↔ s (f a) (f b))
⊢ map f (insertionSort r []) = insertionSort s (map f [])

Tactic:
simp
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  ∀ (hl : ∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))),
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl : ∀ (a : α), a ∈ x :: xs → ∀ (b : α), b ∈ x :: xs → (r a b ↔ s (f a) (f b))
⊢ ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α) (x_2 : x_1 ∈ xs), r x_1 x ↔ s (f x_1) (f x)) ∧
      ∀ (x : α) (x_1 : x ∈ xs) (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))

Tactic:
simp_rw [List.forall_mem_cons, forall_and] at hl

Premises used: List.forall_mem_cons, forall_and
-- Module: Mathlib.Data.List.Sort
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  ∀ (hl : ∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))),
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α) (x_2 : x_1 ∈ xs), r x_1 x ↔ s (f x_1) (f x)) ∧
      ∀ (x : α) (x_1 : x ∈ xs) (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
cons : map f (orderedInsert r x (insertionSort r xs)) = orderedInsert s (f x) (insertionSort s (map f xs))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))

Tactic:
simp_rw [List.map, insertionSort_cons]

Premises used: List.map, List.insertionSort_cons