awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
rw : (replicate n l).flatten.reverse.head? = l.getLast?
rw₁ : (replicate n l).flatten.reverse.head? = l.reverse.head?
rw₂ : (map reverse (replicate n l)).reverse.flatten.head? = l.reverse.head?
rw₃ : (replicate n l.reverse).reverse.flatten.head? = l.reverse.head?
rw₄ : (replicate n l.reverse).flatten.head? = l.reverse.head?
rw₅ rw₆ : l.reverse.head? = l.reverse.head?
⊢ (replicate n l).flatten.getLast? = l.getLast?

Tactic:
rw [← List.head?_reverse, ← List.head?_reverse, List.reverse_flatten, List.map_replicate,
  List.reverse_replicate, head?_flatten_replicate h]

Premises used: List.reverse_flatten, List.head?_reverse, List.head?_flatten_replicate, List.reverse_replicate, List.map_replicate
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x y : α
⊢ Membership.mem (γ := List α) (pure y) x ↔ x = y

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α β : Type u_2
f : α → List β
l : List α
⊢ l >>= f = flatMap f l

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
l : List α
⊢ (a :: l).reverse = l.reverse.concat a

Tactic:
simp only [reverse_cons, concat_eq_append]

Premises used: List.concat_eq_append, List.reverse_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
a : α
rw : [a].reverse ++ l.reverse = a :: l.reverse
⊢ (l ++ [a]).reverse = a :: l.reverse

Tactic:
rw [reverse_append]

Premises used: List.reverse_append
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
a : α
⊢ [a].reverse ++ l.reverse = a :: l.reverse

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
⊢ Involutive.{u + 1} (α := List α) reverse

Tactic:
reverse_reverse

Premises used: List.reverse_reverse, Function.Involutive
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
⊢ Injective.{u + 1, u + 1} (α := List α) reverse

Tactic:
reverse_involutive.injective

Premises used: Function.Involutive.injective, List.reverse_involutive
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
⊢ Surjective.{u + 1, u + 1} (α := List α) reverse

Tactic:
reverse_involutive.surjective

Premises used: Function.Involutive.surjective, List.reverse_involutive
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
⊢ Bijective.{u + 1, u + 1} (α := List α) reverse

Tactic:
reverse_involutive.bijective

Premises used: Function.Involutive.bijective, List.reverse_involutive
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
l : List α
⊢ l.concat a = (a :: l.reverse).reverse

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
l₁ l₂ : List α
⊢ map f (l₁.reverseAux l₂) = (map f l₁).reverseAux (map f l₂)

Tactic:
simp only [reverseAux_eq, map_append, map_reverse]

Premises used: List.reverseAux_eq, List.map_reverse, List.map_append
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
l : List α
⊢ (l ++ [a]).getLast ⋯ = a

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₂ : List α
h : l₂ ≠ []
⊢ ([] ++ l₂).getLast ⋯ = l₂.getLast h

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₂ : List α
h : l₂ ≠ []
head : α
tail : List α
tail_ih : (tail ++ l₂).getLast ⋯ = l₂.getLast h
⊢ (head :: tail ++ l₂).getLast ⋯ = l₂.getLast h

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
h : l₂ ≠ []
nil : ([] ++ l₂).getLast ⋯ = l₂.getLast h
cons :
  ∀ (head : α) (tail : List α), (tail ++ l₂).getLast ⋯ = l₂.getLast h → (head :: tail ++ l₂).getLast ⋯ = l₂.getLast h
⊢ (l₁ ++ l₂).getLast ⋯ = l₂.getLast h

Tactic:
induction l₁ with grind
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l_1 l₁ l₂ : List α
a : α
l : List α
⊢ l.concat a ≠ []

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
l : List α
⊢ (l.concat a).getLast ⋯ = a

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
⊢ [a].getLast ⋯ = a

Tactic:
rfl

Premises used: List.getLast, rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
rw : a :: ((b :: l).dropLast ++ [(b :: l).getLast ⋯]) = a :: b :: l
⊢ (a :: b :: l).dropLast ++ [(a :: b :: l).getLast h] = a :: b :: l

Tactic:
rw [dropLast_cons_cons, cons_append, getLast_cons (cons_ne_nil _ _)]

Premises used: List.getLast_cons, List.cons_ne_nil, List.dropLast_cons_cons, List.cons_append
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
e_tail : (b :: l).dropLast ++ [(b :: l).getLast ⋯] = b :: l
⊢ a :: ((b :: l).dropLast ++ [(b :: l).getLast ⋯]) = a :: b :: l

Tactic:
congr
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ (b :: l).dropLast ++ [(b :: l).getLast ⋯] = b :: l

Tactic:
dropLast_append_getLast (cons_ne_nil b l)

Premises used: List.cons_ne_nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ (b :: l).dropLast ++ [(b :: l).getLast ⋯] = b :: l

Tactic:
exact dropLast_append_getLast (cons_ne_nil b l)

Premises used: List.cons_ne_nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
h₁ : l₁ ≠ []
h₂ : l₂ ≠ []
h₃ : l₁ = l₂
subst : ∀ (h₁ : l₂ ≠ []), l₂.getLast h₁ = l₂.getLast h₂
⊢ l₁.getLast h₁ = l₂.getLast h₂

Tactic:
subst l₁
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₂ : List α
h₂ h₁ : l₂ ≠ []
⊢ l₂.getLast h₁ = l₂.getLast h₂

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
m : ℕ
a : α
simp : (replicate m a ++ [a]).getLast ⋯ = a
⊢ (replicate (m + 1) a).getLast ⋯ = a

Tactic:
simp only [replicate_succ']

Premises used: List.replicate_succ'
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
m : ℕ
a : α
⊢ (replicate m a ++ [a]).getLast ⋯ = a

Tactic:
getLast_append_singleton _

Premises used: List.getLast_append_singleton
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
m : ℕ
a : α
⊢ (replicate m a ++ [a]).getLast ⋯ = a

Tactic:
exact getLast_append_singleton _

Premises used: List.getLast_append_singleton
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x : α
hx : Membership.mem (γ := Option α) (getLast? []) x
⊢ ∃ (h : Ne.{u + 1} (α := List α) [] []), x = getLast [] h

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a x : α
hx : x ∈ [a].getLast?
⊢ ∃ (h : [a] ≠ []), x = [a].getLast h

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b : α
l : List α
x : α
hx : x ∈ (a :: b :: l).getLast?
⊢ ∃ (h : a :: b :: l ≠ []), x = (a :: b :: l).getLast h

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x y : α
h : Membership.mem (γ := Option α) (getLast? []) x
⊢ x ∈ [y].getLast?

Tactic:
contradiction
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (a :: b :: l).getLast?
⊢ c ∈ (b :: l).getLast?

Tactic:
rw [getLast?_cons_cons] at hc

Premises used: List.getLast?_cons_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
rw : a :: (b :: l).dropLast ++ [c] = a :: b :: l
rw₁ : a :: ((b :: l).dropLast ++ [c]) = a :: b :: l
rw₂ rw₃ : a :: b :: l = a :: b :: l
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l

Tactic:
rw [dropLast_cons_cons, cons_append, dropLast_append_getLast? _ hc]

Premises used: List.dropLast_cons_cons, List.cons_append
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
⊢ Eq.{u + 1} (α := α) (getLastI []) (Option.getD (getLast? []) default)

Tactic:
simp [getLastI]

Premises used: List.getLastI
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
head head_1 c : α
l : List α
⊢ (head :: head_1 :: c :: l).getLastI = (head :: head_1 :: c :: l).getLast?.getD default

Tactic:
simp [getLastI, getLastI_eq_getLast?_getD (c :: l)]

Premises used: List.cons, List.getLastI
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
⊢ ∀ (l : List α), l.getLastI = l.getLast?.getD default

Tactic:
getLastI_eq_getLast?_getD

Premises used: List.getLastI_eq_getLast?_getD
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
rw : (b :: (c :: l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
rw₁ : (b :: c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
rw₂ : (c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
rw₃ : (c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
rw₄ rw₅ : (a :: l₂).getLast? = (a :: l₂).getLast?
⊢ (b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?

Tactic:
rw [cons_append, cons_append, getLast?_cons_cons,
    ← cons_append, getLast?_append_cons (c :: l₁)]

Premises used: List.getLast?_cons_cons, List.cons, List.cons_append
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ : List α
hl₂ : Ne.{u + 1} (α := List α) [] []
⊢ (l₁ ++ []).getLast? = getLast? []

Tactic:
contradiction
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
x : α
h : x ∈ l₂.getLast?
⊢ x ∈ (l₁ ++ l₂).getLast?

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
a : α
ha : a ∈ l
ha' : a ≠ l.getLast ⋯
⊢ a ∈ l.dropLast

Tactic:
grind [dropLast_concat_getLast]

Premises used: List.dropLast_concat_getLast
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
a d : α
ha : a ∈ l
ha' : a ≠ l.getLastD d
⊢ a ≠ l.getLast ⋯

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
a : α
ha : a ∈ l
ha' : some a ≠ l.getLast?
⊢ a ≠ l.getLast ⋯

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
⊢ Eq.{u + 1} (α := α) (head! []) default

Tactic:
rfl

Premises used: List.head!, panicCore, panic, rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
hl : l ≠ []
⊢ l.head hl = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯

Tactic:
(getElem_zero _).symm

Premises used: List.getElem_zero, Eq.symm
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
l : List α
nil : Eq.{u + 1} (α := α) (head! []) (Option.getD (head? []) default)
cons : ∀ (head : α) (tail : List α), (head :: tail).head! = (head :: tail).head?.getD default
⊢ l.head! = l.head?.getD default

Tactic:
cases l
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
⊢ Eq.{u + 1} (α := α) (head! []) (Option.getD (head? []) default)

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
head : α
tail : List α
⊢ (head :: tail).head! = (head :: tail).head?.getD default

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
l : List α
⊢ l.head! = l.head?.getD default

Tactic:
head!_eq_head?_getD l

Premises used: List.head!_eq_head?_getD
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
⊢ Surjective.{u + 1, u + 1} (α := List α) head!

Tactic:
fun x => ⟨[x], rfl⟩

Premises used: List.cons, Exists.intro, Function.Surjective, rfl, List.nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
⊢ Surjective.{u + 1, u + 1} (α := List α) head?

Tactic:
Option.forall.2 ⟨⟨[], rfl⟩, fun x => ⟨[x], rfl⟩⟩

Premises used: Iff.mpr, Option.forall, List.cons, And.intro, Exists.intro, Function.Surjective, rfl, List.nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x a : α
l : List α
h : x ∈ (a :: l).head?
⊢ a = x

Tactic:
simp only [head?, Option.mem_def, Option.some_inj] at h

Premises used: List.head?, Option.some_inj, Option.mem_def
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x a : α
l : List α
h : a = x
⊢ a :: l = x :: (a :: l).tail

Tactic:
h ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x a : α
l : List α
h : a = x
⊢ a :: l = x :: (a :: l).tail

Tactic:
exact h ▸ rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
a : α
l : List α
⊢ (a :: l).head! = a

Tactic:
rfl

Premises used: List.head!, rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
t s : List α
h : s ≠ []
nil : ∀ (h : Ne.{u + 1} (α := List α) [] []), ([] ++ t).head! = head! []
cons :
  ∀ (head : α) (tail : List α),
    (∀ (h : tail ≠ []), (tail ++ t).head! = tail.head!) →
      ∀ (h : head :: tail ≠ []), (head :: tail ++ t).head! = (head :: tail).head!
⊢ (s ++ t).head! = s.head!

Tactic:
induction s
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
t : List α
h : Ne.{u + 1} (α := List α) [] []
⊢ ([] ++ t).head! = head! []

Tactic:
contradiction
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
t : List α
head : α
tail : List α
tail_ih : ∀ (h : tail ≠ []), (tail ++ t).head! = tail.head!
h : head :: tail ≠ []
⊢ (head :: tail ++ t).head! = (head :: tail).head!

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
s t : List α
x : α
h : x ∈ s.head?
⊢ x ∈ (s ++ t).head?

Tactic:
grind [Option.mem_def]

Premises used: Option.mem_def
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
l : List α
h : l ≠ []
⊢ (l ++ [a]).tail = l.tail ++ [a]

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
h : Membership.mem (γ := Option α) (head? []) a
⊢ a :: tail [] = []

Tactic:
contradiction
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
b : α
l : List α
a : α
h : a ∈ (b :: l).head?
⊢ b = a

Tactic:
simpa using h
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
b : α
l : List α
a : α
h : a ∈ (b :: l).head?
⊢ b = a

Tactic:
have : b = a := by simpa using h
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
b : α
l : List α
a : α
h : a ∈ (b :: l).head?
this : b = a
⊢ a :: (b :: l).tail = b :: l

Tactic:
simp [this]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
h : Ne.{u + 1} (α := List α) [] []
⊢ Membership.mem (γ := Option α) (head? []) (head! [])

Tactic:
contradiction
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
l : List α
h : l ≠ []
⊢ l.head! :: l.tail = l

Tactic:
cons_head?_tail (head!_mem_head? h)

Premises used: List.head!_mem_head?, List.cons_head?_tail
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
l : List α
h : l ≠ []
⊢ l.head! ∈ l.head! :: l.tail

Tactic:
have h' : l.head! ∈ l.head! :: l.tail := mem_cons_self
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : Inhabited α
l : List α
h : l ≠ []
h' : l.head! ∈ l.head! :: l.tail
rwa rwa₁ rwa₂ rwa₃ : ∀ (h' : l.head! ∈ l), l.head! ∈ l
⊢ l.head! ∈ l

Tactic:
rwa [cons_head!_tail h] at h'

Premises used: List.cons_head!_tail
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l_1 l₁ l₂ l : List α
i : Fin l.length
⊢ (getElem? (valid := fun (xs : List α) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i).isSome = true

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
i : Fin l.length
⊢ l.get i = (getElem? (valid := fun (xs : List α) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i).get ⋯

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p : α → Prop
simp :
  (∃ (x : α),
      (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧ p x) ↔
    ∃ (i : ℕ), ∃ (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x)
⊢ (∃ (x : α), x ∈ l ∧ p x) ↔
    ∃ (i : ℕ), ∃ (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x)

Tactic:
simp only [mem_iff_getElem]

Premises used: List.mem_iff_getElem
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p : α → Prop
⊢ (∃ (x : α),
      (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧ p x) ↔
    ∃ (i : ℕ), ∃ (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x)

Tactic:
⟨fun ⟨_x, ⟨i, hi, hix⟩, hxp⟩ ↦ ⟨i, hi, hix ▸ hxp⟩, fun ⟨i, hi, hp⟩ ↦ ⟨_, ⟨i, hi, rfl⟩, hp⟩⟩

Premises used: Exists, Eq.rec, _private.0.List.exists_mem_iff_getElem.match_2, GetElem.getElem, And, And.intro, Iff.intro, Exists.intro, _private.0.List.exists_mem_iff_getElem.match_1, Eq.symm, Eq, rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p : α → Prop
⊢ (∃ (x : α),
      (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧ p x) ↔
    ∃ (i : ℕ), ∃ (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x)

Tactic:
exact ⟨fun ⟨_x, ⟨i, hi, hix⟩, hxp⟩ ↦ ⟨i, hi, hix ▸ hxp⟩, fun ⟨i, hi, hp⟩ ↦ ⟨_, ⟨i, hi, rfl⟩, hp⟩⟩
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p : α → Prop
⊢ (∃ (x : α), x ∈ l ∧ p x) ↔ ∃ (i : Fin l.length), p (l.get i)

Tactic:
exists_mem_iff_getElem.trans ⟨fun ⟨i, hi, h⟩ ↦ ⟨⟨i, hi⟩, h⟩, fun ⟨i, h⟩ ↦ ⟨i, i.isLt, h⟩⟩

Premises used: List.get, Fin.isLt, Exists, Fin.mk, _private.0.List.exists_mem_iff_getElem.match_2, Fin.val, GetElem.getElem, List.exists_mem_iff_getElem, _private.0.List.exists_mem_iff_get.match_1, Iff.intro, Exists.intro, Iff.trans
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p : α → Prop
⊢ (∀ (x : α), x ∈ l → p x) ↔
    ∀ (i : ℕ) (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x)

Tactic:
simp [mem_iff_getElem, @forall_comm α]

Premises used: forall_comm, List.mem_iff_getElem
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p : α → Prop
⊢ (∀ (x : α), x ∈ l → p x) ↔ ∀ (i : Fin l.length), p (l.get i)

Tactic:
forall_mem_iff_getElem.trans ⟨fun h i ↦ h i i.isLt, fun h i hi ↦ h ⟨i, hi⟩⟩

Premises used: Fin.isLt, Fin.mk, Fin.val, Iff.intro, Iff.trans, List.forall_mem_iff_getElem
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
⊢ Surjective l.get ↔ ∀ (x : α), x ∈ l

Tactic:
forall_congr' fun _ ↦ mem_iff_get.symm

Premises used: List.mem_iff_get, forall_congr', Function.Surjective, Iff.symm
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
⊢ (Surjective.{1, u + 1} (β := α) fun (n : Fin l.length) ↦
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (↑n : ℕ) ⋯) ↔
    ∀ (x : α), x ∈ l

Tactic:
get_surjective_iff

Premises used: List.get_surjective_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
⊢ (Surjective.{1, u + 1} (β := Option α) fun (n : ℕ) ↦
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) ↔
    ∀ (x : α), x ∈ l

Tactic:
⟨fun h x ↦ mem_iff_getElem?.mpr <| h x, fun h x ↦ ?_⟩

Premises used: Iff.mpr, Option.some, List.mem_iff_getElem?, Iff.intro
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
refine :
  ∀ (h : ∀ (x : α), x ∈ l) (x : Option α),
    ∃ (a : ℕ), (fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a = x
⊢ (Surjective.{1, u + 1} (β := Option α) fun (n : ℕ) ↦
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) ↔
    ∀ (x : α), x ∈ l

Tactic:
refine ⟨fun h x ↦ mem_iff_getElem?.mpr <| h x, fun h x ↦ ?_⟩
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
⊢ ∃ (a : ℕ),
    Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a)
      none

Tactic:
⟨l.length, getElem?_eq_none <| Nat.le_refl _⟩

Premises used: Nat.le_refl, List.getElem?_eq_none, Exists.intro, List.length
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
⊢ ∃ (a : ℕ),
    Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a)
      none

Tactic:
exact ⟨l.length, getElem?_eq_none <| Nat.le_refl _⟩
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
x : α
⊢ ∃ (a : ℕ), (fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a = some x

Tactic:
mem_iff_getElem?.mp <| h x

Premises used: List.mem_iff_getElem?, Iff.mp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
x : α
⊢ ∃ (a : ℕ), (fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a = some x

Tactic:
exact mem_iff_getElem?.mp <| h x

Premises used: List.mem_iff_getElem?, Iff.mp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
x : Option α
none :
  ∃ (a : ℕ),
    Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a)
      Option.none
some :
  ∀ (x : α),
    ∃ (a : ℕ), (fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a = Option.some x
⊢ ∃ (a : ℕ), (fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a = x

Tactic:
cases x with
  | none => exact ⟨l.length, getElem?_eq_none <| Nat.le_refl _⟩
  | some x => exact mem_iff_getElem?.mp <| h x

Premises used: Option.some, List.mem_iff_getElem?, Option.none, Iff.mp
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l_1 l₁ l₂ l : List α
i : ℕ
h : i < l.tail.length
⊢ i < l.length - 1

Tactic:
simp only [length_tail] at h

Premises used: List.length_tail
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l_1 l₁ l₂ l : List α
i : ℕ
h : i < l.length - 1
⊢ i + 1 < l.length

Tactic:
lia
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
i : ℕ
h : i < l.tail.length
h' : i + 1 < l.length
⊢ l.tail.get (⟨i, h⟩ : Fin l.tail.length) = l.get (⟨i + 1, h'⟩ : Fin l.length)

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
a b : α
⊢ a :: l₁ <+ b :: l₂ ↔ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
⊢ l₁ <+ a :: l₂

Tactic:
h.cons _

Premises used: List.Sublist.cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
a : α
mp : l <+ [a] → l = [] ∨ l = [a]
mpr : l = [] ∨ l = [a] → l <+ [a]
⊢ l <+ [a] ↔ l = [] ∨ l = [a]

Tactic:
constructor
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
a : α
h : l <+ []
⊢ l = [] ∨ l = [a]

Tactic:
aesop
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
l₁ : List α
h : l₁ <+ []
⊢ a :: l₁ = [] ∨ a :: l₁ = [a]

Tactic:
aesop
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
a : α
h : l = []
⊢ l <+ [a]

Tactic:
aesop
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
a : α
h : l = [a]
⊢ l <+ [a]

Tactic:
aesop
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
s₁ : l₁ <+ l₂
s₂ : l₂ <+ l₁
⊢ l₁ = l₂

Tactic:
s₁.eq_of_length_le s₂.length_le

Premises used: List.Sublist.length_le, List.Sublist.eq_of_length_le
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
a b : α
h₁ : a ≠ b
h₂ : a :: l₁ <+ b :: l₂
⊢ a :: l₁ <+ l₂

Tactic:
match h₁, h₂ with
  | _, .cons _ h => h

Premises used: _private.0.List.Sublist.of_cons_of_ne.match_1, List.cons, List.Sublist
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a b : α
l : List α
h : b = a
e : b = a := h
rw : idxOf b (b :: l) = 0
⊢ idxOf a (b :: l) = 0

Tactic:
rw [← e]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a b : α
l : List α
h : b = a
e : b = a := h
⊢ idxOf b (b :: l) = 0

Tactic:
idxOf_cons_self

Premises used: List.idxOf_cons_self
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a b : α
l : List α
h : b = a
e : b = a := h
⊢ idxOf b (b :: l) = 0

Tactic:
exact idxOf_cons_self

Premises used: List.idxOf_cons_self
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a b : α
l : List α
h : b ≠ a
⊢ idxOf a (b :: l) = (idxOf a l).succ

Tactic:
simp [idxOf_cons, beq_false_of_ne h]

Premises used: beq_false_of_ne, List.idxOf_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l : List α
⊢ idxOf a l = l.length ↔ ¬a ∈ l

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
a : α
⊢ ¬a ∈ l → idxOf a l = l.length

Tactic:
idxOf_eq_length_iff.2

Premises used: Iff.mpr, List.idxOf_eq_length_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
a : α
nil : idxOf a [] = 0 ↔ Eq.{u + 1} (α := List α) [] [] ∨ head? [] = some a
cons : ∀ (head : α) (tail : List α), idxOf a (head :: tail) = 0 ↔ head :: tail = [] ∨ (head :: tail).head? = some a
⊢ idxOf a l = 0 ↔ l = [] ∨ l.head? = some a

Tactic:
cases l
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
⊢ idxOf a [] = 0 ↔ Eq.{u + 1} (α := List α) [] [] ∨ head? [] = some a

Tactic:
simp