awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
⊢ filterMap id l = [] ↔ ∃ (n : ℕ), l = replicate n none
have rw : (∀ (a : Option α), a ∈ l → id a = none) ↔ ∃ (n : ℕ), l = replicate n none
Tactic: rw [filterMap_eq_nil_iff]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
⊢ (∀ (a : Option α), a ∈ l → id a = none) ↔ ∃ (n : ℕ), l = replicate n none
have mp : (∀ (a : Option α), a ∈ l → id a = none) → ∃ (n : ℕ), l = replicate n none
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
mp : (∀ (a : Option α), a ∈ l → id a = none) → ∃ (n : ℕ), l = replicate n none
⊢ (∀ (a : Option α), a ∈ l → id a = none) ↔ ∃ (n : ℕ), l = replicate n none
have mpr : (∃ (n : ℕ), l = replicate n none) → ∀ (a : Option α), a ∈ l → id a = none
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
a : α
⊢ filterMap id l = [a] ↔ ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
have mp : filterMap id l = [a] → ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
a : α
mp : filterMap id l = [a] → ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
⊢ filterMap id l = [a] ↔ ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
have mpr : (∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none) → filterMap id l = [a]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (hypothesis)
Goal:
α : Type u_1
l : List (Option α)
a : α
h : filterMap id l = [a]
⊢ ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
have h₁ : ∃ (l₁ : List (Option α)),
  ∃ (a_1 : Option α),
    ∃ (l₂ : List (Option α)),
      l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : Option α), x ∈ l₁ → id x = none) ∧ id a_1 = some a ∧ filterMap id l₂ = []
Tactic: rw [filterMap_eq_cons_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
a : α
h :
  ∃ (l₁ : List (Option α)),
    ∃ (a_1 : Option α),
      ∃ (l₂ : List (Option α)),
        l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : Option α), x ∈ l₁ → id x = none) ∧ id a_1 = some a ∧ filterMap id l₂ = []
⊢ ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
have mp : ∀ (l₁ l₂ : List (Option α)) (hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none) (hl₂ : filterMap id l₂ = [])
  (h : l = l₁ ++ some a :: l₂), ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
Tactic: obtain ⟨l₁, _, l₂, h, hl₁, ⟨⟩, hl₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (hypothesis)
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : filterMap id l₂ = []
h : l = l₁ ++ some a :: l₂
⊢ ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
have hl₃ : ∀ (a : Option α), a ∈ l₂ → id a = none
Tactic: rw [filterMap_eq_nil_iff] at hl₂
Cleared hypotheses: hl₂, h
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (hypothesis)
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₁ : ∀ (x : Option α), x ∈ l₁ → id x = none
hl₂ : ∀ (a : Option α), a ∈ l₂ → id a = none
h : l = l₁ ++ some a :: l₂
⊢ ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
have hl₃ : l₁ = replicate l₁.length none
Tactic: apply eq_replicate_of_mem at hl₁
Cleared hypotheses: hl₁
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (hypothesis)
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
hl₂ : ∀ (a : Option α), a ∈ l₂ → id a = none
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
⊢ ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
have hl₃ : l₂ = replicate l₂.length none
Tactic: apply eq_replicate_of_mem at hl₂
Cleared hypotheses: hl₂
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ (m : ℕ), ∃ (n : ℕ), l = replicate m none ++ some a :: replicate n none
have mp : ∃ (m : ℕ),
  ∃ (n : ℕ),
    replicate l₁.length none ++ some a :: replicate l₂.length none = replicate m none ++ some a :: replicate n none
Tactic: rw [h, hl₁, hl₂]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
⊢ ∃ (m : ℕ),
    ∃ (n : ℕ),
      replicate l₁.length none ++ some a :: replicate l₂.length none = replicate m none ++ some a :: replicate n none
have w : ℕ
Tactic: use l₁.length, l₂.length
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
a : α
l₁ l₂ : List (Option α)
h : l = l₁ ++ some a :: l₂
hl₁ : l₁ = replicate l₁.length none
hl₂ : l₂ = replicate l₂.length none
w w₁ : ℕ
⊢ ∃ (m : ℕ),
    ∃ (n : ℕ),
      replicate l₁.length none ++ some a :: replicate l₂.length none = replicate m none ++ some a :: replicate n none
have h₁ : replicate l₁.length none ++ some a :: replicate l₂.length none =
  replicate l₁.length none ++ some a :: replicate l₂.length none
Tactic: use l₁.length, l₂.length
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l'.concat a ↔
    ∃ (l₁ : List (Option α)),
      ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
have rw : l.reduceOption = l' ++ [a] ↔
  ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
Tactic: rw [concat_eq_append]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
⊢ l.reduceOption = l' ++ [a] ↔
    ∃ (l₁ : List (Option α)),
      ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
have mp : l.reduceOption = l' ++ [a] →
  ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
mp :
  l.reduceOption = l' ++ [a] →
    ∃ (l₁ : List (Option α)),
      ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
⊢ l.reduceOption = l' ++ [a] ↔
    ∃ (l₁ : List (Option α)),
      ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
have mpr : (∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []) →
  l.reduceOption = l' ++ [a]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (hypothesis)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : l.reduceOption = l' ++ [a]
⊢ ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
have h₁ : ∃ (l₁ : List (Option α)), ∃ (l₂ : List (Option α)), l = l₁ ++ l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = [a]
Tactic: rw [reduceOption_eq_append_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
h : ∃ (l₁ : List (Option α)), ∃ (l₂ : List (Option α)), l = l₁ ++ l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = [a]
⊢ ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
have mp : ∀ (l₁ w : List (Option α)) (h : l = l₁ ++ w) (hl₁ : l₁.reduceOption = l') (hl₂ : w.reduceOption = [a]),
  ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
Tactic: obtain ⟨l₁, _, h, hl₁, hl₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (hypothesis)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
hl₂ : w.reduceOption = [a]
⊢ ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
have hl₃ : ∃ (m : ℕ), ∃ (n : ℕ), w = replicate m none ++ some a :: replicate n none
Tactic: rw [reduceOption_eq_singleton_iff] at hl₂
Cleared hypotheses: hl₂
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
hl₂ : ∃ (m : ℕ), ∃ (n : ℕ), w = replicate m none ++ some a :: replicate n none
⊢ ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
have mp : ∀ (m n : ℕ) (hl₂ : w = replicate m none ++ some a :: replicate n none),
  ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
Tactic: obtain ⟨m, n, hl₂⟩ := hl₂
Cleared hypotheses: hl₂
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w = replicate m none ++ some a :: replicate n none
⊢ ∃ (l₁ : List (Option α)),
    ∃ (l₂ : List (Option α)), l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
have h₁ : l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
  (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
Tactic: use l₁ ++ replicate m none, replicate n none
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w = replicate m none ++ some a :: replicate n none
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
have h₁ : l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
  (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
Tactic: simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁,
      hl₂, and_self]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w = replicate m none ++ some a :: replicate n none
h₁ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
have h₂ : l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
  l₁.reduceOption ++ reduceOption (replicate m none) = l' ∧
    Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
Tactic: simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁,
      hl₂, and_self]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w = replicate m none ++ some a :: replicate n none
h₁ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
h₂ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    l₁.reduceOption ++ reduceOption (replicate m none) = l' ∧
      Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
have h₃ : l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧ l₁.reduceOption ++ [] = l' ∧ True
Tactic: simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁,
      hl₂, and_self]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w = replicate m none ++ some a :: replicate n none
h₁ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
h₂ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    l₁.reduceOption ++ reduceOption (replicate m none) = l' ∧
      Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
h₃ : l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧ l₁.reduceOption ++ [] = l' ∧ True
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
have h₄ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ l₁.reduceOption ++ [] = l' ∧ True
Tactic: simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁,
      hl₂, and_self]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w = replicate m none ++ some a :: replicate n none
h₁ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
h₂ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    l₁.reduceOption ++ reduceOption (replicate m none) = l' ∧
      Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
h₃ : l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧ l₁.reduceOption ++ [] = l' ∧ True
h₄ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ l₁.reduceOption ++ [] = l' ∧ True
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
have h₅ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ l₁.reduceOption = l' ∧ True
Tactic: simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁,
      hl₂, and_self]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w = replicate m none ++ some a :: replicate n none
h₁ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
h₂ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    l₁.reduceOption ++ reduceOption (replicate m none) = l' ∧
      Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
h₃ : l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧ l₁.reduceOption ++ [] = l' ∧ True
h₄ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ l₁.reduceOption ++ [] = l' ∧ True
h₅ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ l₁.reduceOption = l' ∧ True
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
have h₆ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ True ∧ True
Tactic: simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁,
      hl₂, and_self]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w = replicate m none ++ some a :: replicate n none
h₁ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
h₂ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    l₁.reduceOption ++ reduceOption (replicate m none) = l' ∧
      Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
h₃ : l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧ l₁.reduceOption ++ [] = l' ∧ True
h₄ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ l₁.reduceOption ++ [] = l' ∧ True
h₅ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ l₁.reduceOption = l' ∧ True
h₆ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ True ∧ True
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
have h₇ : True ∧ True ∧ True
Tactic: simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁,
      hl₂, and_self]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
w w_1 : List (Option α)
h : l = w ++ some a :: w_1
hl₁ : w.reduceOption = l'
hl₂ : w_1.reduceOption = []
⊢ l.reduceOption = l' ++ [a]
have mpr : (w ++ some a :: w_1).reduceOption = l' ++ [a]
Tactic: rw [h, reduceOption_append, reduceOption_cons_of_some, hl₁, hl₂]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
w w_1 : List (Option α)
h : l = w ++ some a :: w_1
hl₁ : w.reduceOption = l'
hl₂ : w_1.reduceOption = []
mpr : (w ++ some a :: w_1).reduceOption = l' ++ [a]
⊢ l.reduceOption = l' ++ [a]
have mpr₁ : w.reduceOption ++ (some a :: w_1).reduceOption = l' ++ [a]
Tactic: rw [h, reduceOption_append, reduceOption_cons_of_some, hl₁, hl₂]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
w w_1 : List (Option α)
h : l = w ++ some a :: w_1
hl₁ : w.reduceOption = l'
hl₂ : w_1.reduceOption = []
mpr : (w ++ some a :: w_1).reduceOption = l' ++ [a]
mpr₁ : w.reduceOption ++ (some a :: w_1).reduceOption = l' ++ [a]
⊢ l.reduceOption = l' ++ [a]
have mpr₂ : w.reduceOption ++ a :: w_1.reduceOption = l' ++ [a]
Tactic: rw [h, reduceOption_append, reduceOption_cons_of_some, hl₁, hl₂]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
w w_1 : List (Option α)
h : l = w ++ some a :: w_1
hl₁ : w.reduceOption = l'
hl₂ : w_1.reduceOption = []
mpr : (w ++ some a :: w_1).reduceOption = l' ++ [a]
mpr₁ : w.reduceOption ++ (some a :: w_1).reduceOption = l' ++ [a]
mpr₂ : w.reduceOption ++ a :: w_1.reduceOption = l' ++ [a]
⊢ l.reduceOption = l' ++ [a]
have mpr₃ : l' ++ a :: w_1.reduceOption = l' ++ [a]
Tactic: rw [h, reduceOption_append, reduceOption_cons_of_some, hl₁, hl₂]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
w w_1 : List (Option α)
h : l = w ++ some a :: w_1
hl₁ : w.reduceOption = l'
hl₂ : w_1.reduceOption = []
mpr : (w ++ some a :: w_1).reduceOption = l' ++ [a]
mpr₁ : w.reduceOption ++ (some a :: w_1).reduceOption = l' ++ [a]
mpr₂ : w.reduceOption ++ a :: w_1.reduceOption = l' ++ [a]
mpr₃ : l' ++ a :: w_1.reduceOption = l' ++ [a]
⊢ l.reduceOption = l' ++ [a]
have mpr₄ : l' ++ [a] = l' ++ [a]
Tactic: rw [h, reduceOption_append, reduceOption_cons_of_some, hl₁, hl₂]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
⊢ length.{u_1} (α := α) (reduceOption []) = length.{u_1} (α := Option α) (filter Option.isSome [])
have nil : length.{u_1} (α := α) [] = length.{u_1} (α := Option α) (filter Option.isSome [])
Tactic: simp_rw [reduceOption_nil, filter_nil, length]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
nil : length.{u_1} (α := α) [] = length.{u_1} (α := Option α) (filter Option.isSome [])
⊢ length.{u_1} (α := α) (reduceOption []) = length.{u_1} (α := Option α) (filter Option.isSome [])
have nil₁ : length.{u_1} (α := α) [] = length.{u_1} (α := Option α) []
Tactic: simp_rw [reduceOption_nil, filter_nil, length]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
hd : Option α
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
⊢ (hd :: tl).reduceOption.length = (filter Option.isSome (hd :: tl)).length
have cons : (none :: tl).reduceOption.length = (filter Option.isSome (none :: tl)).length
Tactic: cases hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
hd : Option α
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
cons : (none :: tl).reduceOption.length = (filter Option.isSome (none :: tl)).length
⊢ (hd :: tl).reduceOption.length = (filter Option.isSome (hd :: tl)).length
have cons₁ : ∀ (val : α), (some val :: tl).reduceOption.length = (filter Option.isSome (some val :: tl)).length
Tactic: cases hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length = (filter Option.isSome l).length
have nil : length.{u_1} (α := α) (reduceOption []) = length.{u_1} (α := Option α) (filter Option.isSome [])
Tactic: induction l with
  | nil => simp_rw [reduceOption_nil, filter_nil, length]
  | cons hd tl hl => cases hd <;> simp [hl]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
nil : length.{u_1} (α := α) (reduceOption []) = length.{u_1} (α := Option α) (filter Option.isSome [])
⊢ l.reduceOption.length = (filter Option.isSome l).length
have cons : ∀ (hd : Option α) (tl : List (Option α)) (hl : tl.reduceOption.length = (filter Option.isSome tl).length),
  (hd :: tl).reduceOption.length = (filter Option.isSome (hd :: tl)).length
Tactic: induction l with
  | nil => simp_rw [reduceOption_nil, filter_nil, length]
  | cons hd tl hl => cases hd <;> simp [hl]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
⊢ l.length = l.reduceOption.length + (filter Option.isNone l).length
have simp_rw : l.length = (filter Option.isSome l).length + (filter Option.isNone l).length
Tactic: simp_rw [reduceOption_length_eq, l.length_eq_length_filter_add Option.isSome, Option.not_isSome]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
simp_rw : l.length = (filter Option.isSome l).length + (filter Option.isNone l).length
⊢ l.length = l.reduceOption.length + (filter Option.isNone l).length
have simp_rw₁ : (filter Option.isSome l).length + (filter (fun (x : Option α) ↦ !x.isSome) l).length =
  (filter Option.isSome l).length + (filter Option.isNone l).length
Tactic: simp_rw [reduceOption_length_eq, l.length_eq_length_filter_add Option.isSome, Option.not_isSome]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length ≤ l.length
have rw : l.reduceOption.length ≤ l.reduceOption.length + (filter Option.isNone l).length
Tactic: rw [length_eq_reduceOption_length_add_filter_none]