awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Basic
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 β) f a with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (f a).toList ++ flatMap (fun (a : α) ↦ (f a).toList) l
⊢ filterMap f (a :: l) = flatMap (fun (a : α) ↦ (f a).toList) (a :: l)

Tactic:
simp [filterMap_cons]

Premises used: List.filterMap_cons
-- Module: Mathlib.Data.List.Basic
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)
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
⊢ (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:
rcases f a
-- Module: Mathlib.Data.List.Basic
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 β) 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:
simp [ih]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun (a : α) ↦ (f a).toList) l
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:
simp [ih]
-- Module: Mathlib.Data.List.Basic
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 []
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)
⊢ filterMap f l = filterMap g l

Tactic:
induction l
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f g : α → Option β
h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x = g x
⊢ filterMap f [] = filterMap g []

Tactic:
simp_all [filterMap_cons]

Premises used: List.filterMap_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f g : α → Option β
head : α
tail : List α
tail_ih : ∀ (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:
simp_all [filterMap_cons]

Premises used: List.filterMap_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → Option β
g : α → β
⊢ filterMap f [] = map g [] → ∀ (x : α), Membership.mem (γ := List α) [] x → f x = some (g x)

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
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)

Tactic:
?_
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → Option β
g : α → β
l : List α
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)
⊢ filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)

Tactic:
induction l with | nil => simp | cons a l ih => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Basic
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)
cons₁ : ∀ (b : β) (ha : f a = some b), 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)

Tactic:
rcases ha : f a with - | b
-- Module: Mathlib.Data.List.Basic
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)
⊢ (filterMap f l).length = l.length + 1

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
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)
⊢ (filterMap f l).length = l.length + 1

Tactic:
have : (filterMap f l).length = l.length + 1 := by grind
-- Module: Mathlib.Data.List.Basic
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)
this : (filterMap f l).length = l.length + 1
⊢ ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
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)
b : β
ha : f a = some b
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
simp +contextual [ha, ih]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → Option β
g : α → β
l : List α
h : ∀ (x : α), x ∈ l → f x = some (g x)
⊢ ∀ (x : α), x ∈ l → f x = (some ∘ g) x

Tactic:
simpa
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
l : List α
nil : Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) []) []
cons :
  ∀ (head : α) (tail : List α),
    Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) tail) [] →
      Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) (head :: tail)) []
⊢ Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) l) []

Tactic:
induction l
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
⊢ Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) []) []

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
head : α
tail : List α
tail_ih : Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) tail) []
⊢ Eq.{v + 1} (α := List β) (filterMap (fun (x : α) ↦ none) (head :: tail)) []

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Bool
a : α
⊢ filter p [a] = bif p a then [a] else []

Tactic:
rfl

Premises used: cond, List.filter, rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Bool
l : List α
nil : filter p [] = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] []
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)
⊢ filter p l = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] l

Tactic:
induction l
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Bool
⊢ filter p [] = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] []

Tactic:
simp [*, filter]

Premises used: List.filter
-- Module: Mathlib.Data.List.Basic
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
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
⊢ filter p (head :: tail) = foldr (fun (a : α) (out : List α) ↦ bif p a then a :: out else out) [] (head :: tail)

Tactic:
simp [*, filter]

Premises used: List.filter
-- Module: Mathlib.Data.List.Basic
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
⊢ (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:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Bool
l : List α
⊢ filter p l ⊆ l

Tactic:
filter_sublist.subset

Premises used: List.filter_sublist, List.Sublist.subset
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Bool
a : α
l : List α
h : a ∈ filter p l
⊢ p a = true

Tactic:
(mem_filter.1 h).2

Premises used: And.right, List.mem_filter, Iff.mp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Bool
a : α
l : List α
h : a ∈ filter p l
⊢ a ∈ l

Tactic:
filter_subset_self l h

Premises used: List.filter_subset_self
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Bool
a : α
l : List α
h₁ : a ∈ l
h₂ : p a = true
⊢ a ∈ filter p l

Tactic:
mem_filter.2 ⟨h₁, h₂⟩

Premises used: Iff.mpr, And.intro, List.mem_filter
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
⊢ filter p [] <+ filter q []

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
head : α
tail : List α
tail_ih : filter p tail <+ filter q tail
⊢ filter p (head :: tail) <+ filter q (head :: tail)

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
nil : filter p [] <+ filter q []
cons : ∀ (head : α) (tail : List α), filter p tail <+ filter q tail → filter p (head :: tail) <+ filter q (head :: tail)
⊢ filter p l <+ filter q l

Tactic:
induction l with grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
p : α → Bool
f : α → β
hf : Injective f
l : List α
inst : DecidablePred fun (b : β) ↦ ∃ (a : α), p a = true ∧ f a = b
⊢ map f (filter p l) = filter (fun (b : β) ↦ decide (∃ (a : α), p a = true ∧ f a = b)) (map f l)

Tactic:
simp [comp_def, filter_map, hf.eq_iff]

Premises used: List.filter_map, Function.Injective.eq_iff, Function.comp_def
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p : { a : α // a ∈ l } → Bool
inst : DecidableEq α
⊢ filter p l.attach =
    map
      (Subtype.map (p := fun (x : α) ↦
        x ∈ filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l) (q :=
        Membership.mem l) id ⋯)
      (filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l).attach

Tactic:
map_injective_iff.2 Subtype.coe_injective ?_

Premises used: Iff.mpr, Subtype.coe_injective, List.map_injective_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p : { a : α // a ∈ l } → Bool
inst : DecidableEq α
refine :
  Eq (α := List α) (map (fun (a : { a : α // a ∈ l }) ↦ (↑a : α)) (filter p l.attach))
    (map (fun (a : { a : α // a ∈ l }) ↦ (↑a : α))
      (map
        (Subtype.map (p := fun (x : α) ↦
          x ∈ filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l)
          (q := Membership.mem l) id ⋯)
        (filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l).attach))
⊢ filter p l.attach =
    map
      (Subtype.map (p := fun (x : α) ↦
        x ∈ filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l) (q :=
        Membership.mem l) id ⋯)
      (filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l).attach

Tactic:
refine map_injective_iff.2 Subtype.coe_injective ?_

Premises used: Iff.mpr, Subtype.coe_injective, List.map_injective_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p : { a : α // a ∈ l } → Bool
inst : DecidableEq α
⊢ Eq (α := List α) (map (fun (a : { a : α // a ∈ l }) ↦ (↑a : α)) (filter p l.attach))
    (map (fun (a : { a : α // a ∈ l }) ↦ (↑a : α))
      (map
        (Subtype.map (p := fun (x : α) ↦
          x ∈ filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l)
          (q := Membership.mem l) id ⋯)
        (filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l).attach))

Tactic:
simp [comp_def, map_filter _ Subtype.coe_injective]

Premises used: List.map_filter, Subtype.coe_injective, Function.comp_def
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p : { a : α // a ∈ l } → Bool
inst : DecidableEq α
refine :
  Eq (α := List α) (map (fun (a : { a : α // a ∈ l }) ↦ (↑a : α)) (filter p l.attach))
    (map (fun (a : { a : α // a ∈ l }) ↦ (↑a : α))
      (map
        (Subtype.map (p := fun (x : α) ↦
          x ∈ filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l)
          (q := Membership.mem l) id ⋯)
        (filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l).attach))
⊢ filter p l.attach =
    map
      (Subtype.map (p := fun (x : α) ↦
        x ∈ filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l) (q :=
        Membership.mem l) id ⋯)
      (filter (fun (x : α) ↦ decide (∃ (h : x ∈ l), p (Subtype.mk (p := fun (a : α) ↦ a ∈ l) x h) = true)) l).attach

Tactic:
classical
  refine map_injective_iff.2 Subtype.coe_injective ?_
  simp [comp_def, map_filter _ Subtype.coe_injective]

Premises used: Iff.mpr, List.map_filter, Subtype.coe_injective, Function.comp_def, List.map_injective_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
p : α → Bool
simp_rw :
  Eq (α := List α)
    (map (fun (a : { x : α // x ∈ l }) ↦ (↑a : α)) (filter (fun (x : { x : α // x ∈ l }) ↦ p (↑x : α)) l.attach))
    (map
      ((fun (a : { x : α // x ∈ l }) ↦ (↑a : α)) ∘
        Subtype.map (p := fun (x : α) ↦ x ∈ filter p l) (q := Membership.mem l) id ⋯)
      (filter p l).attach)
simp_rw₁ :
  Eq (α := List α)
    (map (fun (a : { x : α // x ∈ l }) ↦ (↑a : α)) (filter (fun (x : { x : α // x ∈ l }) ↦ p (↑x : α)) l.attach))
    (map
      (fun (x : { x : α // x ∈ filter p l }) ↦
        (↑(Subtype.map (p := fun (x : α) ↦ x ∈ filter p l) (q := Membership.mem l) id ⋯ x) : α))
      (filter p l).attach)
simp_rw₂ :
  Eq (α := List α)
    (map (fun (a : { x : α // x ∈ l }) ↦ (↑a : α)) (filter (fun (x : { x : α // x ∈ l }) ↦ p (↑x : α)) l.attach))
    (map (fun (x : { x : α // x ∈ filter p l }) ↦ id (↑x : α)) (filter p l).attach)
simp_rw₃ :
  Eq (α := List α)
    (map (fun (a : { x : α // x ∈ l }) ↦ (↑a : α)) (filter (fun (x : { x : α // x ∈ l }) ↦ p (↑x : α)) l.attach))
    (map (fun (x : { x : α // x ∈ filter p l }) ↦ (↑x : α)) (filter p l).attach)
simp_rw₄ :
  Eq (α := List α)
    (map (fun (a : { x : α // x ∈ l }) ↦ (↑a : α))
      (filter (fun (x : { x : α // x ∈ l }) ↦ (p ∘ Subtype.val (p := fun (x : α) ↦ x ∈ l)) x) l.attach))
    (map (fun (x : { x : α // x ∈ filter p l }) ↦ (↑x : α)) (filter p l).attach)
simp_rw₅ :
  filter p (map (fun (a : { x : α // x ∈ l }) ↦ (↑a : α)) l.attach) =
    map (fun (x : { x : α // x ∈ filter p l }) ↦ (↑x : α)) (filter p l).attach
⊢ Eq (α := List α)
    (map (fun (a : { x : α // x ∈ l }) ↦ (↑a : α)) (filter (fun (x : { x : α // x ∈ l }) ↦ p (↑x : α)) l.attach))
    (map (fun (a : { x : α // x ∈ l }) ↦ (↑a : α))
      (map (Subtype.map (p := fun (x : α) ↦ x ∈ filter p l) (q := Membership.mem l) id ⋯) (filter p l).attach))

Tactic:
simp_rw [map_map, comp_def, Subtype.map, id, ← Function.comp_apply (g := Subtype.val),
      ← filter_map, attach_map_subtype_val]

Premises used: Subtype.map, List.filter_map, id, List.map_map, Function.comp_def, Function.comp_apply, List.attach_map_subtype_val
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p q : α → Bool
l : List α
⊢ filter p (filter q l) = filter q (filter p l)

Tactic:
simp [Bool.and_comm]

Premises used: Bool.and_comm
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
nil : Eq.{u + 1} (α := List α) (filter (fun (x : α) ↦ true) []) []
cons :
  ∀ (head : α) (tail : List α),
    filter (fun (x : α) ↦ true) tail = tail → filter (fun (x : α) ↦ true) (head :: tail) = head :: tail
⊢ filter (fun (x : α) ↦ true) l = l

Tactic:
induction l
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List α) (filter (fun (x : α) ↦ true) []) []

Tactic:
simp [*, filter]

Premises used: List.filter
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
head : α
tail : List α
tail_ih : filter (fun (x : α) ↦ true) tail = tail
⊢ filter (fun (x : α) ↦ true) (head :: tail) = head :: tail

Tactic:
simp [*, filter]

Premises used: List.filter
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
nil : Eq.{u + 1} (α := List α) (filter (fun (x : α) ↦ false) []) []
cons :
  ∀ (head : α) (tail : List α),
    filter (fun (x : α) ↦ false) tail = [] → filter (fun (x : α) ↦ false) (head :: tail) = []
⊢ filter (fun (x : α) ↦ false) l = []

Tactic:
induction l
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List α) (filter (fun (x : α) ↦ false) []) []

Tactic:
simp [*, filter]

Premises used: List.filter
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
head : α
tail : List α
tail_ih : filter (fun (x : α) ↦ false) tail = []
⊢ filter (fun (x : α) ↦ false) (head :: tail) = []

Tactic:
simp [*, filter]

Premises used: List.filter
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
⊢ (eraseP p l).length + 1 = l.length

Tactic:
grind
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l : List α
h : a ∈ l
rw : (eraseP (fun (x : α) ↦ a == x) l).length + 1 = l.length
rw₁ rw₂ : l.length = l.length
⊢ (l.erase a).length + 1 = l.length

Tactic:
rw [erase_eq_eraseP, length_eraseP_add_one h BEq.rfl]

Premises used: BEq.rfl, List.erase_eq_eraseP, List.length_eraseP_add_one
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
h : ∀ (b : α), (a == b) = (f a == f b)
⊢ Eq.{u + 1} (α := α → Bool) (fun (x : α) ↦ a == x) fun (x : α) ↦ f a == f x

Tactic:
ext b
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
b : α
⊢ (a == b) = (f a == f b)

Tactic:
simp [finj.eq_iff]

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
⊢ Eq.{u + 1} (α := α → Bool) (fun (x : α) ↦ a == x) fun (x : α) ↦ f a == f x

Tactic:
have this : (a == ·) = (f a == f ·) := by ext b; simp [finj.eq_iff]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : Eq.{u + 1} (α := α → Bool) (fun (x : α) ↦ a == x) fun (x : α) ↦ f a == f x
rw : map f (eraseP (fun (x : α) ↦ f a == f x) l) = map f (eraseP ((fun (x : β) ↦ f a == x) ∘ f) l)
⊢ map f (l.erase a) = (map f l).erase (f a)

Tactic:
rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_map, this]

Premises used: List.erase_eq_eraseP, List.eraseP_map
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : Eq.{u + 1} (α := α → Bool) (fun (x : α) ↦ a == x) fun (x : α) ↦ f a == f x
⊢ map f (eraseP (fun (x : α) ↦ f a == f x) l) = map f (eraseP ((fun (x : β) ↦ f a == x) ∘ f) l)

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
l₁ l₂ : List α
nil : ∀ {l₁ : List α}, map f (foldl List.erase l₁ []) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) []
cons :
  ∀ (head : α) (tail : List α),
    (∀ {l₁ : List α},
        map f (foldl List.erase l₁ tail) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) tail) →
      ∀ {l₁ : List α},
        map f (foldl List.erase l₁ (head :: tail)) =
          foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) (head :: tail)
⊢ map f (foldl List.erase l₁ l₂) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) l₂

Tactic:
induction l₂ generalizing l₁
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
l₁ : List α
⊢ map f (foldl List.erase l₁ []) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) []

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
head : α
tail : List α
tail_ih :
  ∀ {l₁ : List α}, map f (foldl List.erase l₁ tail) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) tail
l₁ : List α
⊢ map f (foldl List.erase l₁ (head :: tail)) =
    foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) (head :: tail)

Tactic:
simp only [foldl_cons, map_erase finj, *]

Premises used: List.map_erase, List.foldl_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
l₁ l₂ : List α
nil : ∀ {l₁ : List α}, map f (foldl List.erase l₁ []) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) []
cons :
  ∀ (head : α) (tail : List α),
    (∀ {l₁ : List α},
        map f (foldl List.erase l₁ tail) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) tail) →
      ∀ {l₁ : List α},
        map f (foldl List.erase l₁ (head :: tail)) =
          foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) (head :: tail)
nil₁ : ∀ {l₁ : List α}, map f (foldl List.erase l₁ []) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) []
cons₁ :
  ∀ (head : α) (tail : List α),
    (∀ {l₁ : List α},
        map f (foldl List.erase l₁ tail) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) tail) →
      ∀ {l₁ : List α},
        map f (foldl List.erase l₁ (head :: tail)) =
          foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) (head :: tail)
⊢ map f (foldl List.erase l₁ l₂) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) l₂

Tactic:
induction l₂ generalizing l₁ <;> [rfl; simp only [foldl_cons, map_erase finj, *]]

Premises used: List.map_erase, List.foldl_cons
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
inst : BEq ι
inst_1 : LawfulBEq ι
i : ℕ
hi : i < length.{u_1} (α := ι) []
⊢ List.erase [] (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) [] i hi) ~ eraseIdx [] i

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
inst : BEq ι
inst_1 : LawfulBEq ι
a : ι
l : List ι
IH :
  ∀ {i : ℕ} (hi : i < l.length),
    l.erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l i hi) ~ l.eraseIdx i
hi : 0 < (a :: l).length
⊢ (a :: l).erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) (a :: l) 0 hi) ~ (a :: l).eraseIdx 0

Tactic:
grind