awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
n m : ℕ
l : List α
rw : take n l ++ drop (n + m) l = take n l ++ drop m (drop n l)
⊢ dropSlice n m l = take n l ++ drop m (drop n l)
have rw₁ : take n l ++ drop (n + m) l = take n l ++ drop (n + m) l
Tactic: rw [dropSlice_eq, drop_drop, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
n m : ℕ
l : List α
rw : take n l ++ drop (n + m) l = take n l ++ drop m (drop n l)
rw₁ : take n l ++ drop (n + m) l = take n l ++ drop (n + m) l
⊢ dropSlice n m l = take n l ++ drop m (drop n l)
have rw₂ : take n l ++ drop (m + n) l = take n l ++ drop (m + n) l
Tactic: rw [dropSlice_eq, drop_drop, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] <+: y
have h₁ : x ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] ++ drop (x.length + 1) y = y
Tactic: use y.drop (x.length + 1)
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] ++ drop (x.length + 1) y = y
have h₁ : take x.length y ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] ++ drop (x.length + 1) y = y
Tactic: nth_rw 1 [List.prefix_iff_eq_take.mp h]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] ++ drop (x.length + 1) y = y
have h₁ : take x.length y ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] = take (x.length + 1) y
Tactic: convert! List.take_append_drop (x.length + 1) y using 2
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] = take (x.length + 1) y
have h₁ : take x.length y ++ [y.get (⟨x.length, hl⟩ : Fin y.length)] =
  take x.length y ++ [getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) y x.length hl]
Tactic: rw [← List.take_concat_get, List.concat_eq_append]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
head : α
tail : List α
ih : ∀ {l₁ : List α} (h : l₁ <+: tail), tail = l₁ ++ drop l₁.length tail
head_1 : α
tail_1 : List α
h : head_1 :: tail_1 <+: head :: tail
⊢ head :: tail = head_1 :: tail_1 ++ drop (head_1 :: tail_1).length (head :: tail)
have cons : ∀ (h' : tail_1 <+: tail) (h : head_1 :: tail_1 <+: head_1 :: tail),
  head_1 :: tail = head_1 :: tail_1 ++ drop (head_1 :: tail_1).length (head_1 :: tail)
Tactic: obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
Cleared hypotheses: head, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
head : α
tail : List α
ih : ∀ {l₁ : List α} (h : l₁ <+: tail), tail = l₁ ++ drop l₁.length tail
l₁ : List α
h : l₁ <+: head :: tail
⊢ head :: tail = l₁ ++ drop l₁.length (head :: tail)
have cons : ∀ (h : [] <+: head :: tail), head :: tail = [] ++ drop (length.{u_1} (α := α) []) (head :: tail)
Tactic: cases l₁ with
    | nil => rfl
    | cons =>
      obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
      simpa using ih h'
Cleared hypotheses: l₁, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
head : α
tail : List α
ih : ∀ {l₁ : List α} (h : l₁ <+: tail), tail = l₁ ++ drop l₁.length tail
l₁ : List α
h : l₁ <+: head :: tail
cons : ∀ (h : [] <+: head :: tail), head :: tail = [] ++ drop (length.{u_1} (α := α) []) (head :: tail)
⊢ head :: tail = l₁ ++ drop l₁.length (head :: tail)
have cons₁ : ∀ (head_1 : α) (tail_1 : List α) (h : head_1 :: tail_1 <+: head :: tail),
  head :: tail = head_1 :: tail_1 ++ drop (head_1 :: tail_1).length (head :: tail)
Tactic: cases l₁ with
    | nil => rfl
    | cons =>
      obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
      simpa using ih h'
Cleared hypotheses: l₁, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
⊢ l₂ = l₁ ++ drop l₁.length l₂
have nil : ∀ {l₁ : List α} (h : l₁ <+: []), [] = l₁ ++ drop l₁.length []
Tactic: induction l₂ generalizing l₁ with
  | nil => simp [List.prefix_nil.mp h]
  | cons _ _ ih =>
    cases l₁ with
    | nil => rfl
    | cons =>
      obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
      simpa using ih h'
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
nil : ∀ {l₁ : List α} (h : l₁ <+: []), [] = l₁ ++ drop l₁.length []
⊢ l₂ = l₁ ++ drop l₁.length l₂
have cons : ∀ (head : α) (tail : List α) (ih : ∀ {l₁ : List α} (h : l₁ <+: tail), tail = l₁ ++ drop l₁.length tail) {l₁ : List α}
  (h : l₁ <+: head :: tail), head :: tail = l₁ ++ drop l₁.length (head :: tail)
Tactic: induction l₂ generalizing l₁ with
  | nil => simp [List.prefix_nil.mp h]
  | cons _ _ ih =>
    cases l₁ with
    | nil => rfl
    | cons =>
      obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
      simpa using ih h'
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
x : α
xs : List α
⊢ [x] <:+: xs ↔ x ∈ xs
have rw : (∃ (s : List α), ∃ (t : List α), s ++ [x] ++ t = xs) ↔ ∃ (s : List α), ∃ (t : List α), xs = s ++ x :: t
Tactic: rw [List.mem_iff_append, List.IsInfix]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
x : α
xs : List α
⊢ (∃ (s : List α), ∃ (t : List α), s ++ [x] ++ t = xs) ↔ ∃ (s : List α), ∃ (t : List α), xs = s ++ x :: t
have a : ∀ (x_1 x_2 : List α), x_1 ++ [x] ++ x_2 = xs ↔ xs = x_1 ++ x :: x_2
Tactic: congr! 4
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
x y : α
⊢ [x] <:+: [y] ↔ x = y
have mp : [x] <:+: [y] → x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
x y : α
mp : [x] <:+: [y] → x = y
⊢ [x] <:+: [y] ↔ x = y
have mpr : x = y → [x] <:+: [y]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
xs : List α
x head head_1 : α
tail : List α
⊢ head :: head_1 :: tail <:+: [x] ↔ head :: head_1 :: tail = [] ∨ head :: head_1 :: tail = [x]
have mp : head :: head_1 :: tail <:+: [x] → head :: head_1 :: tail = [] ∨ head :: head_1 :: tail = [x]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
xs : List α
x head head_1 : α
tail : List α
mp : head :: head_1 :: tail <:+: [x] → head :: head_1 :: tail = [] ∨ head :: head_1 :: tail = [x]
⊢ head :: head_1 :: tail <:+: [x] ↔ head :: head_1 :: tail = [] ∨ head :: head_1 :: tail = [x]
have mpr : head :: head_1 :: tail = [] ∨ head :: head_1 :: tail = [x] → head :: head_1 :: tail <:+: [x]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
s_1 : List α
a : α
t : List α
o : s_1 = [] ∨ ∃ (l : List α), l ∈ t.inits ∧ a :: l = s_1
s r : List α
hr : r ∈ t.inits
hs : a :: r = s
⊢ s <+: a :: t
have let : ∀ (s_2 : List α) (ht : r ++ s_2 = t), s <+: a :: t
Tactic: let ⟨s, ht⟩ := (mem_inits _ _).1 hr
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
s_1 : List α
a : α
t : List α
o : s_1 = [] ∨ ∃ (l : List α), l ∈ t.inits ∧ a :: l = s_1
s_2 r : List α
hr : r ∈ t.inits
hs : a :: r = s_2
s : List α
ht : r ++ s = t
⊢ s_2 <+: a :: t
have rw : a :: r <+: a :: (r ++ s)
Tactic: rw [← hs, ← ht]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
s_1 : List α
a : α
t : List α
mi : s_1 <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
⊢ ∃ (l : List α), l ∈ t.inits ∧ a :: l = b :: s
have rw : ∃ (l : List α), l ∈ t.inits ∧ a :: l = a :: s
Tactic: rw [eq_of_heq ba]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
s : List α
a : α
t : List α
⊢ s ∈ (a :: t).tails ↔ s <:+ a :: t
have simp : s = a :: t ∨ s <:+ t ↔ s <:+ a :: t
Tactic: simp only [tails, mem_cons, mem_tails s t]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse l.tails).reverse
have rw : l.reverse.inits = (map reverse (map reverse l.reverse.inits).reverse).reverse
Tactic: rw [tails_eq_inits l]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
⊢ l.reverse.tails = (map reverse l.inits).reverse
have rw : l.reverse.tails = (map reverse (map reverse l.reverse.tails).reverse).reverse
Tactic: rw [inits_eq_tails l]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
⊢ map reverse l.inits = l.reverse.tails.reverse
have rw : map reverse (map reverse l.reverse.tails).reverse = l.reverse.tails.reverse
Tactic: rw [inits_eq_tails l]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
⊢ map reverse l.tails = l.reverse.inits.reverse
have rw : map reverse (map reverse l.reverse.inits).reverse = l.reverse.inits.reverse
Tactic: rw [tails_eq_inits l]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
⊢ l.tails.length = l.length + 1
have nil : length.{u_1} (α := List α) (tails []) = length.{u_1} (α := α) [] + 1
Tactic: induction l with
  | nil => simp
  | cons x l IH => simpa using IH
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
nil : length.{u_1} (α := List α) (tails []) = length.{u_1} (α := α) [] + 1
⊢ l.tails.length = l.length + 1
have cons : ∀ (x : α) (l : List α) (IH : l.tails.length = l.length + 1), (x :: l).tails.length = (x :: l).length + 1
Tactic: induction l with
  | nil => simp
  | cons x l IH => simpa using IH
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
a : α
l : List α
ihl :
  ∀ (n : ℕ) (h : n < l.tails.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.tails n h = drop n l
n : ℕ
h : n < (a :: l).tails.length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails n h = drop n (a :: l)
have cons : ∀ (h : 0 < (a :: l).tails.length),
  getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails 0 h = drop 0 (a :: l)
Tactic: cases n with
    | zero => simp
    | succ n => simp [ihl]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
a : α
l : List α
ihl :
  ∀ (n : ℕ) (h : n < l.tails.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.tails n h = drop n l
n : ℕ
h : n < (a :: l).tails.length
cons :
  ∀ (h : 0 < (a :: l).tails.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails 0 h = drop 0 (a :: l)
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails n h = drop n (a :: l)
have cons₁ : ∀ (n : ℕ) (h : n + 1 < (a :: l).tails.length),
  getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails (n + 1) h = drop (n + 1) (a :: l)
Tactic: cases n with
    | zero => simp
    | succ n => simp [ihl]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.tails.length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.tails n h = drop n l
have nil : ∀ (n : ℕ) (h : n < length.{u_1} (α := List α) (tails [])),
  getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tails []) n h = drop n []
Tactic: induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]
Cleared hypotheses: l, n, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.tails.length
nil :
  ∀ (n : ℕ) (h : n < length.{u_1} (α := List α) (tails [])),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tails []) n h = drop n []
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.tails n h = drop n l
have cons : ∀ (a : α) (l : List α)
  (ihl :
    ∀ (n : ℕ) (h : n < l.tails.length),
      getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.tails n h = drop n l)
  (n : ℕ) (h : n < (a :: l).tails.length),
  getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails n h = drop n (a :: l)
Tactic: induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]
Cleared hypotheses: l, n, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
a : α
l : List α
ihl :
  ∀ (n : ℕ) (h : n < l.inits.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.inits n h = take n l
n : ℕ
h : n < (a :: l).inits.length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits n h = take n (a :: l)
have cons : ∀ (h : 0 < (a :: l).inits.length),
  getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits 0 h = take 0 (a :: l)
Tactic: cases n with
    | zero => simp
    | succ n => simp [ihl]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
a : α
l : List α
ihl :
  ∀ (n : ℕ) (h : n < l.inits.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.inits n h = take n l
n : ℕ
h : n < (a :: l).inits.length
cons :
  ∀ (h : 0 < (a :: l).inits.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits 0 h = take 0 (a :: l)
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits n h = take n (a :: l)
have cons₁ : ∀ (n : ℕ) (h : n + 1 < (a :: l).inits.length),
  getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits (n + 1) h = take (n + 1) (a :: l)
Tactic: cases n with
    | zero => simp
    | succ n => simp [ihl]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.inits.length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.inits n h = take n l
have nil : ∀ (n : ℕ) (h : n < length.{u_1} (α := List α) (inits [])),
  getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (inits []) n h = take n []
Tactic: induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]
Cleared hypotheses: l, n, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.inits.length
nil :
  ∀ (n : ℕ) (h : n < length.{u_1} (α := List α) (inits [])),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (inits []) n h = take n []
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.inits n h = take n l
have cons : ∀ (a : α) (l : List α)
  (ihl :
    ∀ (n : ℕ) (h : n < l.inits.length),
      getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.inits n h = take n l)
  (n : ℕ) (h : n < (a :: l).inits.length),
  getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits n h = take n (a :: l)
Tactic: induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]
Cleared hypotheses: l, n, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).inits = map (map g) l.inits
have nil : (map g []).inits = map (map g) (inits [])
Tactic: induction l using reverseRecOn
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
β : Type u_3
g : α → β
nil : (map g []).inits = map (map g) (inits [])
⊢ (map g l).inits = map (map g) l.inits
have append_singleton : ∀ (l : List α) (a : α), (map g l).inits = map (map g) l.inits → (map g (l ++ [a])).inits = map (map g) (l ++ [a]).inits
Tactic: induction l using reverseRecOn
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).tails = map (map g) l.tails
have nil : (map g []).tails = map (map g) (tails [])
Tactic: induction l using reverseRecOn
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
β : Type u_3
g : α → β
nil : (map g []).tails = map (map g) (tails [])
⊢ (map g l).tails = map (map g) l.tails
have append_singleton : ∀ (l : List α) (a : α), (map g l).tails = map (map g) l.tails → (map g (l ++ [a])).tails = map (map g) (l ++ [a]).tails
Tactic: induction l using reverseRecOn
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits = take (n + 1) l.inits
have hl : (take n l).inits.length = (take (n + 1) l.inits).length
Tactic: apply ext_getElem
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
hl : (take n l).inits.length = (take (n + 1) l.inits).length
⊢ (take n l).inits = take (n + 1) l.inits
have h : ∀ (i : ℕ) (h₁ : i < (take n l).inits.length) (h₂ : i < (take (n + 1) l.inits).length),
  getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take n l).inits i h₁ =
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take (n + 1) l.inits) i h₂
Tactic: apply ext_getElem
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (take n l).inits.length) (h₂ : i < (take (n + 1) l.inits).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take n l).inits i h₁ =
      getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take (n + 1) l.inits) i h₂
have h : ∀ (i : ℕ) (h₂ : i < min n l.length + 1), min i (min n l.length) = min i l.length
Tactic: simp [take_take]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ insert a l = if a ∈ l then l else a :: l
have simp : insert a l = if elem a l = true then l else a :: l
Tactic: simp only [← elem_iff]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ l <:+ List.insert a l
have pos : ∀ (h : a ∈ l), l <:+ List.insert a l
Tactic: by_cases h : a ∈ l
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
pos : ∀ (h : a ∈ l), l <:+ List.insert a l
⊢ l <:+ List.insert a l
have neg : ∀ (h : ¬a ∈ l), l <:+ List.insert a l
Tactic: by_cases h : a ∈ l
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
l : List α
n : ℕ
hn : n ≠ l.length
a : α
⊢ (l.eraseIdx n).insertIdx n a = l.set n a
have zero : ∀ {l : List α} (hn : 0 ≠ l.length), (l.eraseIdx 0).insertIdx 0 a = l.set 0 a
Tactic: induction n generalizing l
Cleared hypotheses: l, n, hn
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
l : List α
n : ℕ
hn : n ≠ l.length
a : α
zero : ∀ {l : List α} (hn : 0 ≠ l.length), (l.eraseIdx 0).insertIdx 0 a = l.set 0 a
⊢ (l.eraseIdx n).insertIdx n a = l.set n a
have succ : ∀ (n : ℕ),
  (∀ {l : List α} (hn : n ≠ l.length), (l.eraseIdx n).insertIdx n a = l.set n a) →
    ∀ {l : List α} (hn : n + 1 ≠ l.length), (l.eraseIdx (n + 1)).insertIdx (n + 1) a = l.set (n + 1) a
Tactic: induction n generalizing l
Cleared hypotheses: l, n, hn
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
a : α
l : List α
hn : 0 ≠ l.length
⊢ (l.eraseIdx 0).insertIdx 0 a = l.set 0 a
have zero : ∀ (hn : 0 ≠ length.{u} (α := α) []), insertIdx (eraseIdx [] 0) 0 a = set [] 0 a
Tactic: cases l
Cleared hypotheses: l, hn
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
a : α
l : List α
hn : 0 ≠ l.length
zero : ∀ (hn : 0 ≠ length.{u} (α := α) []), insertIdx (eraseIdx [] 0) 0 a = set [] 0 a
⊢ (l.eraseIdx 0).insertIdx 0 a = l.set 0 a
have zero₁ : ∀ (head : α) (tail : List α) (hn : 0 ≠ (head :: tail).length),
  ((head :: tail).eraseIdx 0).insertIdx 0 a = (head :: tail).set 0 a
Tactic: cases l
Cleared hypotheses: l, hn
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {l : List α} (hn : n ≠ l.length), (l.eraseIdx n).insertIdx n a = l.set n a
l : List α
hn : n + 1 ≠ l.length
⊢ (l.eraseIdx (n + 1)).insertIdx (n + 1) a = l.set (n + 1) a
have succ : ∀ (hn : n + 1 ≠ length.{u} (α := α) []), insertIdx (eraseIdx [] (n + 1)) (n + 1) a = set [] (n + 1) a
Tactic: cases l
Cleared hypotheses: l, hn
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {l : List α} (hn : n ≠ l.length), (l.eraseIdx n).insertIdx n a = l.set n a
l : List α
hn : n + 1 ≠ l.length
succ : ∀ (hn : n + 1 ≠ length.{u} (α := α) []), insertIdx (eraseIdx [] (n + 1)) (n + 1) a = set [] (n + 1) a
⊢ (l.eraseIdx (n + 1)).insertIdx (n + 1) a = l.set (n + 1) a
have succ₁ : ∀ (head : α) (tail : List α) (hn : n + 1 ≠ (head :: tail).length),
  ((head :: tail).eraseIdx (n + 1)).insertIdx (n + 1) a = (head :: tail).set (n + 1) a
Tactic: cases l
Cleared hypotheses: l, hn
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (hypothesis)
Goal:
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
hn : l.length < n
⊢ a = b ∨ a ∈ l
have h₁ : a ∈ l
Tactic: rw [insertIdx_of_length_lt hn] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
hn : l.length ≥ n
⊢ a = b ∨ a ∈ l
have inr : ∀ (h : a = b ∨ a ∈ l) (hn : l.length ≥ n), a = b ∨ a ∈ l
Tactic: rwa [mem_insertIdx hn] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (hypothesis)
Goal:
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
⊢ a = b ∨ a ∈ l
have x : l.length < n ∨ l.length ≥ n
Tactic: cases Nat.lt_or_ge (length l) n with
  | inl hn =>
    rw [insertIdx_of_length_lt hn] at h
    exact .inr h
  | inr hn =>
    rwa [mem_insertIdx hn] at h
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
l : List α
hl : ∀ (x : α), x ∈ l → p x
⊢ (pmap (P := p) f l hl).insertIdx 0 (f a ha) = pmap (P := p) f (l.insertIdx 0 a) ⋯
have zero : ∀ (hl : ∀ (x : α), Membership.mem (γ := List α) [] x → p x),
  (pmap (P := p) f [] hl).insertIdx 0 (f a ha) = pmap (P := p) f (insertIdx [] 0 a) sorry
Tactic: cases l
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
l : List α
hl : ∀ (x : α), x ∈ l → p x
zero :
  ∀ (hl : ∀ (x : α), Membership.mem (γ := List α) [] x → p x),
    (pmap (P := p) f [] hl).insertIdx 0 (f a ha) = pmap (P := p) f (insertIdx [] 0 a) ⋯
⊢ (pmap (P := p) f l hl).insertIdx 0 (f a ha) = pmap (P := p) f (l.insertIdx 0 a) ⋯
have zero₁ : ∀ (head : α) (tail : List α) (hl : ∀ (x : α), x ∈ head :: tail → p x),
  (pmap (P := p) f (head :: tail) hl).insertIdx 0 (f a ha) = pmap (P := p) f ((head :: tail).insertIdx 0 a) sorry
Tactic: cases l
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.InsertIdx (goal)
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn :
  ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
    (pmap (P := p) f l hl).insertIdx n (f a ha) = pmap (P := p) f (l.insertIdx n a) ⋯
l : List α
hl : ∀ (x : α), x ∈ l → p x
⊢ (pmap (P := p) f l hl).insertIdx (n + 1) (f a ha) = pmap (P := p) f (l.insertIdx (n + 1) a) ⋯
have succ : ∀ (hl : ∀ (x : α), Membership.mem (γ := List α) [] x → p x),
  (pmap (P := p) f [] hl).insertIdx (n + 1) (f a ha) = pmap (P := p) f (insertIdx [] (n + 1) a) sorry
Tactic: cases l
Cleared hypotheses: l, hl