awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
refine_1 : ∀ (h : r a b ∨ a = b ∧ Lex r l₁ l₂), Lex r (a :: l₁) (b :: l₂)
refine_2 : ∀ (h : Lex r (a :: l₁) (b :: l₂)), r a b ∨ a = b ∧ Lex r l₁ l₂
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))

Tactic:
refine decidable_of_iff (r a b ∨ a = b ∧ Lex r l₁ l₂) ⟨fun h => ?_, fun h => ?_⟩

Premises used: decidable_of_iff, And, Iff.intro, Or, Eq, List.Lex
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b ∨ a = b ∧ Lex r l₁ l₂
refine_1 : ∀ (h : r a b), Lex r (a :: l₁) (b :: l₂)
refine_1₁ : ∀ (h : Lex r l₁ l₂), Lex r (a :: l₁) (a :: l₂)
⊢ Lex r (a :: l₁) (b :: l₂)

Tactic:
rcases h with (h | ⟨rfl, h⟩)

Premises used: rfl
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ Lex r (a :: l₁) (b :: l₂)

Tactic:
Lex.rel h

Premises used: List.Lex.rel
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ Lex r (a :: l₁) (b :: l₂)

Tactic:
exact Lex.rel h

Premises used: List.Lex.rel
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ Lex r (a :: l₁) (a :: l₂)

Tactic:
Lex.cons h

Premises used: List.Lex.cons
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ Lex r (a :: l₁) (a :: l₂)

Tactic:
exact Lex.cons h

Premises used: List.Lex.cons
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r (a :: l₁) (b :: l₂)
refine_2 : ∀ (h : r a b), r a b ∨ a = b ∧ Lex r l₁ l₂
refine_2₁ : ∀ (h : Lex r l₁ l₂), r a a ∨ a = a ∧ Lex r l₁ l₂
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂

Tactic:
rcases h with (_ | h | h)
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂

Tactic:
Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂

Tactic:
exact Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ r a a ∨ a = a ∧ Lex r l₁ l₂

Tactic:
Or.inr ⟨rfl, h⟩

Premises used: And.intro, Or.inr, rfl
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ r a a ∨ a = a ∧ Lex r l₁ l₂

Tactic:
exact Or.inr ⟨rfl, h⟩

Premises used: Or.inr
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
h : l₁ ≠ l₂
nil : ∀ {l₂ : List α} (H : length.{u} (α := α) [] ≤ l₂.length) (h : [] ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] l₂
cons :
  ∀ (head : α) (tail : List α),
    (∀ {l₂ : List α} (H : tail.length ≤ l₂.length) (h : tail ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) tail l₂) →
      ∀ {l₂ : List α} (H : (head :: tail).length ≤ l₂.length) (h : head :: tail ≠ l₂),
        Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) l₂
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂

Tactic:
induction l₁ generalizing l₂
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
l₂ : List α
H : length.{u} (α := α) [] ≤ l₂.length
h : [] ≠ l₂
nil :
  ∀ (H : length.{u} (α := α) [] ≤ length.{u} (α := α) []) (h : Ne.{u + 1} (α := List α) [] []),
    Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] []
nil₁ :
  ∀ (b : α) (l₂ : List α) (H : length.{u} (α := α) [] ≤ (b :: l₂).length) (h : [] ≠ b :: l₂),
    Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] (b :: l₂)
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] l₂

Tactic:
rcases l₂ with - | ⟨b, l₂⟩
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
head : α
tail : List α
tail_ih : ∀ {l₂ : List α} (H : tail.length ≤ l₂.length) (h : tail ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) tail l₂
l₂ : List α
H : (head :: tail).length ≤ l₂.length
h : head :: tail ≠ l₂
cons :
  ∀ (H : (head :: tail).length ≤ length.{u} (α := α) []) (h : head :: tail ≠ []),
    Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) []
cons₁ :
  ∀ (b : α) (l₂ : List α) (H : (head :: tail).length ≤ (b :: l₂).length) (h : head :: tail ≠ b :: l₂),
    Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) (b :: l₂)
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) l₂

Tactic:
rcases l₂ with - | ⟨b, l₂⟩
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
H : length.{u} (α := α) [] ≤ length.{u} (α := α) []
h : Ne.{u + 1} (α := List α) [] []
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] []

Tactic:
contradiction
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
b : α
l₂ : List α
H : length.{u} (α := α) [] ≤ (b :: l₂).length
h : [] ≠ b :: l₂
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] (b :: l₂)

Tactic:
apply nil

Premises used: List.Lex.nil
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
head : α
tail : List α
tail_ih : ∀ {l₂ : List α} (H : tail.length ≤ l₂.length) (h : tail ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) tail l₂
H : (head :: tail).length ≤ length.{u} (α := α) []
h : head :: tail ≠ []
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) []

Tactic:
(not_lt_of_ge H).elim (succ_pos _)

Premises used: Not.elim, Nat.succ_pos, not_lt_of_ge
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
head : α
tail : List α
tail_ih : ∀ {l₂ : List α} (H : tail.length ≤ l₂.length) (h : tail ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) tail l₂
H : (head :: tail).length ≤ length.{u} (α := α) []
h : head :: tail ≠ []
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) []

Tactic:
exact (not_lt_of_ge H).elim (succ_pos _)

Premises used: Not.elim, Nat.succ_pos, not_lt_of_ge
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α} (H : l₁.length ≤ l₂.length) (h : l₁ ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
pos : ∀ (ab : a = b), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)
neg : ∀ (ab : ¬a = b), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
by_cases ab : a = b
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α} (H : l₁.length ≤ l₂.length) (h : l₁ ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : a = b
pos :
  ∀ (H : (a :: l₁).length ≤ (a :: l₂).length) (h : a :: l₁ ≠ a :: l₂),
    Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (a :: l₂)
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
subst b
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α} (H : l₁.length ≤ l₂.length) (h : l₁ ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂
l₂ : List α
H : (a :: l₁).length ≤ (a :: l₂).length
h : a :: l₁ ≠ a :: l₂
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (a :: l₂)

Tactic:
.cons <| IH (le_of_succ_le_succ H) (mt (congr_arg _) h)

Premises used: mt, congr_arg, Nat.le_of_succ_le_succ, List.Lex.cons
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α} (H : l₁.length ≤ l₂.length) (h : l₁ ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂
l₂ : List α
H : (a :: l₁).length ≤ (a :: l₂).length
h : a :: l₁ ≠ a :: l₂
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (a :: l₂)

Tactic:
exact .cons <| IH (le_of_succ_le_succ H) (mt (congr_arg _) h)

Premises used: mt, congr_arg, Nat.le_of_succ_le_succ
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α} (H : l₁.length ≤ l₂.length) (h : l₁ ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
.rel ab

Premises used: List.Lex.rel
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α} (H : l₁.length ≤ l₂.length) (h : l₁ ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)

Tactic:
exact .rel ab
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂

Tactic:
Decidable.List.Lex.ne_iff H

Premises used: Decidable.List.Lex.ne_iff
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂

Tactic:
exact Decidable.List.Lex.ne_iff H

Premises used: Decidable.List.Lex.ne_iff
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂

Tactic:
classical
  exact Decidable.List.Lex.ne_iff H
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : LT α
l l' : List α
rw rw₁ : Lex (fun (x1 x2 : α) ↦ x1 < x2) l l' ↔ Lex (fun (x1 x2 : α) ↦ x1 < x2) l l'
⊢ l.lt l' ↔ Lex (fun (x1 x2 : α) ↦ x1 < x2) l l'

Tactic:
rw [List.lt]

Premises used: List.lt
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : Preorder α
a a' : α
l l' : List α
h : a' :: l' < a :: l
⊢ a' ≤ a

Tactic:
match h with
  | .cons _ => le_rfl
  | .rel h => h.le

Premises used: le_rfl, LT.lt.le, LE.le, _private.0.List.head_le_of_lt.match_1
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : Preorder α
inst_1 : Inhabited α
l l' : List α
h : l' < l
hl' : l' ≠ []
⊢ Lex (fun (x1 x2 : α) ↦ x1 < x2) l' l

Tactic:
replace h : List.Lex (· < ·) l' l := h
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : Preorder α
inst_1 : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun (x1 x2 : α) ↦ x1 < x2) l' l
pos : ∀ (hl : l = []), l'.head! ≤ l.head!
neg : ∀ (hl : ¬l = []), l'.head! ≤ l.head!
⊢ l'.head! ≤ l.head!

Tactic:
by_cases hl : l = []
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : Preorder α
inst_1 : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun (x1 x2 : α) ↦ x1 < x2) l' l
hl : l = []
⊢ l'.head! ≤ l.head!

Tactic:
simp [hl] at h
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : Preorder α
inst_1 : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun (x1 x2 : α) ↦ x1 < x2) l' l
hl : ¬l = []
⊢ Lex (fun (x1 x2 : α) ↦ x1 < x2) (l'.head! :: l'.tail) (l.head! :: l.tail)

Tactic:
rw [← List.cons_head!_tail hl', ← List.cons_head!_tail hl] at h

Premises used: List.cons_head!_tail
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : Preorder α
inst_1 : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun (x1 x2 : α) ↦ x1 < x2) l' l
hl : ¬l = []
h₁ : Lex (fun (x1 x2 : α) ↦ x1 < x2) (l'.head! :: l'.tail) (l.head! :: l.tail)
⊢ ¬l = []

Tactic:
rw [← List.cons_head!_tail hl', ← List.cons_head!_tail hl] at h

Premises used: List.cons_head!_tail
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : Preorder α
inst_1 : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun (x1 x2 : α) ↦ x1 < x2) (l'.head! :: l'.tail) (l.head! :: l.tail)
hl : ¬l = []
⊢ l'.head! ≤ l.head!

Tactic:
head_le_of_lt h

Premises used: List.head_le_of_lt
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : Preorder α
inst_1 : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun (x1 x2 : α) ↦ x1 < x2) (l'.head! :: l'.tail) (l.head! :: l.tail)
hl : ¬l = []
⊢ l'.head! ≤ l.head!

Tactic:
exact head_le_of_lt h

Premises used: List.head_le_of_lt
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : LinearOrder α
a : α
l l' : List α
h : l' ≤ l
rw : ∀ (h : l' < l ∨ l' = l), a :: l' < a :: l ∨ a :: l' = a :: l
⊢ a :: l' ≤ a :: l

Tactic:
rw [le_iff_lt_or_eq] at h ⊢

Premises used: le_iff_lt_or_eq
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : LinearOrder α
a : α
l l' : List α
h : l' < l ∨ l' = l
⊢ a :: l' < a :: l ∨ a :: l' = a :: l

Tactic:
h.imp .cons (congr_arg _)

Premises used: congr_arg, Or.imp, List.Lex.cons
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : LinearOrder α
a : α
l l' : List α
h : l' < l ∨ l' = l
⊢ a :: l' < a :: l ∨ a :: l' = a :: l

Tactic:
exact h.imp .cons (congr_arg _)

Premises used: congr_arg, Or.imp
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
acc : Array α
⊢ go f [] acc = acc.toListAppend (lookmap f [])

Tactic:
simp [go, lookmap]

Premises used: List.lookmap, List.lookmap.go
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
cons :
  (match (motive := Option α → List α) f hd with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match (motive := Option α → List α) f hd with
      | some b => Array.toListAppend #[] (b :: tl)
      | none => go f tl (Array.push #[] hd))
⊢ go f (hd :: tl) acc = acc.toListAppend (lookmap f (hd :: tl))

Tactic:
rw [lookmap, go, go]

Premises used: List.lookmap, List.lookmap.go
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
cons : acc.toList ++ ([hd] ++ lookmap f tl) = acc.toList ++ ([] ++ ([hd] ++ lookmap f tl))
⊢ (match (motive := Option α → List α) none with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match (motive := Option α → List α) none with
      | some b => Array.toListAppend #[] (b :: tl)
      | none => go f tl (Array.push #[] hd))

Tactic:
simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.toList_push]

Premises used: Array.toList_push, Array.toListAppend_eq, List.append_assoc
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ acc.toList ++ ([hd] ++ lookmap f tl) = acc.toList ++ ([] ++ ([hd] ++ lookmap f tl))

Tactic:
rfl
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
a : α
⊢ (match (motive := Option α → List α) some a with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match (motive := Option α → List α) some a with
      | some b => Array.toListAppend #[] (b :: tl)
      | none => go f tl (Array.push #[] hd))

Tactic:
rfl
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
cons :
  ∀ (x : Option α),
    (match (motive := Option α → List α) x with
      | some b => acc.toListAppend (b :: tl)
      | none => go f tl (acc.push hd)) =
      acc.toListAppend
        (match (motive := Option α → List α) x with
        | some b => Array.toListAppend #[] (b :: tl)
        | none => go f tl (Array.push #[] hd))
⊢ (match (motive := Option α → List α) f hd with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match (motive := Option α → List α) f hd with
      | some b => Array.toListAppend #[] (b :: tl)
      | none => go f tl (Array.push #[] hd))

Tactic:
cases f hd with
    | none =>
      simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.toList_push]
      rfl
    | some a => rfl

Premises used: Array.toList_push, Array.toListAppend_eq, List.append_assoc, Option.some, Option.none
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
l : List α
acc : Array α
nil : go f [] acc = acc.toListAppend (lookmap f [])
cons : ∀ (hd : α) (tl : List α), go f (hd :: tl) acc = acc.toListAppend (lookmap f (hd :: tl))
⊢ go f l acc = acc.toListAppend (lookmap f l)

Tactic:
cases l with
  | nil => simp [go, lookmap]
  | cons hd tl =>
    rw [lookmap, go, go]
    cases f hd with
    | none =>
      simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.toList_push]
      rfl
    | some a => rfl

Premises used: Array.toList_push, Array.toListAppend_eq, List.append_assoc, Option.some, List.lookmap, List.lookmap.go, List.cons, Option.none, List.nil
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
⊢ lookmap f [] = []

Tactic:
rfl

Premises used: List.lookmap.go, rfl
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
simp :
  (match (motive := Option α → List α) f a with
    | some b => b :: l
    | none => lookmap.go f l (Array.push #[] a)) =
    a :: lookmap.go f l #[]
⊢ lookmap f (a :: l) = a :: lookmap f l

Tactic:
simp only [lookmap, lookmap.go, Array.toListAppend_eq, nil_append]

Premises used: Array.toListAppend_eq, List.lookmap, List.lookmap.go, List.nil_append
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
rw :
  (match (motive := Option α → List α) none with
    | some b => b :: l
    | none => (Array.push #[] a).toListAppend (lookmap f l)) =
    a :: lookmap.go f l #[]
⊢ (match (motive := Option α → List α) f a with
    | some b => b :: l
    | none => lookmap.go f l (Array.push #[] a)) =
    a :: lookmap.go f l #[]

Tactic:
rw [lookmap.go_append, h]

Premises used: _private.0.List.lookmap.go_append
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match (motive := Option α → List α) none with
    | some b => b :: l
    | none => (Array.push #[] a).toListAppend (lookmap f l)) =
    a :: lookmap.go f l #[]

Tactic:
rfl
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
a b : α
l : List α
h : f a = some b
simp :
  (match (motive := Option α → List α) f a with
    | some b => b :: l
    | none => lookmap.go f l (Array.push #[] a)) =
    b :: l
⊢ lookmap f (a :: l) = b :: l

Tactic:
simp only [lookmap, lookmap.go, Array.toListAppend_eq, nil_append]

Premises used: Array.toListAppend_eq, List.lookmap, List.lookmap.go, List.nil_append
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
a b : α
l : List α
h : f a = some b
rw rw₁ :
  (match (motive := Option α → List α) some b with
    | some b => b :: l
    | none => lookmap.go f l (Array.push #[] a)) =
    b :: l
⊢ (match (motive := Option α → List α) f a with
    | some b => b :: l
    | none => lookmap.go f l (Array.push #[] a)) =
    b :: l

Tactic:
rw [h]
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
a : α
l : List α
none :
  ∀ (h : f a = Option.none),
    lookmap f (a :: l) =
      match (motive := Option α → List α) Option.none with
      | Option.none => a :: lookmap f l
      | Option.some b => b :: l
some :
  ∀ (val : α) (h : f a = Option.some val),
    lookmap f (a :: l) =
      match (motive := Option α → List α) Option.some val with
      | Option.none => a :: lookmap f l
      | Option.some b => b :: l
⊢ lookmap f (a :: l) =
    match (motive := Option α → List α) f a with
    | Option.none => a :: lookmap f l
    | Option.some b => b :: l

Tactic:
cases h : f a
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ lookmap f (a :: l) =
    match (motive := Option α → List α) none with
    | none => a :: lookmap f l
    | some b => b :: l

Tactic:
simp_all
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
a : α
l : List α
val : α
h : f a = some val
⊢ lookmap f (a :: l) =
    match (motive := Option α → List α) some val with
    | none => a :: lookmap f l
    | some b => b :: l

Tactic:
simp_all
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
⊢ f a = g a

Tactic:
obtain ⟨H₁, H₂⟩ := forall_mem_cons.1 H

Premises used: List.forall_mem_cons, Iff.mp
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
⊢ ∀ (x : α), x ∈ l → f x = g x

Tactic:
obtain ⟨H₁, H₂⟩ := forall_mem_cons.1 H

Premises used: List.forall_mem_cons, Iff.mp
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
none : ∀ (h : g a = Option.none), lookmap f (a :: l) = lookmap g (a :: l)
some : ∀ (b : α) (h : g a = Option.some b), lookmap f (a :: l) = lookmap g (a :: l)
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
rcases h : g a with - | b
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
h : g a = none
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
simp [h, H₁.trans h, lookmap_congr H₂]

Premises used: Eq.trans
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
b : α
h : g a = some b
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
simp [lookmap_cons_some _ _ h, lookmap_cons_some _ _ (H₁.trans h)]

Premises used: List.lookmap_cons_some, Eq.trans
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
l : List α
H : ∀ (a : α), a ∈ l → f a = none
⊢ lookmap f l = l

Tactic:
(lookmap_congr H).trans (lookmap_none l)

Premises used: List.lookmap_congr, Eq.trans, List.lookmap_none
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
none : ∀ (h' : f a = Option.none), map g (lookmap f (a :: l)) = map g (a :: l)
some : ∀ (b : α) (h' : f a = Option.some b), map g (lookmap f (a :: l)) = map g (a :: l)
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

Tactic:
rcases h' : f a with - | b
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
h' : f a = none
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

Tactic:
simpa [h'] using lookmap_map_eq _ h l
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
b : α
h' : f a = some b
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

Tactic:
simp [lookmap_cons_some _ _ h', h _ _ h']

Premises used: List.lookmap_cons_some
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
h₁ : ∀ (a b : α), b ∈ f a → id a = id b
⊢ lookmap f l = l

Tactic:
rw [← map_id (l.lookmap f), lookmap_map_eq, map_id]

Premises used: List.map_id, List.lookmap, List.lookmap_map_eq
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ ∀ (a b : α), b ∈ f a → id a = id b

Tactic:
h
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ ∀ (a b : α), b ∈ f a → id a = id b

Tactic:
exact h
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
l : List α
h : ∀ (a b : α), b ∈ f a → () = ()
⊢ (lookmap f l).length = l.length

Tactic:
rw [← length_map, lookmap_map_eq _ fun _ => (), length_map]

Premises used: Unit.unit, List.lookmap_map_eq, List.length_map
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
l : List α
⊢ ∀ (a b : α), b ∈ f a → () = ()

Tactic:
simp
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) []
⊢ lookmap f [] ~ lookmap f []

Tactic:
simp