awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
Rₐ : α → α → Prop
l₁ l₂ : List α
h : l₁ <+ l₂
inst : Std.Refl Rₐ
⊢ SublistForall₂ Rₐ l₁ l₂

Tactic:
sublistForall₂_iff.2 ⟨l₁, forall₂_refl l₁, h⟩

Premises used: Iff.mpr, List.forall₂_refl, And.intro, List.sublistForall₂_iff, Exists.intro
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
Rₐ : α → α → Prop
inst : Std.Refl Rₐ
l : List α
⊢ SublistForall₂ Rₐ l.tail l

Tactic:
l.tail_sublist.sublistForall₂

Premises used: List.tail_sublist, List.Sublist.sublistForall₂
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → α
l₁ : List γ
l₂ : List β
⊢ SublistForall₂ R (map f l₁) l₂ ↔ SublistForall₂ (fun (c : γ) (b : β) ↦ R (f c) b) l₁ l₂

Tactic:
simp [sublistForall₂_iff]

Premises used: List.sublistForall₂_iff
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
simp :
  (∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂) ↔
    ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l₂

Tactic:
simp only [sublistForall₂_iff]

Premises used: List.sublistForall₂_iff
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
mp :
  (∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂) →
    ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂
mpr :
  (∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂) →
    ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂
⊢ (∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂) ↔
    ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
constructor
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
l1 : List β
h1 : Forall₂ R l₁ l1
h2 : l1 <+ map f l₂
mp :
  ∀ (l' : List γ) (hl1 : l' <+ l₂) (h1 : Forall₂ R l₁ (map f l')) (h2 : map f l' <+ map f l₂),
    ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂
⊢ ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
obtain ⟨l', hl1, rfl⟩ := sublist_map_iff.mp h2

Premises used: List.sublist_map_iff, Iff.mp, rfl
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l' : List γ
hl1 : l' <+ l₂
h1 : Forall₂ R l₁ (map f l')
h2 : map f l' <+ map f l₂
h : Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l' ∧ l' <+ l₂
⊢ ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
use l'
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l' : List γ
hl1 : l' <+ l₂
h1 : Forall₂ R l₁ (map f l')
h2 : map f l' <+ map f l₂
⊢ Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l' ∧ l' <+ l₂

Tactic:
simpa [hl1] using h1
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l1 : List γ
h1 : Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l1
h2 : l1 <+ l₂
h : Forall₂ R l₁ (map f l1) ∧ map f l1 <+ map f l₂
⊢ ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂

Tactic:
use l1.map f

Premises used: List.map
-- Module: Mathlib.Data.List.Forall2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l1 : List γ
h1 : Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l1
h2 : l1 <+ l₂
⊢ Forall₂ R l₁ (map f l1) ∧ map f l1 <+ map f l₂

Tactic:
simp [h1, h2.map]

Premises used: List.Sublist.map
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
d : α
n : ℕ
hn : n < l.length
⊢ l.getD n d = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn

Tactic:
grind
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
β : Type v
l : List α
x : α
xs : List α
n : ℕ
d : α
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.GetD
Goal:
α : Type u
l : List α
d : α
i : Fin l.length
⊢ l.getD (↑i : ℕ) d = (getElem? (valid := fun (xs : List α) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i).get ⋯

Tactic:
simp only [getD_eq_getElem?_getD, Fin.is_lt, getElem?_pos, Option.getD_some, Fin.getElem_fin,
    Option.get_some]

Premises used: Option.get_some, Option.getD_some, Fin.is_lt, getElem?_pos, Fin.getElem_fin, List.getD_eq_getElem?_getD
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
d : α
i : Fin l.length
⊢ l.getD (↑i : ℕ) d = l.get i

Tactic:
getD_eq_getElem ..

Premises used: List.getD_eq_getElem
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
β : Type v
l : List α
d : α
n : ℕ
f : α → β
⊢ (map f l).getD n (f d) = f (l.getD n d)

Tactic:
simp only [getD_eq_getElem?_getD, getElem?_map, Option.getD_map]

Premises used: List.getElem?_map, Option.getD_map, List.getD_eq_getElem?_getD
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
d : α
n : ℕ
hn : l.length ≤ n
⊢ l.getD n d = d

Tactic:
grind
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
i : ℕ
h : i < l.length
⊢ l.reverse.getD i = l.getD (l.length - 1 - i)

Tactic:
grind
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
d : α
n : ℕ
⊢ (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [d] n).getD d = d

Tactic:
grind
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
d : α
r n : ℕ
⊢ (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (replicate r d) n).getD d = d

Tactic:
grind
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
x y : α
i n : ℕ
h : i < n
⊢ (replicate n x).getD i y = x

Tactic:
grind
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l l' : List α
d : α
n : ℕ
h : n < l.length
⊢ (l ++ l').getD n d = l.getD n d

Tactic:
grind
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l l' : List α
d : α
n : ℕ
h : l.length ≤ n
⊢ (l ++ l').getD n d = l'.getD (n - l.length) d

Tactic:
grind
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
d : α
h : ∀ (a : α), (∃ (a_1 : ℕ), (fun (x : ℕ) ↦ l.getD x d) a_1 = a) ↔ a = d ∨ a ∈ l
⊢ (Function.Surjective.{1, u + 1} (β := α) fun (x : ℕ) ↦ l.getD x d) ↔ ∀ (x : α), x = d ∨ x ∈ l

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
d : α
⊢ ∃ (x : ℕ), l.length ≤ x

Tactic:
have : ∃ x, l.length ≤ x := ⟨_, Nat.le_refl _⟩
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
d : α
this : ∃ (x : ℕ), l.length ≤ x
h :
  ∀ (a : α),
    (∃ (x : ℕ), ∃ (h : x < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x h = a) ∨
        True ∧ d = a ↔
      a = d ∨ ∃ (x : ℕ), ∃ (h : x < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x h = a
⊢ ∀ (a : α), (∃ (a_1 : ℕ), (fun (x : ℕ) ↦ l.getD x d) a_1 = a) ↔ a = d ∨ a ∈ l

Tactic:
simp only [getD_eq_getElem?_getD, getD_getElem?, dite_eq_iff, Nat.not_lt, exists_prop, exists_or,
    exists_and_right, this, mem_iff_getElem?, getElem?_eq_some_iff]

Premises used: exists_or, List.getElem?_eq_some_iff, Nat.not_lt, exists_and_right, exists_prop, List.mem_iff_getElem?, List.getD_getElem?, dite_eq_iff, List.getD_eq_getElem?_getD
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
d : α
this : ∃ (x : ℕ), l.length ≤ x
⊢ ∀ (a : α),
    (∃ (x : ℕ), ∃ (h : x < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x h = a) ∨
        True ∧ d = a ↔
      a = d ∨ ∃ (x : ℕ), ∃ (h : x < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x h = a

Tactic:
grind
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
d : α
⊢ Function.Surjective.{1, u + 1} (β := α) fun (x : ℕ) ↦ l.getD x d

Tactic:
getD_surjective_iff.mpr fun _ ↦ .inr <| h _

Premises used: Iff.mpr, List.getD_surjective_iff, Or.inr
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
n : ℕ
inst : Inhabited α
⊢ Eq.{u + 1} (α := α) (getI [] n) default

Tactic:
rfl

Premises used: Option.getD, List.getD, List.getI, rfl
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
x : α
xs : List α
inst : Inhabited α
⊢ (x :: xs).getI 0 = x

Tactic:
rfl

Premises used: Option.getD, List.getD, List.getI, rfl
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
x : α
xs : List α
n : ℕ
inst : Inhabited α
⊢ (x :: xs).getI (n + 1) = xs.getI n

Tactic:
rfl

Premises used: List.getD, List.get?Internal, List.getI, rfl
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
inst : Inhabited α
n : ℕ
hn : n < l.length
⊢ l.getI n = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn

Tactic:
getD_eq_getElem l default hn

Premises used: Inhabited.default, List.getD_eq_getElem, List.getI
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
inst : Inhabited α
n : ℕ
hn : l.length ≤ n
⊢ l.getI n = default

Tactic:
getD_eq_default _ _ hn

Premises used: List.getD_eq_default, List.getI
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
inst : Inhabited α
n : ℕ
⊢ l.getD n default = l.getI n

Tactic:
rfl

Premises used: List.getI, rfl
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
inst : Inhabited α
l l' : List α
n : ℕ
h : n < l.length
⊢ (l ++ l').getI n = l.getI n

Tactic:
getD_append _ _ _ _ h

Premises used: List.getD_append, List.getI
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
inst : Inhabited α
l l' : List α
n : ℕ
h : l.length ≤ n
⊢ (l ++ l').getI n = l'.getI (n - l.length)

Tactic:
getD_append_right _ _ _ _ h

Premises used: List.getD_append_right, List.getI
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
inst : Inhabited α
n : ℕ
rw : l.getD n default = (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD default
rw₁ rw₂ :
  (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD default =
    (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD default
⊢ l.getI n = (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD default

Tactic:
rw [← getD_default_eq_getI, getD_eq_getElem?_getD]

Premises used: List.getD_default_eq_getI, List.getD_eq_getElem?_getD
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
inst : Inhabited α
n : ℕ
⊢ l.getI n = (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD default

Tactic:
getI_eq_getElem?_getD (l := l) n

Premises used: List.getI_eq_getElem?_getD
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
l : List α
inst : Inhabited α
nil : Eq.{u + 1} (α := α) (getI [] 0) (headI [])
cons : ∀ (head : α) (tail : List α), (head :: tail).getI 0 = (head :: tail).headI
⊢ l.getI 0 = l.headI

Tactic:
cases l
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
inst : Inhabited α
⊢ Eq.{u + 1} (α := α) (getI [] 0) (headI [])

Tactic:
rfl
-- Module: Mathlib.Data.List.GetD
Goal:
α : Type u
inst : Inhabited α
head : α
tail : List α
⊢ (head :: tail).getI 0 = (head :: tail).headI

Tactic:
rfl
-- Module: Mathlib.Data.List.Indexes
Goal:
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e]

Tactic:
mapIdx_concat

Premises used: List.mapIdx_concat
-- Module: Mathlib.Data.List.Indexes
Goal:
α : Type u
β : Type v
f : ℕ → α → β
⊢ mapIdx f [] = ofFn (n := length.{u} (α := α) []) fun (i : Fin (length.{u} (α := α) [])) ↦ f (↑i : ℕ) (get [] i)

Tactic:
simp
-- Module: Mathlib.Data.List.Indexes
Goal:
α : Type u
β : Type v
head : α
tail : List α
IH : ∀ (f : ℕ → α → β), mapIdx f tail = ofFn (n := tail.length) fun (i : Fin tail.length) ↦ f (↑i : ℕ) (tail.get i)
f : ℕ → α → β
⊢ mapIdx f (head :: tail) =
    ofFn (n := (head :: tail).length) fun (i : Fin (head :: tail).length) ↦ f (↑i : ℕ) ((head :: tail).get i)

Tactic:
simp [IH]
-- Module: Mathlib.Data.List.Indexes
Goal:
α : Type u
β : Type v
l : List α
f : ℕ → α → β
nil :
  ∀ (f : ℕ → α → β),
    mapIdx f [] = ofFn (n := length.{u} (α := α) []) fun (i : Fin (length.{u} (α := α) [])) ↦ f (↑i : ℕ) (get [] i)
cons :
  ∀ (head : α) (tail : List α)
    (IH :
      ∀ (f : ℕ → α → β), mapIdx f tail = ofFn (n := tail.length) fun (i : Fin tail.length) ↦ f (↑i : ℕ) (tail.get i))
    (f : ℕ → α → β),
    mapIdx f (head :: tail) =
      ofFn (n := (head :: tail).length) fun (i : Fin (head :: tail).length) ↦ f (↑i : ℕ) ((head :: tail).get i)
⊢ mapIdx f l = ofFn (n := l.length) fun (i : Fin l.length) ↦ f (↑i : ℕ) (l.get i)

Tactic:
induction l generalizing f with
  | nil => simp
  | cons _ _ IH => simp [IH]

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Indexes
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
arr : Array PUnit
⊢ mapIdxMAux' f arr.size [] = mapIdxM.go f [] arr *> pure PUnit.unit

Tactic:
simp only [mapIdxMAux', mapIdxM.go, seqRight_eq, map_pure, seq_pure]

Premises used: LawfulApplicative.seq_pure, List.mapIdxM.go, List.mapIdxMAux', LawfulApplicative.seqRight_eq, LawfulApplicative.map_pure
-- Module: Mathlib.Data.List.Indexes
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
cons :
  Eq (α := m PUnit)
    (do
      f arr.size head
      mapIdxMAux' f (arr.size + 1) tail)
    do
    let x ← f arr.size head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)
⊢ mapIdxMAux' f arr.size (head :: tail) = mapIdxM.go f (head :: tail) arr *> pure PUnit.unit

Tactic:
simp only [mapIdxMAux', seqRight_eq, map_eq_pure_bind, seq_eq_bind_map, bind_pure_unit,
      LawfulMonad.bind_assoc, pure_bind, mapIdxM.go]

Premises used: LawfulMonad.bind_assoc, List.mapIdxM.go, bind_pure_unit, List.mapIdxMAux', LawfulApplicative.seqRight_eq, LawfulMonad.pure_bind, map_eq_pure_bind, seq_eq_bind_map
-- Module: Mathlib.Data.List.Indexes
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
cons :
  ∀ (head : m PUnit),
    Eq (α := m PUnit)
      (do
        head
        mapIdxMAux' f (arr.size + 1) tail)
      do
      let x ← head
      let x ← mapIdxM.go f tail (arr.push x)
      pure (const (List PUnit) id x PUnit.unit)
⊢ Eq (α := m PUnit)
    (do
      f arr.size head
      mapIdxMAux' f (arr.size + 1) tail)
    do
    let x ← f arr.size head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)

Tactic:
generalize (f (Array.size arr) head) = head

Premises used: Array.size
-- Module: Mathlib.Data.List.Indexes
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head_1 : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
⊢ (arr.push PUnit.unit).size = arr.size + 1

Tactic:
have : (arr.push ⟨⟩).size = arr.size + 1 := Array.size_push _
-- Module: Mathlib.Data.List.Indexes
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head_1 : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
this : (arr.push PUnit.unit).size = arr.size + 1
cons :
  Eq (α := m PUnit)
    (do
      head
      mapIdxM.go f tail (arr.push PUnit.unit) *> pure PUnit.unit)
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)
⊢ Eq (α := m PUnit)
    (do
      head
      mapIdxMAux' f (arr.size + 1) tail)
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)

Tactic:
rw [← this, ih]
-- Module: Mathlib.Data.List.Indexes
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head_1 : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ Eq (α := m PUnit)
    (do
      head
      mapIdxM.go f tail (arr.push PUnit.unit) *> pure PUnit.unit)
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)

Tactic:
simp only [seqRight_eq, map_eq_pure_bind, seq_pure, LawfulMonad.bind_assoc, pure_bind]

Premises used: LawfulMonad.bind_assoc, LawfulApplicative.seq_pure, LawfulApplicative.seqRight_eq, LawfulMonad.pure_bind, map_eq_pure_bind
-- Module: Mathlib.Data.List.Indexes
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
arr : Array PUnit
nil : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size [] = mapIdxM.go f [] arr *> pure PUnit.unit
cons :
  ∀ (head : α) (tail : List α)
    (ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit)
    (arr : Array PUnit), mapIdxMAux' f arr.size (head :: tail) = mapIdxM.go f (head :: tail) arr *> pure PUnit.unit
⊢ mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit

Tactic:
induction as generalizing arr with
  | nil => simp only [mapIdxMAux', mapIdxM.go, seqRight_eq, map_pure, seq_pure]
  | cons head tail ih =>
    simp only [mapIdxMAux', seqRight_eq, map_eq_pure_bind, seq_eq_bind_map, bind_pure_unit,
      LawfulMonad.bind_assoc, pure_bind, mapIdxM.go]
    generalize (f (Array.size arr) head) = head
    have : (arr.push ⟨⟩).size = arr.size + 1 := Array.size_push _
    rw [← this, ih]
    simp only [seqRight_eq, map_eq_pure_bind, seq_pure, LawfulMonad.bind_assoc, pure_bind]

Premises used: List.head, LawfulMonad.bind_assoc, List.tail, List.cons, LawfulApplicative.seq_pure, List.mapIdxM.go, bind_pure_unit, List.mapIdxMAux', LawfulApplicative.seqRight_eq, LawfulMonad.pure_bind, LawfulApplicative.map_pure, map_eq_pure_bind, seq_eq_bind_map, List.nil
-- Module: Mathlib.Data.List.Indexes
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
⊢ mapIdxM' f as = mapIdxM f as *> pure PUnit.unit

Tactic:
mapIdxMAux'_eq_mapIdxMGo f as #[]

Premises used: List.mapIdxMAux'_eq_mapIdxMGo, List.mapIdxM', List.toArray, List.nil
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : List α → Sort u_2
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ reverseRec (motive := fun (x : List α) ↦ motive x) nil append_singleton [] = nil

Tactic:
grind [reverseRec]
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ reverseRec (motive := fun (x : List α) ↦ motive x) nil append_singleton (xs ++ [x]) =
    append_singleton xs x (reverseRec (motive := fun (x : List α) ↦ motive x) nil append_singleton xs)

Tactic:
grind [reverseRec, cases List]

Premises used: List
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : List α → Sort u_2
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ reverseRecOn (motive := fun (x : List α) ↦ motive x) [] nil append_singleton = nil

Tactic:
simp
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ reverseRecOn (motive := fun (x : List α) ↦ motive x) (xs ++ [x]) nil append_singleton =
    append_singleton xs x (reverseRecOn (motive := fun (x : List α) ↦ motive x) xs nil append_singleton)

Tactic:
simp
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
⊢ bidirectionalRec (motive := fun (x : List α) ↦ motive x) nil singleton cons_append [] = nil

Tactic:
grind [bidirectionalRec]
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a : α
⊢ bidirectionalRec (motive := fun (x : List α) ↦ motive x) nil singleton cons_append [a] = singleton a

Tactic:
grind [bidirectionalRec]
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a : α
l : List α
b : α
⊢ bidirectionalRec (motive := motive) nil singleton cons_append (a :: (l ++ [b])) =
    cons_append a l b (bidirectionalRec (motive := fun (x : List α) ↦ motive x) nil singleton cons_append l)

Tactic:
grind [bidirectionalRec, cases List]

Premises used: List
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : (l : List α) → l ≠ [] → Sort u_2
x : α
singleton : (x : α) → motive [x] ⋯
cons : (x : α) → (xs : List α) → (h : xs ≠ []) → motive xs h → motive (x :: xs) ⋯
⊢ recNeNil (motive := fun (x : List α) (x_1 : x ≠ []) ↦ motive x x_1) singleton cons [x] ⋯ = singleton x

Tactic:
rfl

Premises used: List.recNeNil, rfl
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : (l : List α) → l ≠ [] → Sort u_2
x : α
xs : List α
h : xs ≠ []
singleton : (x : α) → motive [x] ⋯
cons : (x : α) → (xs : List α) → (h : xs ≠ []) → motive xs h → motive (x :: xs) ⋯
⊢ recNeNil (motive := fun (x : List α) (x_1 : x ≠ []) ↦ motive x x_1) singleton cons (x :: xs) ⋯ =
    cons x xs h (recNeNil (motive := fun (x : List α) (x_1 : x ≠ []) ↦ motive x x_1) singleton cons xs h)

Tactic:
match xs with
  | _ :: _ => rfl

Premises used: List.recNeNil, List.cons, List.cons_ne_nil, Eq, rfl, _private.0.List.recNeNil_cons.match_1
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : (l : List α) → Sort u_2
nil : motive []
singleton : (x : α) → motive [x]
cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)
⊢ twoStepInduction (motive := fun (x : List α) ↦ motive x) nil singleton cons_cons [] = nil

Tactic:
twoStepInduction.eq_1 ..

Premises used: List.twoStepInduction.eq_1
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : (l : List α) → Sort u_2
x : α
nil : motive []
singleton : (x : α) → motive [x]
cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)
⊢ twoStepInduction (motive := fun (x : List α) ↦ motive x) nil singleton cons_cons [x] = singleton x

Tactic:
twoStepInduction.eq_2 ..

Premises used: List.twoStepInduction.eq_2
-- Module: Mathlib.Data.List.Induction
Goal:
α : Type u_1
motive : (l : List α) → Sort u_2
x y : α
xs : List α
nil : motive []
singleton : (x : α) → motive [x]
cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)
⊢ twoStepInduction (motive := fun (x : List α) ↦ motive x) nil singleton cons_cons (x :: y :: xs) =
    cons_cons x y xs (twoStepInduction (motive := fun (x : List α) ↦ motive x) nil singleton cons_cons xs) fun (y : α) ↦
      twoStepInduction (motive := fun (x : List α) ↦ motive x) nil singleton cons_cons (y :: xs)

Tactic:
twoStepInduction.eq_3 ..

Premises used: List.twoStepInduction.eq_3
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take n l₁ <+: List.take n l₂

Tactic:
simpa [prefix_take_iff, Nat.min_le_left] using (take_prefix n l₁).trans h

Premises used: List.IsPrefix.trans, Nat.min_le_left, List.take_prefix, List.prefix_take_iff
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
rw : List.take (l₁.length - n) (List.drop n l₂) <+: List.drop n l₂
⊢ List.drop n l₁ <+: List.drop n l₂

Tactic:
rw [prefix_iff_eq_take.mp h, drop_take]

Premises used: List.prefix_iff_eq_take, List.drop_take, Iff.mp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take (l₁.length - n) (List.drop n l₂) <+: List.drop n l₂

Tactic:
apply take_prefix

Premises used: List.take_prefix