awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
have 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 sorry)
      (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 ?_
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
have 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 sorry)
      (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]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
p : α → Bool
⊢ 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))
have 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 sorry)
    (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]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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)
⊢ 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))
have 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 sorry x) : α))
    (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]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: simp_rw [map_map, comp_def, Subtype.map, id, ← Function.comp_apply (g := Subtype.val),
      ← filter_map, attach_map_subtype_val]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: simp_rw [map_map, comp_def, Subtype.map, id, ← Function.comp_apply (g := Subtype.val),
      ← filter_map, attach_map_subtype_val]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: simp_rw [map_map, comp_def, Subtype.map, id, ← Function.comp_apply (g := Subtype.val),
      ← filter_map, attach_map_subtype_val]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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)
⊢ 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))
have 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
Tactic: simp_rw [map_map, comp_def, Subtype.map, id, ← Function.comp_apply (g := Subtype.val),
      ← filter_map, attach_map_subtype_val]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
⊢ filter (fun (x : α) ↦ true) l = l
have nil : Eq.{u + 1} (α := List α) (filter (fun (x : α) ↦ true) []) []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
nil : Eq.{u + 1} (α := List α) (filter (fun (x : α) ↦ true) []) []
⊢ filter (fun (x : α) ↦ true) l = l
have cons : ∀ (head : α) (tail : List α),
  filter (fun (x : α) ↦ true) tail = tail → filter (fun (x : α) ↦ true) (head :: tail) = head :: tail
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
⊢ filter (fun (x : α) ↦ false) l = []
have nil : Eq.{u + 1} (α := List α) (filter (fun (x : α) ↦ false) []) []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l : List α
nil : Eq.{u + 1} (α := List α) (filter (fun (x : α) ↦ false) []) []
⊢ filter (fun (x : α) ↦ false) l = []
have cons : ∀ (head : α) (tail : List α), filter (fun (x : α) ↦ false) tail = [] → filter (fun (x : α) ↦ false) (head :: tail) = []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
inst : BEq α
inst_1 : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ (l.erase a).length + 1 = l.length
have rw : (eraseP (fun (x : α) ↦ a == x) l).length + 1 = l.length
Tactic: rw [erase_eq_eraseP, length_eraseP_add_one h BEq.rfl]
-- 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 : (eraseP (fun (x : α) ↦ a == x) l).length + 1 = l.length
⊢ (l.erase a).length + 1 = l.length
have rw₁ : l.length = l.length
Tactic: rw [erase_eq_eraseP, length_eraseP_add_one h BEq.rfl]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
have h : ∀ (b : α), (a == b) = (f a == f b)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Data.List.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
⊢ map f (l.erase a) = (map f l).erase (f a)
have this : 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]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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 (l.erase a) = (map f l).erase (f a)
have rw : map f (eraseP (fun (x : α) ↦ f a == f x) l) = map f (eraseP ((fun (x : β) ↦ f a == x) ∘ f) l)
Tactic: rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_map, this]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
l₁ l₂ : List α
⊢ map f (foldl List.erase l₁ l₂) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) l₂
have nil : ∀ {l₁ : List α}, map f (foldl List.erase l₁ []) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) []
Tactic: induction l₂ generalizing l₁
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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₁) []
⊢ map f (foldl List.erase l₁ l₂) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) l₂
have 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)
Tactic: induction l₂ generalizing l₁
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
f : α → β
finj : Injective f
l₁ l₂ : List α
⊢ map f (foldl List.erase l₁ l₂) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) l₂
have nil : ∀ {l₁ : List α}, map f (foldl List.erase l₁ []) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) []
Tactic: induction l₂ generalizing l₁ <;> [rfl; simp only [foldl_cons, map_erase finj, *]]
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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₁) []
⊢ map f (foldl List.erase l₁ l₂) = foldl (fun (l : List β) (a : α) ↦ l.erase (f a)) (map f l₁) l₂
have 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)
Tactic: induction l₂ generalizing l₁ <;> [rfl; simp only [foldl_cons, map_erase finj, *]]
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
i : ℕ
hi : i < (a :: l).length
⊢ (a :: l).erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) (a :: l) i hi) ~ (a :: l).eraseIdx i
have cons : ∀ (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: cases i with grind
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
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
i : ℕ
hi : i < (a :: l).length
cons :
  ∀ (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
⊢ (a :: l).erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) (a :: l) i hi) ~ (a :: l).eraseIdx i
have cons₁ : ∀ (n : ℕ) (hi : n + 1 < (a :: l).length),
  (a :: l).erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) (a :: l) (n + 1) hi) ~
    (a :: l).eraseIdx (n + 1)
Tactic: cases i with grind
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
inst : BEq ι
inst_1 : LawfulBEq ι
l : List ι
i : ℕ
hi : i < l.length
⊢ l.erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l i hi) ~ l.eraseIdx i
have nil : ∀ {i : ℕ} (hi : i < length.{u_1} (α := ι) []),
  List.erase [] (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) [] i hi) ~ eraseIdx [] i
Tactic: induction l generalizing i with
  | nil => simp
  | cons a l IH => cases i with grind
Cleared hypotheses: l, i, hi
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
ι : Type u_1
inst : BEq ι
inst_1 : LawfulBEq ι
l : List ι
i : ℕ
hi : i < l.length
nil :
  ∀ {i : ℕ} (hi : i < length.{u_1} (α := ι) []),
    List.erase [] (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) [] i hi) ~ eraseIdx [] i
⊢ l.erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l i hi) ~ l.eraseIdx i
have cons : ∀ (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)
  {i : ℕ} (hi : i < (a :: l).length),
  (a :: l).erase (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) (a :: l) i hi) ~ (a :: l).eraseIdx i
Tactic: induction l generalizing i with
  | nil => simp
  | cons a l IH => cases i with grind
Cleared hypotheses: l, i, hi
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
p : α → Prop
x : α
l : List α
⊢ Forall p (x :: l) ↔ ∀ (x_1 : α), x_1 ∈ x :: l → p x_1
have rw : Forall p (x :: l) ↔ p x ∧ ∀ (x : α), x ∈ l → p x
Tactic: rw [forall_mem_cons, forall_cons, forall_iff_forall_mem]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
p : α → Prop
x : α
l : List α
rw : Forall p (x :: l) ↔ p x ∧ ∀ (x : α), x ∈ l → p x
⊢ Forall p (x :: l) ↔ ∀ (x_1 : α), x_1 ∈ x :: l → p x_1
have rw₁ : p x ∧ Forall p l ↔ p x ∧ ∀ (x : α), x ∈ l → p x
Tactic: rw [forall_mem_cons, forall_cons, forall_iff_forall_mem]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
p : α → Prop
x : α
l : List α
rw : Forall p (x :: l) ↔ p x ∧ ∀ (x : α), x ∈ l → p x
rw₁ : p x ∧ Forall p l ↔ p x ∧ ∀ (x : α), x ∈ l → p x
⊢ Forall p (x :: l) ↔ ∀ (x_1 : α), x_1 ∈ x :: l → p x_1
have rw₂ : (p x ∧ ∀ (x : α), x ∈ l → p x) ↔ p x ∧ ∀ (x : α), x ∈ l → p x
Tactic: rw [forall_mem_cons, forall_cons, forall_iff_forall_mem]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ Forall p (x :: l) → Forall q (x :: l)
have simp : p x → Forall p l → q x ∧ Forall q l
Tactic: simp only [forall_cons, and_imp]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x → Forall p l → q x ∧ Forall q l
have rw : p x ∧ Forall p l → q x ∧ Forall q l
Tactic: rw [← and_imp]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
⊢ Forall p (map f l) ↔ Forall (p ∘ f) l
have nil : Forall p (map f []) ↔ Forall (p ∘ f) []
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
nil : Forall p (map f []) ↔ Forall (p ∘ f) []
⊢ Forall p (map f l) ↔ Forall (p ∘ f) l
have cons : ∀ (head : α) (tail : List α),
  (Forall p (map f tail) ↔ Forall (p ∘ f) tail) → (Forall p (map f (head :: tail)) ↔ Forall (p ∘ f) (head :: tail))
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
⊢ (pmap (P := p) f s hs).Disjoint (pmap (P := p) f t ht)
have simp : ∀ ⦃a : β⦄, (∃ (a_1 : α), ∃ (h : a_1 ∈ s), f a_1 sorry = a) → (∃ (a_2 : α), ∃ (h : a_2 ∈ t), f a_2 sorry = a) → False
Tactic: simp only [Disjoint, mem_pmap]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ False
have apply : a ∈ t
Tactic: apply h ha
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s t : List α
hf : Injective f
h : s.Disjoint t
⊢ (map f s).Disjoint (map f t)
have rw : Disjoint.{v} (α := β) (pmap (P := fun (x : α) ↦ True) (fun (a : α) (x : True) ↦ f a) s sorry)
  (pmap (P := fun (x : α) ↦ True) (fun (a : α) (x : True) ↦ f a) t sorry)
Tactic: rw [← pmap_eq_map (fun _ _ ↦ trivial), ← pmap_eq_map (fun _ _ ↦ trivial)]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l.Disjoint l₁ ↔ l.Disjoint l₂
have simp_rw : (∀ ⦃a : α⦄, a ∈ l₁ → ¬a ∈ l) ↔ ∀ ⦃a : α⦄, a ∈ l₂ → ¬a ∈ l
Tactic: simp_rw [List.disjoint_right, p.mem_iff]
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
f : α → β
a : α
as : List α
h : a ∈ as
⊢ lookup a (map (fun (x : α) ↦ (x, f x)) as) = some (f a)
have nil : ∀ (h : Membership.mem (γ := List α) [] a), lookup a (map (fun (x : α) ↦ (x, f x)) []) = some (f a)
Tactic: induction as with grind
Cleared hypotheses: as, h
-- Lean 4 proof step from Mathlib.Data.List.Basic (goal)
Goal:
α : Type u
β : Type v
inst : BEq α
inst_1 : LawfulBEq α
f : α → β
a : α
as : List α
h : a ∈ as
nil : ∀ (h : Membership.mem (γ := List α) [] a), lookup a (map (fun (x : α) ↦ (x, f x)) []) = some (f a)
⊢ lookup a (map (fun (x : α) ↦ (x, f x)) as) = some (f a)
have cons : ∀ (head : α) (tail : List α),
  (∀ (h : a ∈ tail), lookup a (map (fun (x : α) ↦ (x, f x)) tail) = some (f a)) →
    ∀ (h : a ∈ head :: tail), lookup a (map (fun (x : α) ↦ (x, f x)) (head :: tail)) = some (f a)
Tactic: induction as with grind
Cleared hypotheses: as, h