awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.TFAE
Goal:
c : Prop
l : List Prop
a b : Prop
IH :
  ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
    (a ↔ b) ∧ (b :: l).TFAE
h_chain : (a → b) ∧ (b → c) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)
h_last : l.getLastD c → a
ab : a → b
bc : b → c
⊢ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)

Tactic:
rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
-- Module: Mathlib.Data.List.TFAE
Goal:
c : Prop
l : List Prop
a b : Prop
IH :
  ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
    (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)
⊢ (b ↔ c) ∧ (c :: l).TFAE

Tactic:
have := IH ⟨bc, ch⟩ (ab ∘ h_last)
-- Module: Mathlib.Data.List.TFAE
Goal:
c : Prop
l : List Prop
a b : Prop
IH :
  ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
    (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)
this : (b ↔ c) ∧ (c :: l).TFAE
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE

Tactic:
⟨⟨ab, h_last ∘ (this.2 c (.head _) _ getLastD_mem_cons).1 ∘ bc⟩, this⟩

Premises used: List.getLastD_mem_cons, Function.comp, And.right, And.intro, Iff.intro, List.Mem.head, Iff.mp
-- Module: Mathlib.Data.List.TFAE
Goal:
c : Prop
l : List Prop
a b : Prop
IH :
  ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
    (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)
this : (b ↔ c) ∧ (c :: l).TFAE
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE

Tactic:
exact ⟨⟨ab, h_last ∘ (this.2 c (.head _) _ getLastD_mem_cons).1 ∘ bc⟩, this⟩
-- Module: Mathlib.Data.List.TFAE
Goal:
a b : Prop
l : List Prop
h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (a :: b :: l)
h_last : l.getLastD b → a
nil : ∀ {a b : Prop} (h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) [a, b]) (h_last : getLastD [] b → a), [a, b].TFAE
cons :
  ∀ (c : Prop) (l : List Prop)
    (IH :
      ∀ {a b : Prop} (h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (a :: b :: l)) (h_last : l.getLastD b → a),
        (a :: b :: l).TFAE)
    {a b : Prop} (h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (a :: b :: c :: l))
    (h_last : (c :: l).getLastD b → a), (a :: b :: c :: l).TFAE
⊢ (a :: b :: l).TFAE

Tactic:
induction l generalizing a b with
  | nil => simp_all [tfae_cons_cons, iff_def]
  | cons c l IH =>
    simp only [tfae_cons_cons, getLastD_cons, isChain_cons_cons] at *
    rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
    have := IH ⟨bc, ch⟩ (ab ∘ h_last)
    exact ⟨⟨ab, h_last ∘ (this.2 c (.head _) _ getLastD_mem_cons).1 ∘ bc⟩, this⟩

Premises used: iff_def, List.cons, List.isChain_cons_cons, List.tfae_cons_cons, List.getLastD_cons, List.nil
-- Module: Mathlib.Data.List.TFAE
Goal:
l : List Prop
h : l.TFAE
n₁ n₂ : Nat
a b : Prop
h₁ : getElem? (valid := fun (as : List Prop) (i : Nat) ↦ i < as.length) l n₁ = some a
h₂ : getElem? (valid := fun (as : List Prop) (i : Nat) ↦ i < as.length) l n₂ = some b
⊢ a ↔ b

Tactic:
h _ (List.mem_of_getElem? h₁) _ (List.mem_of_getElem? h₂)

Premises used: List.mem_of_getElem?
-- Module: Mathlib.Data.List.TFAE
Goal:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun (p : α → Prop) ↦ p a) l)
simp : ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∀ (a : α), j a) ↔ ∀ (a : α), j_1 a)
⊢ TFAE (map (fun (p : α → Prop) ↦ ∀ (a : α), p a) l)

Tactic:
simp only [TFAE, List.forall_mem_map]

Premises used: List.forall_mem_map, List.TFAE
-- Module: Mathlib.Data.List.TFAE
Goal:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun (p : α → Prop) ↦ p a) l)
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∀ (a : α), p₁ a) ↔ ∀ (a : α), p₂ a

Tactic:
forall_congr' fun a ↦ H a (p₁ a) (mem_map_of_mem hp₁)
    (p₂ a) (mem_map_of_mem hp₂)

Premises used: forall_congr', List.mem_map_of_mem
-- Module: Mathlib.Data.List.TFAE
Goal:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun (p : α → Prop) ↦ p a) l)
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∀ (a : α), p₁ a) ↔ ∀ (a : α), p₂ a

Tactic:
exact forall_congr' fun a ↦ H a (p₁ a) (mem_map_of_mem hp₁)
    (p₂ a) (mem_map_of_mem hp₂)

Premises used: forall_congr', List.mem_map_of_mem
-- Module: Mathlib.Data.List.TFAE
Goal:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun (p : α → Prop) ↦ p a) l)
simp : ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∃ (a : α), j a) ↔ ∃ (a : α), j_1 a)
⊢ TFAE (map (fun (p : α → Prop) ↦ ∃ (a : α), p a) l)

Tactic:
simp only [TFAE, List.forall_mem_map]

Premises used: List.forall_mem_map, List.TFAE
-- Module: Mathlib.Data.List.TFAE
Goal:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun (p : α → Prop) ↦ p a) l)
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∃ (a : α), p₁ a) ↔ ∃ (a : α), p₂ a

Tactic:
exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem hp₁)
    (p₂ a) (mem_map_of_mem hp₂)

Premises used: exists_congr, List.mem_map_of_mem
-- Module: Mathlib.Data.List.TFAE
Goal:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun (p : α → Prop) ↦ p a) l)
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∃ (a : α), p₁ a) ↔ ∃ (a : α), p₂ a

Tactic:
exact exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem hp₁)
    (p₂ a) (mem_map_of_mem hp₂)

Premises used: exists_congr, List.mem_map_of_mem
-- Module: Mathlib.Data.List.TFAE
Goal:
l : List Prop
⊢ (map Not l).TFAE ↔ l.TFAE

Tactic:
simp only [TFAE, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
    Decidable.not_iff_not]

Premises used: and_imp, forall_exists_index, List.TFAE, Decidable.not_iff_not, List.mem_map, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Data.List.TFAE
Goal:
l : List Prop
⊢ (map Not l).TFAE ↔ l.TFAE

Tactic:
classical
  simp only [TFAE, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
    Decidable.not_iff_not]

Premises used: and_imp, forall_exists_index, List.TFAE, Decidable.not_iff_not, List.mem_map, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.length
rw : [getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n h] = [l.get (⟨n, h⟩ : Fin l.length)]
⊢ take 1 (drop n l) = [l.get (⟨n, h⟩ : Fin l.length)]

Tactic:
rw [drop_eq_getElem_cons h, take, take]

Premises used: List.take, List.drop_eq_getElem_cons
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ [getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n h] = [l.get (⟨n, h⟩ : Fin l.length)]

Tactic:
simp
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
x : List α
n : ℕ
⊢ take n x = x → x.length ≤ n

Tactic:
grind
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
x : List α
n : ℕ
rw : take n x = x ↔ x.length ≤ n
rw₁ rw₂ : x.length ≤ n ↔ x.length ≤ n
⊢ x = take n x ↔ x.length ≤ n

Tactic:
rw [Eq.comm, take_eq_self_iff]

Premises used: Eq.comm, List.take_eq_self_iff
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
x y : List α
n : ℕ
⊢ take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length

Tactic:
simp [take_append, Nat.sub_eq_zero_iff_le, Or.comm]

Premises used: Or.comm, Nat.sub_eq_zero_iff_le, List.take_append
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
x y : List α
n : ℕ
rw : take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length
⊢ take n x = take n (x ++ y) ↔ y = [] ∨ n ≤ x.length

Tactic:
rw [Eq.comm]

Premises used: Eq.comm
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
x y : List α
n : ℕ
⊢ take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length

Tactic:
apply take_eq_left_iff

Premises used: List.take_eq_left_iff
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
x : List α
m n : ℕ
rw : take n (drop m x) ++ drop n (drop m x) = drop m x
rw₁ rw₂ : drop m x = drop m x
⊢ take n (drop m x) ++ drop (m + n) x = drop m x

Tactic:
rw [← drop_drop, take_append_drop]

Premises used: List.drop_drop, List.take_append_drop
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
x : List α
m n : ℕ
rw : take n (drop m x) ++ drop (m + n) x = drop m x
rw₁ rw₂ : drop m x = drop m x
⊢ take n (drop m x) ++ drop (n + m) x = drop m x

Tactic:
rw [Nat.add_comm, drop_take_append_drop]

Premises used: List.drop_take_append_drop, Nat.add_comm
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
i : ℕ
h : i < l.length
⊢ take i l ++ [getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h] = take (i + 1) l

Tactic:
simp
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n h :: drop (n + 1) l = drop n l

Tactic:
(drop_eq_getElem_cons h).symm

Premises used: Eq.symm, List.drop_eq_getElem_cons
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n : Fin l.length
⊢ l.get n :: drop ((↑n : ℕ) + 1) l = drop (↑n : ℕ) l

Tactic:
(drop_eq_getElem_cons n.2).symm

Premises used: Fin.isLt, Eq.symm, List.drop_eq_getElem_cons
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
h : Ne.{u + 1} (α := List α) [] []
⊢ drop (length.{u} (α := α) [] - 1) [] = [getLast [] h]

Tactic:
aesop
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
pos : ∀ (hl : l = []), drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
neg : ∀ (hl : ¬l = []), drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

Tactic:
by_cases hl : l = []
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

Tactic:
simp_all
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
neg : [l.getLast hl] = [(a :: l).getLast h]
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

Tactic:
rw [length_cons, Nat.add_one_sub_one, List.drop_length_cons hl a]

Premises used: Nat.add_one_sub_one, List.length_cons, List.drop_length_cons
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ [l.getLast hl] = [(a :: l).getLast h]

Tactic:
simp [getLast_cons, hl]

Premises used: List.getLast_cons
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
h : l ≠ []
nil : ∀ (h : Ne.{u + 1} (α := List α) [] []), drop (length.{u} (α := α) [] - 1) [] = [getLast [] h]
cons :
  ∀ (a : α) (l : List α) (ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]) (h : a :: l ≠ []),
    drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
⊢ drop (l.length - 1) l = [l.getLast h]

Tactic:
induction l with
  | nil => aesop
  | cons a l ih =>
    by_cases hl : l = []
    · simp_all
    rw [length_cons, Nat.add_one_sub_one, List.drop_length_cons hl a]
    simp [getLast_cons, hl]

Premises used: Nat.add_one_sub_one, List.length_cons, List.cons, List.getLast_cons, List.nil
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
⊢ tail^[0] l = drop 0 l

Tactic:
rfl
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
l : List α
succ : Eq.{u + 1} (α := List α) (tail^[n + 1] []) (drop (n + 1) [])
succ₁ : ∀ (head : α) (tail : List α), List.tail^[n + 1] (head :: tail) = drop (n + 1) (head :: tail)
⊢ tail^[n + 1] l = drop (n + 1) l

Tactic:
cases l
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
⊢ Eq.{u + 1} (α := List α) (tail^[n + 1] []) (drop (n + 1) [])

Tactic:
simp [*]
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
n : ℕ
ih : ∀ (l : List α), List.tail^[n] l = drop n l
head : α
tail : List α
⊢ List.tail^[n + 1] (head :: tail) = drop (n + 1) (head :: tail)

Tactic:
simp [*]
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n : ℕ
zero : ∀ (l : List α), tail^[0] l = drop 0 l
succ : ∀ (n : ℕ) (ih : ∀ (l : List α), tail^[n] l = drop n l) (l : List α), tail^[n + 1] l = drop (n + 1) l
⊢ tail^[n] l = drop n l

Tactic:
induction n generalizing l with
  | zero => rfl
  | succ n ih => cases l <;> simp [*]

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n : ℕ
h :
  ∀ (i : ℕ) (a : α),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n l).tail i = some a ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n - 1) l.tail) i = some a
⊢ (take n l).tail = take (n - 1) l.tail

Tactic:
ext
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n i : ℕ
a : α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n l).tail i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n - 1) l.tail) i = some a

Tactic:
grind
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n : ℕ
h :
  ∀ (i : ℕ) (a : α),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n l).dropLast i = some a ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n - 1) l.dropLast) i = some a
⊢ (take n l).dropLast = take (n - 1) l.dropLast

Tactic:
ext
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n i : ℕ
a : α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take n l).dropLast i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n - 1) l.dropLast) i = some a

Tactic:
grind
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n : ℕ
h :
  ∀ (i : ℕ) (a : α),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l).tail i = some a ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l.tail) i = some a
⊢ (drop n l).tail = drop n l.tail

Tactic:
ext
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n i : ℕ
a : α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l).tail i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l.tail) i = some a

Tactic:
grind
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n : ℕ
h :
  ∀ (i : ℕ) (a : α),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l).dropLast i = some a ↔
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l.dropLast) i = some a
⊢ (drop n l).dropLast = drop n l.dropLast

Tactic:
ext
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l : List α
n i : ℕ
a : α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l).dropLast i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (drop n l.dropLast) i = some a

Tactic:
grind
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
inst : Inhabited α
l₁ l₂ : List α
⊢ l₁.length ≤ (l₁ ++ l₂).length

Tactic:
simp only [length_append, Nat.le_add_right]

Premises used: Nat.le_add_right, List.length_append
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
inst : Inhabited α
l₁ l₂ : List α
n : ℕ
h : l₁.length = n
rw : takeI l₁.length (l₁ ++ l₂) = l₁
⊢ takeI n (l₁ ++ l₂) = l₁

Tactic:
rw [← h]
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
inst : Inhabited α
l₁ l₂ : List α
n : ℕ
h : l₁.length = n
⊢ takeI l₁.length (l₁ ++ l₂) = l₁

Tactic:
apply takeI_left

Premises used: List.takeI_left
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l₁ l₂ : List α
a : α
⊢ l₁.length ≤ (l₁ ++ l₂).length

Tactic:
simp only [length_append, Nat.le_add_right]

Premises used: Nat.le_add_right, List.length_append
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l₁ l₂ : List α
n : ℕ
a : α
h : l₁.length = n
rw : takeD l₁.length (l₁ ++ l₂) a = l₁
⊢ takeD n (l₁ ++ l₂) a = l₁

Tactic:
rw [← h]
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
l₁ l₂ : List α
n : ℕ
a : α
h : l₁.length = n
⊢ takeD l₁.length (l₁ ++ l₂) a = l₁

Tactic:
apply takeD_left

Premises used: List.takeD_left
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
p : α → Bool
l₂ : List α
⊢ loop p [] l₂ = (l₂.reverse ++ takeWhile p [], dropWhile p [])

Tactic:
simp [span.loop, takeWhile, dropWhile]

Premises used: List.span.loop, List.dropWhile, List.takeWhile
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
p : α → Bool
a : α
l l₂ : List α
false : ∀ (hp : p a = Bool.false), loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))
true : ∀ (hp : p a = Bool.true), loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))

Tactic:
cases hp : p a
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
p : α → Bool
a : α
l l₂ : List α
hp : p a = false
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))

Tactic:
simp [hp, span.loop, span.loop_eq_take_drop, takeWhile, dropWhile]

Premises used: List.span.loop, List.dropWhile, List.takeWhile
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
p : α → Bool
a : α
l l₂ : List α
hp : p a = true
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))

Tactic:
simp [hp, span.loop, span.loop_eq_take_drop, takeWhile, dropWhile]

Premises used: List.span.loop, List.dropWhile, List.takeWhile
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
p : α → Bool
l : List α
⊢ span p l = (takeWhile p l, dropWhile p l)

Tactic:
simpa using span.loop_eq_take_drop p l []

Premises used: _private.0.List.span.loop_eq_take_drop, List.nil
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
m : ℕ
⊢ dropSlice 0 m [] = HAppend.hAppend (α := List α) (take 0 []) (drop (0 + m) [])

Tactic:
grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
m : ℕ
head : α
tail : List α
⊢ dropSlice 0 m (head :: tail) = take 0 (head :: tail) ++ drop (0 + m) (head :: tail)

Tactic:
grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
m : ℕ
xs : List α
zero : dropSlice 0 m [] = HAppend.hAppend (α := List α) (take 0 []) (drop (0 + m) [])
zero₁ :
  ∀ (head : α) (tail : List α), dropSlice 0 m (head :: tail) = take 0 (head :: tail) ++ drop (0 + m) (head :: tail)
⊢ dropSlice 0 m xs = take 0 xs ++ drop (0 + m) xs

Tactic:
cases xs with grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
m n : ℕ
h : ∀ (xs : List α), dropSlice n m xs = take n xs ++ drop (n + m) xs
⊢ dropSlice (n + 1) m [] = HAppend.hAppend (α := List α) (take (n + 1) []) (drop (n + 1 + m) [])

Tactic:
grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
m n : ℕ
h : ∀ (xs : List α), dropSlice n m xs = take n xs ++ drop (n + m) xs
head : α
tail : List α
⊢ dropSlice (n + 1) m (head :: tail) = take (n + 1) (head :: tail) ++ drop (n + 1 + m) (head :: tail)

Tactic:
grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
m n : ℕ
h : ∀ (xs : List α), dropSlice n m xs = take n xs ++ drop (n + m) xs
xs : List α
succ : dropSlice (n + 1) m [] = HAppend.hAppend (α := List α) (take (n + 1) []) (drop (n + 1 + m) [])
succ₁ :
  ∀ (head : α) (tail : List α),
    dropSlice (n + 1) m (head :: tail) = take (n + 1) (head :: tail) ++ drop (n + 1 + m) (head :: tail)
⊢ dropSlice (n + 1) m xs = take (n + 1) xs ++ drop (n + 1 + m) xs

Tactic:
cases xs with grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
xs : List α
n m : ℕ
zero : ∀ (xs : List α), dropSlice 0 m xs = take 0 xs ++ drop (0 + m) xs
succ :
  ∀ (n : ℕ),
    (∀ (xs : List α), dropSlice n m xs = take n xs ++ drop (n + m) xs) →
      ∀ (xs : List α), dropSlice (n + 1) m xs = take (n + 1) xs ++ drop (n + 1 + m) xs
⊢ dropSlice n m xs = take n xs ++ drop (n + m) xs

Tactic:
induction n generalizing xs with cases xs with grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
j : ℕ
⊢ length.{u} (α := α) (dropSlice 0 j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - 0)

Tactic:
grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
j n : ℕ
⊢ length.{u} (α := α) (dropSlice (n + 1) j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - (n + 1))

Tactic:
grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
i j : ℕ
nil : length.{u} (α := α) (dropSlice 0 j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - 0)
nil₁ :
  ∀ (n : ℕ),
    length.{u} (α := α) (dropSlice (n + 1) j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - (n + 1))
⊢ length.{u} (α := α) (dropSlice i j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - i)

Tactic:
cases i with grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
head : α
tail : List α
tail_ih : ∀ (i j : ℕ), (dropSlice i j tail).length = tail.length - min j (tail.length - i)
j : ℕ
⊢ (dropSlice 0 j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - 0)

Tactic:
grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
head : α
tail : List α
tail_ih : ∀ (i j : ℕ), (dropSlice i j tail).length = tail.length - min j (tail.length - i)
j n : ℕ
⊢ (dropSlice (n + 1) j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - (n + 1))

Tactic:
grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
head : α
tail : List α
tail_ih : ∀ (i j : ℕ), (dropSlice i j tail).length = tail.length - min j (tail.length - i)
i j : ℕ
cons : (dropSlice 0 j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - 0)
cons₁ :
  ∀ (n : ℕ),
    (dropSlice (n + 1) j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - (n + 1))
⊢ (dropSlice i j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - i)

Tactic:
cases i with grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
i j : ℕ
xs : List α
nil : ∀ (i j : ℕ), length.{u} (α := α) (dropSlice i j []) = length.{u} (α := α) [] - min j (length.{u} (α := α) [] - i)
cons :
  ∀ (head : α) (tail : List α),
    (∀ (i j : ℕ), (dropSlice i j tail).length = tail.length - min j (tail.length - i)) →
      ∀ (i j : ℕ), (dropSlice i j (head :: tail)).length = (head :: tail).length - min j ((head :: tail).length - i)
⊢ (dropSlice i j xs).length = xs.length - min j (xs.length - i)

Tactic:
induction xs generalizing i j with cases i with grind [dropSlice]

Premises used: List.dropSlice
-- Module: Mathlib.Data.List.TakeDrop
Goal:
α : Type u
i j : ℕ
hj : 0 < j
xs : List α
hi : i < xs.length
⊢ (dropSlice i j xs).length < xs.length

Tactic:
grind
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
hl : 0 < (dropWhile p []).length
⊢ ¬p ((dropWhile p []).get (⟨0, hl⟩ : Fin (dropWhile p []).length)) = true

Tactic:
cases hl
-- Module: Mathlib.Data.List.TakeWhile
Goal:
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get (⟨0, hl⟩ : Fin (dropWhile p tl).length)) = true
hl : 0 < (dropWhile p (hd :: tl)).length
cons :
  ¬p
        (get
          (match (motive := Bool → List α) p hd with
          | true => dropWhile p tl
          | false => hd :: tl)
          (⟨0, hl⟩ :
            Fin
              (length.{u_1} (α := α)
                (match (motive := Bool → List α) p hd with
                | true => dropWhile p tl
                | false => hd :: tl)))) =
      true
⊢ ¬p ((dropWhile p (hd :: tl)).get (⟨0, hl⟩ : Fin (dropWhile p (hd :: tl)).length)) = true

Tactic:
simp only [dropWhile]

Premises used: List.dropWhile