awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 β
rw : foldl f (f a b) l = a
⊢ foldl f a (b :: l) = a
have rw₁ : foldl f a l = a
Tactic: rw [foldl_cons, hf b, foldl_fixed' hf l]
-- 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 β
rw : foldl f (f a b) l = a
rw₁ : foldl f a l = a
⊢ foldl f a (b :: l) = a
have rw₂ : a = a
Tactic: rw [foldl_cons, hf b, foldl_fixed' hf l]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β → β
b : β
hf : ∀ (a : α), f a b = b
a : α
l : List α
⊢ foldr f b (a :: l) = b
have rw : f a (foldr f b l) = b
Tactic: rw [foldr_cons, foldr_fixed' hf l, hf a]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β → β
b : β
hf : ∀ (a : α), f a b = b
a : α
l : List α
rw : f a (foldr f b l) = b
⊢ foldr f b (a :: l) = b
have rw₁ : f a b = b
Tactic: rw [foldr_cons, foldr_fixed' hf l, hf a]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β → β
b : β
hf : ∀ (a : α), f a b = b
a : α
l : List α
rw : f a (foldr f b l) = b
rw₁ : f a b = b
⊢ foldr f b (a :: l) = b
have rw₂ : b = b
Tactic: rw [foldr_cons, foldr_fixed' hf l, hf a]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
a : α
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l
have revert : ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l
Tactic: revert a b
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l
have nil : ∀ (a : α) (b : β), f (foldl op₁ a []) (foldl op₂ b []) = foldl op₃ (f a b) []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
nil : ∀ (a : α) (b : β), f (foldl op₁ a []) (foldl op₂ b []) = foldl op₃ (f a b) []
⊢ ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l
have cons : ∀ (head : ι) (tail : List ι),
  (∀ (a : α) (b : β), f (foldl op₁ a tail) (foldl op₂ b tail) = foldl op₃ (f a b) tail) →
    ∀ (a : α) (b : β), f (foldl op₁ a (head :: tail)) (foldl op₂ b (head :: tail)) = foldl op₃ (f a b) (head :: tail)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l
have nil : ∀ (a : α) (b : β), f (foldl op₁ a []) (foldl op₂ b []) = foldl op₃ (f a b) []
Tactic: induction l <;> intros <;> [rfl; simp only [*, foldl]]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
nil : ∀ (a : α) (b : β), f (foldl op₁ a []) (foldl op₂ b []) = foldl op₃ (f a b) []
⊢ ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l
have cons : ∀ (head : ι) (tail : List ι),
  (∀ (a : α) (b : β), f (foldl op₁ a tail) (foldl op₂ b tail) = foldl op₃ (f a b) tail) →
    ∀ (a : α) (b : β), f (foldl op₁ a (head :: tail)) (foldl op₂ b (head :: tail)) = foldl op₃ (f a b) (head :: tail)
Tactic: induction l <;> intros <;> [rfl; simp only [*, foldl]]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
a : α
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)
have revert : ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)
Tactic: revert a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)
have nil : ∀ (a : α), foldr op₃ (f a b) [] = f (foldr op₁ a []) (foldr op₂ b [])
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
nil : ∀ (a : α), foldr op₃ (f a b) [] = f (foldr op₁ a []) (foldr op₂ b [])
⊢ ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)
have cons : ∀ (head : ι) (tail : List ι),
  (∀ (a : α), foldr op₃ (f a b) tail = f (foldr op₁ a tail) (foldr op₂ b tail)) →
    ∀ (a : α), foldr op₃ (f a b) (head :: tail) = f (foldr op₁ a (head :: tail)) (foldr op₂ b (head :: tail))
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
⊢ ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)
have nil : ∀ (a : α), foldr op₃ (f a b) [] = f (foldr op₁ a []) (foldr op₂ b [])
Tactic: induction l <;> intros <;> [rfl; simp only [*, foldr]]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
nil : ∀ (a : α), foldr op₃ (f a b) [] = f (foldr op₁ a []) (foldr op₂ b [])
⊢ ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)
have cons : ∀ (head : ι) (tail : List ι),
  (∀ (a : α), foldr op₃ (f a b) tail = f (foldr op₁ a tail) (foldr op₂ b tail)) →
    ∀ (a : α), foldr op₃ (f a b) (head :: tail) = f (foldr op₁ a (head :: tail)) (foldr op₂ b (head :: tail))
Tactic: induction l <;> intros <;> [rfl; simp only [*, foldr]]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α} (hl : ∀ (f : α → α), f ∈ lt → Injective f) (hf : Injective f), Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (foldl comp f (lh :: lt))
have cons : Injective (f ∘ lh)
Tactic: apply l_ih fun _ h => hl _ (List.mem_cons_of_mem _ h)
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α} (hl : ∀ (f : α → α), f ∈ lt → Injective f) (hf : Injective f), Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (f ∘ lh)
have cons : Injective lh
Tactic: apply Function.Injective.comp hf
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List (α → α)
f : α → α
hl : ∀ (f : α → α), f ∈ l → Injective f
hf : Injective f
⊢ Injective (foldl comp f l)
have nil : ∀ {f : α → α} (hl : ∀ (f : α → α), Membership.mem (γ := List (α → α)) [] f → Injective f) (hf : Injective f),
  Injective (foldl comp f [])
Tactic: induction l generalizing f with
  | nil => exact hf
  | cons lh lt l_ih =>
    apply l_ih fun _ h => hl _ (List.mem_cons_of_mem _ h)
    apply Function.Injective.comp hf
    apply hl _ mem_cons_self
Cleared hypotheses: l, f, hl, hf
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List (α → α)
f : α → α
hl : ∀ (f : α → α), f ∈ l → Injective f
hf : Injective f
nil :
  ∀ {f : α → α} (hl : ∀ (f : α → α), Membership.mem (γ := List (α → α)) [] f → Injective f) (hf : Injective f),
    Injective (foldl comp f [])
⊢ Injective (foldl comp f l)
have cons : ∀ (lh : α → α) (lt : List (α → α))
  (l_ih : ∀ {f : α → α} (hl : ∀ (f : α → α), f ∈ lt → Injective f) (hf : Injective f), Injective (foldl comp f lt))
  {f : α → α} (hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f) (hf : Injective f), Injective (foldl comp f (lh :: lt))
Tactic: induction l generalizing f with
  | nil => exact hf
  | cons lh lt l_ih =>
    apply l_ih fun _ h => hl _ (List.mem_cons_of_mem _ h)
    apply Function.Injective.comp hf
    apply hl _ mem_cons_self
Cleared hypotheses: l, f, hl, hf
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂
have mp : x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ → x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
mp : x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ → x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂
have mpr : x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂ → x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ → x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂
have mp : ((∃ (as : List α),
      x₂ = x₁ ++ as ∧ (as = [] ∧ a₂ = a₁ ∧ z₂ = z₁ ∨ ∃ (as' : List α), as = a₁ :: as' ∧ z₁ = as' ++ a₂ :: z₂)) ∨
    ∃ (bs : List α),
      x₁ = x₂ ++ bs ∧ (bs = [] ∧ a₁ = a₂ ∧ z₁ = z₂ ∨ ∃ (as' : List α), bs = a₂ :: as' ∧ z₂ = as' ++ a₁ :: z₁)) →
  x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂
Tactic: simp only [append_eq_append_iff, cons_eq_append_iff, cons_eq_cons]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
m : Type v → Type w
inst : Monad m
inst_1 : LawfulMonad m
f : α → β → m β
b : β
l : List α
⊢ foldrM f b l = foldr (fun (a : α) (mb : m β) ↦ mb >>= f a) (pure b) l
have nil : foldrM f b [] = foldr (fun (a : α) (mb : m β) ↦ mb >>= f a) (pure b) []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
m : Type v → Type w
inst : Monad m
inst_1 : LawfulMonad m
f : α → β → m β
b : β
l : List α
nil : foldrM f b [] = foldr (fun (a : α) (mb : m β) ↦ mb >>= f a) (pure b) []
⊢ foldrM f b l = foldr (fun (a : α) (mb : m β) ↦ mb >>= f a) (pure b) l
have cons : ∀ (head : α) (tail : List α),
  foldrM f b tail = foldr (fun (a : α) (mb : m β) ↦ mb >>= f a) (pure b) tail →
    foldrM f b (head :: tail) = foldr (fun (a : α) (mb : m β) ↦ mb >>= f a) (pure b) (head :: tail)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
m : Type v → Type w
inst : Monad m
inst_1 : LawfulMonad m
f : β → α → m β
b : β
l : List α
⊢ foldlM f b l =
    foldl
      (fun (mb : m β) (a : α) ↦ do
        let b ← mb
        f b a)
      (pure b) l
have suffices : ∀ (mb : m β),
  (do
      let b ← mb
      foldlM f b l) =
    foldl
      (fun (mb : m β) (a : α) ↦ do
        let b ← mb
        f b a)
      mb l
Tactic: suffices h :
    ∀ mb : m β, (mb >>= fun b => List.foldlM f b l) = foldl (fun mb a => mb >>= fun b => f b a) mb l
    by simp [← h (pure b)]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
m : Type v → Type w
inst : Monad m
inst_1 : LawfulMonad m
f : β → α → m β
b : β
l : List α
⊢ ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b l) =
      foldl
        (fun (mb : m β) (a : α) ↦ do
          let b ← mb
          f b a)
        mb l
have nil : ∀ (mb : m β),
  (do
      let b ← mb
      foldlM f b []) =
    foldl
      (fun (mb : m β) (a : α) ↦ do
        let b ← mb
        f b a)
      mb []
Tactic: induction l with
  | nil => simp
  | cons _ _ l_ih => intro; simp only [List.foldlM, foldl, ← l_ih, functor_norm]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
m : Type v → Type w
inst : Monad m
inst_1 : LawfulMonad m
f : β → α → m β
b : β
l : List α
nil :
  ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b []) =
      foldl
        (fun (mb : m β) (a : α) ↦ do
          let b ← mb
          f b a)
        mb []
⊢ ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b l) =
      foldl
        (fun (mb : m β) (a : α) ↦ do
          let b ← mb
          f b a)
        mb l
have cons : ∀ (head : α) (tail : List α)
  (l_ih :
    ∀ (mb : m β),
      (do
          let b ← mb
          foldlM f b tail) =
        foldl
          (fun (mb : m β) (a : α) ↦ do
            let b ← mb
            f b a)
          mb tail)
  (mb : m β),
  (do
      let b ← mb
      foldlM f b (head :: tail)) =
    foldl
      (fun (mb : m β) (a : α) ↦ do
        let b ← mb
        f b a)
      mb (head :: tail)
Tactic: induction l with
  | nil => simp
  | cons _ _ l_ih => intro; simp only [List.foldlM, foldl, ← l_ih, functor_norm]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
f : α → Bool
⊢ l.length = (filter f l).length + (filter (fun (x : α) ↦ !f x) l).length
have simp_rw : l.length = countP f l + countP (fun (x : α) ↦ !f x) l
Tactic: simp_rw [← List.countP_eq_length_filter, l.length_eq_countP_add_countP f, Bool.not_eq_true,
    Bool.decide_eq_false]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
f : α → Bool
simp_rw : l.length = countP f l + countP (fun (x : α) ↦ !f x) l
⊢ l.length = (filter f l).length + (filter (fun (x : α) ↦ !f x) l).length
have simp_rw₁ : countP f l + countP (fun (a : α) ↦ decide ¬f a = true) l = countP f l + countP (fun (x : α) ↦ !f x) l
Tactic: simp_rw [← List.countP_eq_length_filter, l.length_eq_countP_add_countP f, Bool.not_eq_true,
    Bool.decide_eq_false]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
f : α → Bool
simp_rw : l.length = countP f l + countP (fun (x : α) ↦ !f x) l
simp_rw₁ : countP f l + countP (fun (a : α) ↦ decide ¬f a = true) l = countP f l + countP (fun (x : α) ↦ !f x) l
⊢ l.length = (filter f l).length + (filter (fun (x : α) ↦ !f x) l).length
have simp_rw₂ : countP f l + countP (fun (a : α) ↦ decide (f a = false)) l = countP f l + countP (fun (x : α) ↦ !f x) l
Tactic: simp_rw [← List.countP_eq_length_filter, l.length_eq_countP_add_countP f, Bool.not_eq_true,
    Bool.decide_eq_false]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → Option β
l : List α
⊢ filterMap f l = flatMap (fun (a : α) ↦ (f a).toList) l
have nil : filterMap f [] = flatMap (fun (a : α) ↦ (f a).toList) []
Tactic: induction l with | nil => ?_ | cons a l ih => ?_
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → Option β
l : List α
nil : filterMap f [] = flatMap (fun (a : α) ↦ (f a).toList) []
⊢ filterMap f l = flatMap (fun (a : α) ↦ (f a).toList) l
have cons : ∀ (a : α) (l : List α) (ih : filterMap f l = flatMap (fun (a : α) ↦ (f a).toList) l),
  filterMap f (a :: l) = flatMap (fun (a : α) ↦ (f a).toList) (a :: l)
Tactic: induction l with | nil => ?_ | cons a l ih => ?_
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun (a : α) ↦ (f a).toList) l
⊢ filterMap f (a :: l) = flatMap (fun (a : α) ↦ (f a).toList) (a :: l)
have cons : (match (motive := Option β → List β) f a with
  | none => filterMap f l
  | some b => b :: filterMap f l) =
  (f a).toList ++ flatMap (fun (a : α) ↦ (f a).toList) l
Tactic: simp [filterMap_cons]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun (a : α) ↦ (f a).toList) l
⊢ (match (motive := Option β → List β) f a with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (f a).toList ++ flatMap (fun (a : α) ↦ (f a).toList) l
have cons : (match (motive := Option β → List β) none with
  | none => filterMap f l
  | some b => b :: filterMap f l) =
  HAppend.hAppend (α := List β) (Option.toList none) (flatMap (fun (a : α) ↦ (f a).toList) l)
Tactic: rcases f a
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun (a : α) ↦ (f a).toList) l
cons :
  (match (motive := Option β → List β) none with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    HAppend.hAppend (α := List β) (Option.toList none) (flatMap (fun (a : α) ↦ (f a).toList) l)
⊢ (match (motive := Option β → List β) f a with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (f a).toList ++ flatMap (fun (a : α) ↦ (f a).toList) l
have cons₁ : ∀ (val : β),
  (match (motive := Option β → List β) some val with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (some val).toList ++ flatMap (fun (a : α) ↦ (f a).toList) l
Tactic: rcases f a
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f g : α → Option β
l : List α
h : ∀ (x : α), x ∈ l → f x = g x
⊢ filterMap f l = filterMap g l
have nil : ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x = g x), filterMap f [] = filterMap g []
Tactic: induction l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f g : α → Option β
l : List α
h : ∀ (x : α), x ∈ l → f x = g x
nil : ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x = g x), filterMap f [] = filterMap g []
⊢ filterMap f l = filterMap g l
have cons : ∀ (head : α) (tail : List α),
  (∀ (h : ∀ (x : α), x ∈ tail → f x = g x), filterMap f tail = filterMap g tail) →
    ∀ (h : ∀ (x : α), x ∈ head :: tail → f x = g x), filterMap f (head :: tail) = filterMap g (head :: tail)
Tactic: induction l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → Option β
g : α → β
l : List α
⊢ filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
have cons : ∀ (a : α) (l : List α) (ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)),
  filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)
Tactic: induction l with | nil => simp | cons a l ih => ?_
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)
have cons : ∀ (ha : f a = none), filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)
Tactic: rcases ha : f a with - | b
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
cons : ∀ (ha : f a = none), filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)
have cons₁ : ∀ (b : β) (ha : f a = some b), filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)
Tactic: rcases ha : f a with - | b
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
ha : f a = none
h : filterMap f (a :: l) = map g (a :: l)
⊢ ∀ (x : α), x ∈ a :: l → f x = some (g x)
have this : (filterMap f l).length = l.length + 1
Tactic: have : (filterMap f l).length = l.length + 1 := by grind
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
l : List α
⊢ Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) l) []
have nil : Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) []) []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
l : List α
nil : Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) []) []
⊢ Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) l) []
have cons : ∀ (head : α) (tail : List α),
  Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) tail) [] →
    Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) (head :: tail)) []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
p : α → Bool
l : List α
⊢ filter p l = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] l
have nil : filter p [] = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
p : α → Bool
l : List α
nil : filter p [] = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] []
⊢ filter p l = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] l
have cons : ∀ (head : α) (tail : List α),
  filter p tail = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] tail →
    filter p (head :: tail) = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] (head :: tail)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
p : α → Bool
head : α
tail : List α
tail_ih : filter p tail = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] tail
⊢ filter p (head :: tail) = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] (head :: tail)
have cons : (match (motive := Bool → List α) p head with
  | true => head :: foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] tail
  | false => foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] tail) =
  bif p head then head :: foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] tail
  else foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] tail
Tactic: simp [*, filter]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
⊢ filter p l <+ filter q l
have nil : filter p [] <+ filter q []
Tactic: induction l with grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
nil : filter p [] <+ filter q []
⊢ filter p l <+ filter q l
have cons : ∀ (head : α) (tail : List α), filter p tail <+ filter q tail → filter p (head :: tail) <+ filter q (head :: tail)
Tactic: induction l with grind
Cleared hypotheses: l