awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
rw : (b :: (c :: l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
rw₁ : (b :: c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
⊢ (b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
have rw₂ : (c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
Tactic: rw [cons_append, cons_append, getLast?_cons_cons,
    ← cons_append, getLast?_append_cons (c :: l₁)]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
rw : (b :: (c :: l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
rw₁ : (b :: c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
rw₂ : (c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
⊢ (b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
have rw₃ : (c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
Tactic: rw [cons_append, cons_append, getLast?_cons_cons,
    ← cons_append, getLast?_append_cons (c :: l₁)]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
rw : (b :: (c :: l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
rw₁ : (b :: c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
rw₂ : (c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
rw₃ : (c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
⊢ (b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
have rw₄ : (a :: l₂).getLast? = (a :: l₂).getLast?
Tactic: rw [cons_append, cons_append, getLast?_cons_cons,
    ← cons_append, getLast?_append_cons (c :: l₁)]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : Inhabited α
l : List α
⊢ l.head! = l.head?.getD default
have nil : Eq.{u + 1} (α := α) (head! []) (Option.getD (head? []) default)
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : Inhabited α
l : List α
nil : Eq.{u + 1} (α := α) (head! []) (Option.getD (head? []) default)
⊢ l.head! = l.head?.getD default
have cons : ∀ (head : α) (tail : List α), (head :: tail).head! = (head :: tail).head?.getD default
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
x a : α
l : List α
h : x ∈ (a :: l).head?
⊢ a :: l = x :: (a :: l).tail
have h₁ : a = x
Tactic: simp only [head?, Option.mem_def, Option.some_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : Inhabited α
t s : List α
h : s ≠ []
⊢ (s ++ t).head! = s.head!
have nil : ∀ (h : Ne.{u + 1} (α := List α) [] []), ([] ++ t).head! = head! []
Tactic: induction s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : Inhabited α
t s : List α
h : s ≠ []
nil : ∀ (h : Ne.{u + 1} (α := List α) [] []), ([] ++ t).head! = head! []
⊢ (s ++ t).head! = s.head!
have cons : ∀ (head : α) (tail : List α),
  (∀ (h : tail ≠ []), (tail ++ t).head! = tail.head!) →
    ∀ (h : head :: tail ≠ []), (head :: tail ++ t).head! = (head :: tail).head!
Tactic: induction s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
b : α
l : List α
a : α
h : a ∈ (b :: l).head?
⊢ a :: (b :: l).tail = b :: l
have this : b = a
Tactic: have : b = a := by simpa using h
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
inst : Inhabited α
l : List α
h : l ≠ []
⊢ l.head! ∈ l
have h' : l.head! ∈ l.head! :: l.tail
Tactic: have h' : l.head! ∈ l.head! :: l.tail := mem_cons_self
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : Inhabited α
l : List α
h : l ≠ []
h' : l.head! ∈ l.head! :: l.tail
⊢ l.head! ∈ l
have rwa : ∀ (h' : l.head! ∈ l), l.head! ∈ l
Tactic: rwa [cons_head!_tail h] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
p : α → Prop
⊢ (∃ (x : α), x ∈ l ∧ p x) ↔
    ∃ (i : ℕ), ∃ (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x)
have simp : (∃ (x : α),
    (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧ p x) ↔
  ∃ (i : ℕ), ∃ (x : i < l.length), p (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i x)
Tactic: simp only [mem_iff_getElem]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
⊢ (Surjective.{1, u + 1} (β := Option α) fun (n : ℕ) ↦
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) ↔
    ∀ (x : α), x ∈ l
have refine : ∀ (h : ∀ (x : α), x ∈ l) (x : Option α),
  ∃ (a : ℕ), (fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a = x
Tactic: refine ⟨fun h x ↦ mem_iff_getElem?.mpr <| h x, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
x : Option α
⊢ ∃ (a : ℕ), (fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a = x
have none : ∃ (a : ℕ),
  Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a) none
Tactic: cases x with
  | none => exact ⟨l.length, getElem?_eq_none <| Nat.le_refl _⟩
  | some x => exact mem_iff_getElem?.mp <| h x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
x : Option α
none :
  ∃ (a : ℕ),
    Eq.{u + 1} (α := Option α) ((fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a)
      Option.none
⊢ ∃ (a : ℕ), (fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a = x
have some : ∀ (x : α), ∃ (a : ℕ), (fun (n : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n) a = some x
Tactic: cases x with
  | none => exact ⟨l.length, getElem?_eq_none <| Nat.le_refl _⟩
  | some x => exact mem_iff_getElem?.mp <| h x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l_1 l₁ l₂ l : List α
i : ℕ
h : i < l.tail.length
⊢ i + 1 < l.length
have h₁ : i < l.length - 1
Tactic: simp only [length_tail] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
a : α
⊢ l <+ [a] ↔ l = [] ∨ l = [a]
have mp : l <+ [a] → l = [] ∨ l = [a]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
a : α
mp : l <+ [a] → l = [] ∨ l = [a]
⊢ l <+ [a] ↔ l = [] ∨ l = [a]
have mpr : l = [] ∨ l = [a] → l <+ [a]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a b : α
l : List α
h : b = a
e : b = a := h
⊢ idxOf a (b :: l) = 0
have rw : idxOf b (b :: l) = 0
Tactic: rw [← e]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
a : α
⊢ idxOf a l = 0 ↔ l = [] ∨ l.head? = some a
have nil : idxOf a [] = 0 ↔ Eq.{u + 1} (α := List α) [] [] ∨ head? [] = some a
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
a : α
nil : idxOf a [] = 0 ↔ Eq.{u + 1} (α := List α) [] [] ∨ head? [] = some a
⊢ idxOf a l = 0 ↔ l = [] ∨ l.head? = some a
have cons : ∀ (head : α) (tail : List α), idxOf a (head :: tail) = 0 ↔ head :: tail = [] ∨ (head :: tail).head? = some a
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
⊢ idxOf a l₁ ≤ idxOf a l₂
have obtain : ∀ (l₃ : List α), idxOf a l₁ ≤ idxOf a (l₁ ++ l₃)
Tactic: obtain ⟨l₃, rfl⟩ := hl
Cleared hypotheses: l₂, hl
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
ha : a ∈ l₁
⊢ idxOf a l₁ = idxOf a l₂
have obtain : ∀ (l₃ : List α), idxOf a l₁ = idxOf a (l₁ ++ l₃)
Tactic: obtain ⟨l₃, rfl⟩ := hl
Cleared hypotheses: l₂, hl
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
⊢ a ∈ l₁ ↔ idxOf a l₂ < l₁.length
have refine_1 : ∀ (h : a ∈ l₁), idxOf a l₂ < l₁.length
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
⊢ a ∈ l₁ ↔ idxOf a l₂ < l₁.length
have refine_2 : ∀ (h : idxOf a l₂ < l₁.length), a ∈ l₁
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <+: l₂
a : α
h : idxOf a l₂ < l₁.length
⊢ a ∈ l₁
have this : idxOf a l₁ ≤ idxOf a l₂
Tactic: have := hl.idxOf_le a
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <:+ l₂
a : α
⊢ idxOf a l₂ ≤ l₂.length - l₁.length + idxOf a l₁
have obtain : ∀ (l₃ : List α), idxOf a (l₃ ++ l₁) ≤ (l₃ ++ l₁).length - l₁.length + idxOf a l₁
Tactic: obtain ⟨l₃, rfl⟩ := hl
Cleared hypotheses: l₂, hl
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l₁ l₂ : List α
inst : BEq α
inst_1 : LawfulBEq α
hl : l₁ <:+ l₂
a : α
⊢ idxOf a l₂ + l₁.length ≤ idxOf a l₁ + l₂.length
have obtain : ∀ (l₃ : List α), idxOf a (l₃ ++ l₁) + l₁.length ≤ idxOf a l₁ + (l₃ ++ l₁).length
Tactic: obtain ⟨l₃, rfl⟩ := hl
Cleared hypotheses: l₂, hl
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
n : ℕ
l : List α
ha : a ∈ l
⊢ a ∈ take n l ↔ idxOf a l < n
have rw : idxOf a l < (take n l).length ↔ idxOf a l < n
Tactic: rw [l.take_prefix n |>.mem_iff_idxOf_lt_length]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
a : α
ha : a ∈ l
⊢ a ∈ l.dropLast ↔ idxOf a l < l.length - 1
have rw : a ∈ take (l.length - 1) l ↔ idxOf a l < l.length - 1
Tactic: rw [dropLast_eq_take, mem_take_iff_idxOf_lt ha]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
⊢ a ∈ l.dropLast ↔ idxOf a l < l.length - 1
have rw₁ : idxOf a l < l.length - 1 ↔ idxOf a l < l.length - 1
Tactic: rw [dropLast_eq_take, mem_take_iff_idxOf_lt ha]
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
a : α
ha : a ∈ l.dropLast
⊢ idxOf a l + 1 < l.length
have this : idxOf a l.dropLast < l.dropLast.length
Tactic: have := idxOf_lt_length_of_mem ha
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.getLast hl ∈ l.dropLast
⊢ l.length - 1 ≤ idxOf (l.getLast hl) l
have contrapose : ∀ (hl' : ¬l.length - 1 ≤ idxOf (l.getLast hl) l), l.getLast hl ∈ l.dropLast
Tactic: contrapose hl'
Cleared hypotheses: hl'
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.length - 1 ≤ idxOf (l.getLast hl) l
⊢ l.getLast hl ∈ l.dropLast
have rwa : idxOf (l.getLast hl) l < l.length - 1
Tactic: rwa [mem_dropLast_iff_idxOf_lt <| getLast_mem hl, ← Nat.not_le]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ take 1 (drop n l) = [l.get (⟨n, h⟩ : Fin l.length)]
have rw : [getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n h] = [l.get (⟨n, h⟩ : Fin l.length)]
Tactic: rw [drop_eq_getElem_cons h, take, take]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
⊢ l₁ = l₂
have h : ∀ (i : ℕ),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₁ i =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l₂ i
Tactic: apply ext_getElem?
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l₁ l₂ : List α
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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)
⊢ 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)
have 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₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l) = some a
have rw : some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l) sorry) = some a
Tactic: rw [getElem?_eq_getElem (idxOf_lt_length_iff.2 h), getElem_idxOf]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l) = some a
have rw₁ : some a = some a
Tactic: rw [getElem?_eq_getElem (idxOf_lt_length_iff.2 h), getElem_idxOf]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
⊢ idxOf x l = idxOf y l ↔ x = y
have refine : ∀ (h : idxOf x l = idxOf y l), x = y
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
l : List α
x y : α
hx : x ∈ l
h : idxOf x l = idxOf y l
⊢ x = y
have rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf x l) sorry = y
Tactic: rw [← getElem_idxOf (idxOf_lt_length_iff.mpr hx)]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map g ∘ map f = map (g ∘ f)
have 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
Tactic: ext l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
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
have 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
Tactic: rw [comp_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [comp_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse f g
x : β
xs : List β
⊢ map f (map g (x :: xs)) = x :: xs
have simp_rw : f (g x) :: map f (map g xs) = x :: xs
Tactic: simp_rw [map_cons, h x, h.list_map xs]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
⊢ map f (map g (x :: xs)) = x :: xs
have simp_rw₁ : x :: map f (map g xs) = x :: xs
Tactic: simp_rw [map_cons, h x, h.list_map xs]
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
h : Injective f
x : α
xs : List α
y : α
ys : List α
hxy : map f (x :: xs) = map f (y :: ys)
⊢ x :: xs = y :: ys
have hxy₁ : f x = f y
Tactic: injection hxy with hxy hxys
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
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
⊢ x :: xs = y :: ys
have hxys : map f xs = map f ys
Tactic: injection hxy with hxy hxys
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
⊢ x :: xs = y :: ys
have rw : y :: xs = y :: ys
Tactic: rw [h hxy, h.list_map hxys]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
⊢ x :: xs = y :: ys
have rw₁ : y :: ys = y :: ys
Tactic: rw [h hxy, h.list_map hxys]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
⊢ Injective (map f) ↔ Injective f
have refine : ∀ (h : Injective (map f)) (x y : α) (hxy : f x = f y), x = y
Tactic: refine ⟨fun h x y hxy => ?_, (·.list_map)⟩
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ x = y
have suffices : [x] = [y]
Tactic: suffices [x] = [y] by simpa using this
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ [x] = [y]
have a : map f [x] = map f [y]
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
⊢ Surjective (map f) ↔ Surjective f
have refine : ∀ (h : Surjective (map f)) (x : β), ∃ (a : α), f a = x
Tactic: refine ⟨fun h x => ?_, (·.list_map)⟩
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (map f)
x : β
⊢ ∃ (a : α), f a = x
have let : ∀ (y : α) (hxy : map f [y] = [x]), ∃ (a : α), f a = x
Tactic: let ⟨[y], hxy⟩ := h [x]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
⊢ Bijective (map f) ↔ Bijective f
have simp_rw : Injective (map f) ∧ Surjective (map f) ↔ Injective f ∧ Surjective f
Tactic: simp_rw [Function.Bijective, map_injective_iff, map_surjective_iff]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
simp_rw : Injective (map f) ∧ Surjective (map f) ↔ Injective f ∧ Surjective f
⊢ Bijective (map f) ↔ Bijective f
have simp_rw₁ : Injective f ∧ Surjective (map f) ↔ Injective f ∧ Surjective f
Tactic: simp_rw [Function.Bijective, map_injective_iff, map_surjective_iff]
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) l
⊢ b₁ = b₂
have h₁ : b₁ ∈ replicate l.length b₂
Tactic: rw [map_const] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f g : α → β → α
hd : β
tl : List β
ih : ∀ (a : α) (H : ∀ (a : α) (b : β), b ∈ tl → f a b = g a b), foldl f a tl = foldl g a tl
a : α
H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b
⊢ foldl f a (hd :: tl) = foldl g a (hd :: tl)
have cons : foldl f (f a hd) tl = foldl g (g a hd) tl
Tactic: unfold foldl
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f g : α → β → α
hd : β
tl : List β
ih : ∀ (a : α) (H : ∀ (a : α) (b : β), b ∈ tl → f a b = g a b), foldl f a tl = foldl g a tl
a : α
H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b
⊢ foldl f (f a hd) tl = foldl g (g a hd) tl
have cons : foldl g (f a hd) tl = foldl g (g a hd) tl
Tactic: rw [ih _ fun a b bin => H a b <| mem_cons_of_mem _ bin, H a hd mem_cons_self]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f g : α → β → α
hd : β
tl : List β
ih : ∀ (a : α) (H : ∀ (a : α) (b : β), b ∈ tl → f a b = g a b), foldl f a tl = foldl g a tl
a : α
H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b
cons : foldl g (f a hd) tl = foldl g (g a hd) tl
⊢ foldl f (f a hd) tl = foldl g (g a hd) tl
have cons₁ : foldl g (g a hd) tl = foldl g (g a hd) tl
Tactic: rw [ih _ fun a b bin => H a b <| mem_cons_of_mem _ bin, H a hd mem_cons_self]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f g : α → β → α
a : α
l : List β
H : ∀ (a : α) (b : β), b ∈ l → f a b = g a b
⊢ foldl f a l = foldl g a l
have nil : ∀ (a : α) (H : ∀ (a : α) (b : β), Membership.mem (γ := List β) [] b → f a b = g a b), foldl f a [] = foldl g a []
Tactic: induction l generalizing a with
  | nil => rfl
  | cons hd tl ih =>
    unfold foldl
    rw [ih _ fun a b bin => H a b <| mem_cons_of_mem _ bin, H a hd mem_cons_self]
Cleared hypotheses: a, l, H
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f g : α → β → α
a : α
l : List β
H : ∀ (a : α) (b : β), b ∈ l → f a b = g a b
nil : ∀ (a : α) (H : ∀ (a : α) (b : β), Membership.mem (γ := List β) [] b → f a b = g a b), foldl f a [] = foldl g a []
⊢ foldl f a l = foldl g a l
have cons : ∀ (hd : β) (tl : List β) (ih : ∀ (a : α) (H : ∀ (a : α) (b : β), b ∈ tl → f a b = g a b), foldl f a tl = foldl g a tl)
  (a : α) (H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b), foldl f a (hd :: tl) = foldl g a (hd :: tl)
Tactic: induction l generalizing a with
  | nil => rfl
  | cons hd tl ih =>
    unfold foldl
    rw [ih _ fun a b bin => H a b <| mem_cons_of_mem _ bin, H a hd mem_cons_self]
Cleared hypotheses: a, l, H
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f g : α → β → β
b : β
l : List α
H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
⊢ foldr f b l = foldr g b l
have cons : ∀ (hd : α) (tl : List α) (ih : ∀ (H : ∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b), foldr f b tl = foldr g b tl)
  (H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b), foldr f b (hd :: tl) = foldr g b (hd :: tl)
Tactic: induction l with | nil => rfl | cons hd tl ih => ?_
Cleared hypotheses: l, H
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : ∀ (H : ∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b), foldr f b tl = foldr g b tl
H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)
have H₁ : (∀ (b : β), f hd b = g hd b) ∧ ∀ (x : α), x ∈ tl → ∀ (b : β), f x b = g x b
Tactic: simp only [mem_cons, or_imp, forall_and, forall_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β → α
a : α
hf : ∀ (b : β), f a b = a
b : β
l : List β
⊢ foldl f a (b :: l) = a
have rw : foldl f (f a b) l = a
Tactic: rw [foldl_cons, hf b, foldl_fixed' hf l]