awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a head : α
tail : List α
⊢ idxOf a (head :: tail) = 0 ↔ head :: tail = [] ∨ (head :: tail).head? = some a

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
hl : l ≠ []
a : α
⊢ idxOf a l = 0 ↔ l.head hl = a

Tactic:
simp [hl, idxOf_eq_zero_iff_eq_nil_or_head_eq, head?_eq_some_head]

Premises used: List.head?_eq_some_head, List.idxOf_eq_zero_iff_eq_nil_or_head_eq
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
a : α
h : a ∈ l₁
⊢ idxOf a (l₁ ++ l₂) = idxOf a l₁

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
a : α
h : ¬a ∈ l₁
⊢ idxOf a (l₁ ++ l₂) = l₁.length + idxOf a l₂

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
obtain : ∀ (l₃ : List α), idxOf a l₁ ≤ idxOf a (l₁ ++ l₃)
⊢ idxOf a l₁ ≤ idxOf a l₂

Tactic:
obtain ⟨l₃, rfl⟩ := hl

Premises used: rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ : List α
inst : BEq α
inst_1 : LawfulBEq α
a : α
l₃ : List α
⊢ idxOf a l₁ ≤ idxOf a (l₁ ++ l₃)

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
ha : a ∈ l₁
obtain : ∀ (l₃ : List α), idxOf a l₁ = idxOf a (l₁ ++ l₃)
⊢ idxOf a l₁ = idxOf a l₂

Tactic:
obtain ⟨l₃, rfl⟩ := hl

Premises used: rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ : List α
inst : BEq α
inst_1 : LawfulBEq α
a : α
ha : a ∈ l₁
l₃ : List α
⊢ idxOf a l₁ = idxOf a (l₁ ++ l₃)

Tactic:
idxOf_append_of_mem ha |>.symm

Premises used: List.idxOf_append_of_mem, Eq.symm
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ : List α
inst : BEq α
inst_1 : LawfulBEq α
a : α
ha : a ∈ l₁
l₃ : List α
⊢ idxOf a l₁ = idxOf a (l₁ ++ l₃)

Tactic:
exact idxOf_append_of_mem ha |>.symm

Premises used: List.idxOf_append_of_mem, Eq.symm
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
⊢ a ∈ l₁ ↔ idxOf a l₂ < l₁.length

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
refine_1 : ∀ (h : a ∈ l₁), idxOf a l₂ < l₁.length
refine_2 : ∀ (h : idxOf a l₂ < l₁.length), a ∈ l₁
⊢ a ∈ l₁ ↔ idxOf a l₂ < l₁.length

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : a ∈ l₁
⊢ idxOf a l₂ < l₁.length

Tactic:
hl.idxOf_eq_of_mem h ▸ idxOf_lt_length_of_mem h

Premises used: List.idxOf_lt_length_of_mem, Eq.rec, List.IsPrefix.idxOf_eq_of_mem
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : a ∈ l₁
⊢ idxOf a l₂ < l₁.length

Tactic:
exact hl.idxOf_eq_of_mem h ▸ idxOf_lt_length_of_mem h
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
⊢ idxOf a l₁ ≤ idxOf a l₂

Tactic:
have := hl.idxOf_le a
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
this : idxOf a l₁ ≤ idxOf a l₂
⊢ a ∈ l₁

Tactic:
grind [List.idxOf_lt_length_iff]

Premises used: List.idxOf_lt_length_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <:+ l₂
a : α
obtain : ∀ (l₃ : List α), idxOf a (l₃ ++ l₁) ≤ (l₃ ++ l₁).length - l₁.length + idxOf a l₁
⊢ idxOf a l₂ ≤ l₂.length - l₁.length + idxOf a l₁

Tactic:
obtain ⟨l₃, rfl⟩ := hl

Premises used: rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ : List α
inst : BEq α
inst_1 : LawfulBEq α
a : α
l₃ : List α
⊢ idxOf a (l₃ ++ l₁) ≤ (l₃ ++ l₁).length - l₁.length + idxOf a l₁

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <:+ l₂
a : α
obtain : ∀ (l₃ : List α), idxOf a (l₃ ++ l₁) + l₁.length ≤ idxOf a l₁ + (l₃ ++ l₁).length
⊢ idxOf a l₂ + l₁.length ≤ idxOf a l₁ + l₂.length

Tactic:
obtain ⟨l₃, rfl⟩ := hl

Premises used: rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ : List α
inst : BEq α
inst_1 : LawfulBEq α
a : α
l₃ : List α
⊢ idxOf a (l₃ ++ l₁) + l₁.length ≤ idxOf a l₁ + (l₃ ++ l₁).length

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
n : ℕ
l : List α
ha : a ∈ l
rw : idxOf a l < (take n l).length ↔ idxOf a l < n
⊢ a ∈ take n l ↔ idxOf a l < n

Tactic:
rw [l.take_prefix n |>.mem_iff_idxOf_lt_length]

Premises used: List.IsPrefix.mem_iff_idxOf_lt_length, List.take_prefix
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
n : ℕ
l : List α
ha : a ∈ l
⊢ idxOf a l < (take n l).length ↔ idxOf a l < n

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
a : α
ha : a ∈ l
rw : a ∈ take (l.length - 1) l ↔ idxOf a l < l.length - 1
rw₁ rw₂ : idxOf a l < l.length - 1 ↔ idxOf a l < l.length - 1
⊢ a ∈ l.dropLast ↔ idxOf a l < l.length - 1

Tactic:
rw [dropLast_eq_take, mem_take_iff_idxOf_lt ha]

Premises used: List.dropLast_eq_take, List.mem_take_iff_idxOf_lt
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
a : α
ha : a ∈ l.dropLast
⊢ idxOf a l.dropLast < l.dropLast.length

Tactic:
have := idxOf_lt_length_of_mem ha
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
a : α
ha : a ∈ l.dropLast
this : idxOf a l.dropLast < l.dropLast.length
⊢ idxOf a l + 1 < l.length

Tactic:
grind [IsPrefix.idxOf_eq_of_mem]

Premises used: List.IsPrefix.idxOf_eq_of_mem
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.getLast hl ∈ l.dropLast
contrapose : ∀ (hl' : ¬l.length - 1 ≤ idxOf (l.getLast hl) l), l.getLast hl ∈ l.dropLast
⊢ l.length - 1 ≤ idxOf (l.getLast hl) l

Tactic:
contrapose hl'
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.length - 1 ≤ idxOf (l.getLast hl) l
rwa : idxOf (l.getLast hl) l < l.length - 1
rwa₁ rwa₂ rwa₃ rwa₄ : ¬l.length - 1 ≤ idxOf (l.getLast hl) l
⊢ l.getLast hl ∈ l.dropLast

Tactic:
rwa [mem_dropLast_iff_idxOf_lt <| getLast_mem hl, ← Nat.not_le]

Premises used: List.getLast_mem, List.mem_dropLast_iff_idxOf_lt, Nat.not_le
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l l.length = none

Tactic:
getElem?_eq_none (Nat.le_refl _)

Premises used: Nat.le_refl, List.getElem?_eq_none
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
l : List α
n : ℕ
h : n < l.length
⊢ f (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n h) =
    getElem (valid := fun (as : List β) (i : ℕ) ↦ i < as.length) (map f l) n ⋯

Tactic:
Eq.symm (getElem_map _)

Premises used: List.getElem_map, Eq.symm
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l l₁ l₂ : List α
h : length.{u} (α := α) [] - 1 < length.{u} (α := α) []
⊢ False

Tactic:
Nat.lt_irrefl 0 h

Premises used: Nat.lt_irrefl, OfNat.ofNat
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l l₁ l₂ : List α
h : length.{u} (α := α) [] - 1 < length.{u} (α := α) []
⊢ False

Tactic:
exact Nat.lt_irrefl 0 h

Premises used: Nat.lt_irrefl, OfNat.ofNat
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : l.length - 1 < l.length
⊢ l.get (⟨l.length - 1, h⟩ : Fin l.length) = l.getLast ⋯

Tactic:
(getLast_eq_getElem _).symm

Premises used: List.getLast_eq_getElem, Eq.symm
-- Module: Mathlib.Data.List.Basic
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.Basic
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.Basic
Goal:
α : Type u
l₁ l₂ : List α
h' :
  ∀ (n : ℕ),
    n < max l₁.length l₂.length →
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ n =
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n
h :
  ∀ (i : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ i
⊢ l₁ = l₂

Tactic:
apply ext_getElem?

Premises used: List.ext_getElem?
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
h' :
  ∀ (n : ℕ),
    n < max l₁.length l₂.length →
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ n =
        getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n
⊢ ∀ (i : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ i =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ i

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
mp :
  l₁ = l₂ →
    l₁.length = l₂.length ∧
      ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length),
        l₁.get (⟨n, h₁⟩ : Fin l₁.length) = l₂.get (⟨n, h₂⟩ : Fin l₂.length)
mpr :
  (l₁.length = l₂.length ∧
      ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length),
        l₁.get (⟨n, h₁⟩ : Fin l₁.length) = l₂.get (⟨n, h₂⟩ : Fin l₂.length)) →
    l₁ = l₂
⊢ l₁ = l₂ ↔
    l₁.length = l₂.length ∧
      ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length),
        l₁.get (⟨n, h₁⟩ : Fin l₁.length) = l₂.get (⟨n, h₂⟩ : Fin l₂.length)

Tactic:
constructor
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ : List α
⊢ l₁.length = l₁.length ∧
    ∀ (n : ℕ) (h₁ h₂ : n < l₁.length), l₁.get (⟨n, h₁⟩ : Fin l₁.length) = l₁.get (⟨n, h₂⟩ : Fin l₁.length)

Tactic:
⟨rfl, fun _ _ _ ↦ rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ : List α
⊢ l₁.length = l₁.length ∧
    ∀ (n : ℕ) (h₁ h₂ : n < l₁.length), l₁.get (⟨n, h₁⟩ : Fin l₁.length) = l₁.get (⟨n, h₂⟩ : Fin l₁.length)

Tactic:
exact ⟨rfl, fun _ _ _ ↦ rfl⟩
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
h₁ : l₁.length = l₂.length
h₂ :
  ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length),
    l₁.get (⟨n, h₁⟩ : Fin l₁.length) = l₂.get (⟨n, h₂⟩ : Fin l₂.length)
⊢ l₁ = l₂

Tactic:
ext_get h₁ h₂

Premises used: List.ext_get
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
h₁ : l₁.length = l₂.length
h₂ :
  ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length),
    l₁.get (⟨n, h₁⟩ : Fin l₁.length) = l₂.get (⟨n, h₂⟩ : Fin l₂.length)
⊢ l₁ = l₂

Tactic:
exact ext_get h₁ h₂

Premises used: List.ext_get
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ : List α
n : ℕ
h : n < max l₁.length l₁.length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ n =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ n

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l₁ l₂ : List α
inst : Inhabited α
hl : l₁.length = l₂.length
h :
  ∀ (n : ℕ),
    getElem! (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ n =
      getElem! (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n
n : ℕ
h₁ : n < l₁.length
h₂ : n < l₂.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ n h₁ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ n h₂

Tactic:
simpa only [← getElem!_pos] using h n

Premises used: getElem!_pos
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l : List α
h : idxOf a l < l.length
⊢ l.get (⟨idxOf a l, h⟩ : Fin l.length) = a

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l : List α
h : a ∈ l
rw : some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l) ⋯) = some a
rw₁ rw₂ : some a = some a
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l) = some a

Tactic:
rw [getElem?_eq_getElem (idxOf_lt_length_iff.2 h), getElem_idxOf]

Premises used: Iff.mpr, List.getElem_idxOf, List.idxOf_lt_length_iff, List.getElem?_eq_getElem
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
⊢ idxOf x l = idxOf y l ↔ x = y

Tactic:
⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
refine : ∀ (h : idxOf x l = idxOf y l), x = y
⊢ idxOf x l = idxOf y l ↔ x = y

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
h : idxOf x l = idxOf y l
rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf x l) ⋯ = y
⊢ x = y

Tactic:
rw [← getElem_idxOf (idxOf_lt_length_iff.mpr hx)]

Premises used: Iff.mpr, List.getElem_idxOf, List.idxOf_lt_length_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
h : idxOf x l = idxOf y l
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf x l) ⋯ = y

Tactic:
simp [h]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
n : Fin l.reverse.length
hn' : l.length - 1 - (↑n : ℕ) < l.length
⊢ l.reverse.get n = l.get (⟨l.length - 1 - (↑n : ℕ), hn'⟩ : Fin l.length)

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l_1 l₁ l₂ l : List α
h : l.length = 1
⊢ 0 < l.length

Tactic:
lia
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : l.length = 1
⊢ l.length = 1

Tactic:
h
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : l.length = 1
⊢ l.length = [l.get (⟨0, ⋯⟩ : Fin l.length)].length

Tactic:
convert! h
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : l.length = 1
⊢ ∀ (n : ℕ) (h₁ : n < l.length) (h₂ : n < [l.get (⟨0, ⋯⟩ : Fin l.length)].length),
    l.get (⟨n, h₁⟩ : Fin l.length) =
      [l.get (⟨0, ⋯⟩ : Fin l.length)].get (⟨n, h₂⟩ : Fin [l.get (⟨0, ⋯⟩ : Fin l.length)].length)

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
h : l.length = 1
⊢ l = [l.get (⟨0, ⋯⟩ : Fin l.length)]

Tactic:
refine ext_get (by convert! h) (by grind)

Premises used: List.ext_get
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l_1 l₁ l₂ l : List α
i j : ℕ
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ j < l.length

Tactic:
simpa using hj
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
i j : ℕ
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.set i a) j hj =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯

Tactic:
simp [h]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
l : List α
⊢ flatMap (pure ∘ f) l = map f l

Tactic:
.symm <| map_eq_flatMap ..

Premises used: List.map_eq_flatMap, Eq.symm
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l : List α
f g : α → List β
h : ∀ (x : α), x ∈ l → f x = g x
⊢ flatMap f l = flatMap g l

Tactic:
(congr_arg List.flatten <| map_congr_left h :)

Premises used: List.map_congr_left, congr_arg, List.flatten
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
a : α
as : List α
h : a ∈ as
f : α → List α
⊢ f a <:+: flatMap f as

Tactic:
infix_of_mem_flatten (mem_map_of_mem h)

Premises used: List.infix_of_mem_flatten, List.mem_map_of_mem
-- Module: Mathlib.Data.List.Basic
Goal:
α β : Type u_2
f : α → β
l : List α
⊢ f <$> l = map f l

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
γ : Type w
h : β → γ
g : α → β
l : List α
⊢ map (h ∘ g) l = map h (map g l)

Tactic:
map_map.symm

Premises used: List.map_map, Eq.symm
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
h :
  ∀ (l : List α) (i : ℕ) (a : γ),
    getElem? (valid := fun (as : List γ) (i : ℕ) ↦ i < as.length) ((map g ∘ map f) l) i = some a ↔
      getElem? (valid := fun (as : List γ) (i : ℕ) ↦ i < as.length) (map (g ∘ f) l) i = some a
⊢ map g ∘ map f = map (g ∘ f)

Tactic:
ext l
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
l : List α
i : ℕ
a : γ
h :
  getElem? (valid := fun (as : List γ) (i : ℕ) ↦ i < as.length) ((map g ∘ map f) l) i = some a ↔
    getElem? (valid := fun (as : List γ) (i : ℕ) ↦ i < as.length) (map g (map f l)) i = some a
h₁ h₂ :
  getElem? (valid := fun (as : List γ) (i : ℕ) ↦ i < as.length) (map g (map f l)) i = some a ↔
    getElem? (valid := fun (as : List γ) (i : ℕ) ↦ i < as.length) (map g (map f l)) i = some a
⊢ getElem? (valid := fun (as : List γ) (i : ℕ) ↦ i < as.length) ((map g ∘ map f) l) i = some a ↔
    getElem? (valid := fun (as : List γ) (i : ℕ) ↦ i < as.length) (map (g ∘ f) l) i = some a

Tactic:
rw [comp_map, Function.comp_apply]

Premises used: List.comp_map, Function.comp_apply
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse f g
⊢ map f (map g []) = []

Tactic:
simp_rw [map_nil]

Premises used: List.map_nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse f g
x : β
xs : List β
simp_rw : f (g x) :: map f (map g xs) = x :: xs
simp_rw₁ : x :: map f (map g xs) = x :: xs
⊢ map f (map g (x :: xs)) = x :: xs

Tactic:
simp_rw [map_cons, h x, h.list_map xs]

Premises used: List.map_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
h : RightInverse f g
⊢ RightInverse (map f) (map g)

Tactic:
h.list_map

Premises used: Function.RightInverse, Function.LeftInverse.list_map
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
f : α → α
h : Involutive f
⊢ Involutive (map f)

Tactic:
Function.LeftInverse.list_map h

Premises used: Function.Involutive, Function.LeftInverse.list_map
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse (map f) (map g)
x : β
⊢ f (g x) = x

Tactic:
injection h [x]

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
⊢ RightInverse (map f) (map g) ↔ RightInverse f g

Tactic:
map_leftInverse_iff

Premises used: Function.RightInverse, List.map_leftInverse_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
f : α → α
⊢ Involutive (map f) ↔ Involutive f

Tactic:
map_leftInverse_iff

Premises used: Function.Involutive, List.map_leftInverse_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : map f (x :: xs) = map f (y :: ys)
⊢ f x = f y

Tactic:
injection hxy with hxy hxys
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : map f (x :: xs) = map f (y :: ys)
hxy₁ : f x = f y
⊢ map f xs = map f ys

Tactic:
injection hxy with hxy hxys
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : f x = f y
hxys : map f xs = map f ys
rw : y :: xs = y :: ys
rw₁ rw₂ : y :: ys = y :: ys
⊢ x :: xs = y :: ys

Tactic:
rw [h hxy, h.list_map hxys]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
⊢ Injective (map f) ↔ Injective f

Tactic:
⟨fun h x y hxy => ?_, (·.list_map)⟩

Premises used: Function.Injective.list_map, Iff.intro
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
refine : ∀ (h : Injective (map f)) (x y : α) (hxy : f x = f y), x = y
⊢ Injective (map f) ↔ Injective f

Tactic:
refine ⟨fun h x y hxy => ?_, (·.list_map)⟩
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
this : [x] = [y]
⊢ x = y

Tactic:
simpa using this
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
suffices : [x] = [y]
⊢ x = y

Tactic:
suffices [x] = [y] by simpa using this
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
a : map f [x] = map f [y]
⊢ [x] = [y]

Tactic:
apply h
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ map f [x] = map f [y]

Tactic:
simp [hxy]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective f
⊢ Surjective (map f)

Tactic:
let ⟨_, h⟩ := h.hasRightInverse; h.list_map.surjective

Premises used: Function.Surjective.hasRightInverse, List.map, _private.0.Function.Surjective.list_map.match_1, Function.RightInverse.surjective, Function.RightInverse.list_map, Function.Surjective
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
⊢ Surjective (map f) ↔ Surjective f

Tactic:
⟨fun h x => ?_, (·.list_map)⟩

Premises used: Iff.intro, Function.Surjective.list_map
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
refine : ∀ (h : Surjective (map f)) (x : β), ∃ (a : α), f a = x
⊢ Surjective (map f) ↔ Surjective f

Tactic:
refine ⟨fun h x => ?_, (·.list_map)⟩
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (map f)
x : β
let : ∀ (y : α) (hxy : map f [y] = [x]), ∃ (a : α), f a = x
⊢ ∃ (a : α), f a = x

Tactic:
let ⟨[y], hxy⟩ := h [x]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (map f)
x : β
y : α
hxy : map f [y] = [x]
⊢ ∃ (a : α), f a = x

Tactic:
⟨_, List.singleton_injective hxy⟩

Premises used: List.singleton_injective, Exists.intro
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (map f)
x : β
y : α
hxy : map f [y] = [x]
⊢ ∃ (a : α), f a = x

Tactic:
exact ⟨_, List.singleton_injective hxy⟩
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
h : Bijective f
⊢ Bijective (map f)

Tactic:
⟨h.1.list_map, h.2.list_map⟩

Premises used: Function.Injective.list_map, And.right, And.left, And.intro, Function.Surjective.list_map, Function.Bijective
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β
simp_rw : Injective (map f) ∧ Surjective (map f) ↔ Injective f ∧ Surjective f
simp_rw₁ : Injective f ∧ Surjective (map f) ↔ Injective f ∧ Surjective f
⊢ Bijective (map f) ↔ Bijective f

Tactic:
simp_rw [Function.Bijective, map_injective_iff, map_surjective_iff]

Premises used: List.map_surjective_iff, List.map_injective_iff, Function.Bijective
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) l
⊢ b₁ ∈ replicate l.length b₂

Tactic:
rw [map_const] at h

Premises used: List.map_const
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate l.length b₂
⊢ b₁ = b₂

Tactic:
eq_of_mem_replicate h

Premises used: List.eq_of_mem_replicate
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate l.length b₂
⊢ b₁ = b₂

Tactic:
exact eq_of_mem_replicate h

Premises used: List.eq_of_mem_replicate
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
⊢ l = [] ∨ ∃ (L : List α), ∃ (b : α), l = L ++ [b]

Tactic:
simpa using l.eq_nil_or_concat

Premises used: List.eq_nil_or_concat
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f g : α → β → α
a : α
H : ∀ (a : α) (b : β), Membership.mem (γ := List β) [] b → f a b = g a b
⊢ foldl f a [] = foldl g a []

Tactic:
rfl