awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f g : α → β → α
hd : β
tl : List β
ih : ∀ (a : α) (H : ∀ (a : α) (b : β), b ∈ tl → f a b = g a b), foldl f a tl = foldl g a tl
a : α
H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b
cons : foldl f (f a hd) tl = foldl g (g a hd) tl
⊢ foldl f a (hd :: tl) = foldl g a (hd :: tl)

Tactic:
unfold foldl

Premises used: List.foldl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f g : α → β → α
hd : β
tl : List β
ih : ∀ (a : α) (H : ∀ (a : α) (b : β), b ∈ tl → f a b = g a b), foldl f a tl = foldl g a tl
a : α
H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b
cons : foldl g (f a hd) tl = foldl g (g a hd) tl
cons₁ cons₂ : foldl g (g a hd) tl = foldl g (g a hd) tl
⊢ foldl f (f a hd) tl = foldl g (g a hd) tl

Tactic:
rw [ih _ fun a b bin => H a b <| mem_cons_of_mem _ bin, H a hd mem_cons_self]

Premises used: List.mem_cons_of_mem, List.mem_cons_self
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f g : α → β → α
a : α
l : List β
H : ∀ (a : α) (b : β), b ∈ l → f a b = g a b
nil : ∀ (a : α) (H : ∀ (a : α) (b : β), Membership.mem (γ := List β) [] b → f a b = g a b), foldl f a [] = foldl g a []
cons :
  ∀ (hd : β) (tl : List β) (ih : ∀ (a : α) (H : ∀ (a : α) (b : β), b ∈ tl → f a b = g a b), foldl f a tl = foldl g a tl)
    (a : α) (H : ∀ (a : α) (b : β), b ∈ hd :: tl → f a b = g a b), foldl f a (hd :: tl) = foldl g a (hd :: tl)
⊢ foldl f a l = foldl g a l

Tactic:
induction l generalizing a with
  | nil => rfl
  | cons hd tl ih =>
    unfold foldl
    rw [ih _ fun a b bin => H a b <| mem_cons_of_mem _ bin, H a hd mem_cons_self]

Premises used: List.foldl, List.cons, List.nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f g : α → β → β
b : β
H : ∀ (a : α), Membership.mem (γ := List α) [] a → ∀ (b : β), f a b = g a b
⊢ foldr f b [] = foldr g b []

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : ∀ (H : ∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b), foldr f b tl = foldr g b tl
H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)

Tactic:
?_
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f g : α → β → β
b : β
l : List α
H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
cons :
  ∀ (hd : α) (tl : List α) (ih : ∀ (H : ∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b), foldr f b tl = foldr g b tl)
    (H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b), foldr f b (hd :: tl) = foldr g b (hd :: tl)
⊢ foldr f b l = foldr g b l

Tactic:
induction l with | nil => rfl | cons hd tl ih => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : ∀ (H : ∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b), foldr f b tl = foldr g b tl
H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b
⊢ (∀ (b : β), f hd b = g hd b) ∧ ∀ (x : α), x ∈ tl → ∀ (b : β), f x b = g x b

Tactic:
simp only [mem_cons, or_imp, forall_and, forall_eq] at H

Premises used: forall_eq, or_imp, List.mem_cons, forall_and
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : ∀ (H : ∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b), foldr f b tl = foldr g b tl
H : (∀ (b : β), f hd b = g hd b) ∧ ∀ (x : α), x ∈ tl → ∀ (b : β), f x b = g x b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)

Tactic:
simp only [foldr, ih H.2, H.1]

Premises used: And.right, And.left, List.foldr
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : β → α → β
b : β
x : α
xs : List α
⊢ foldl f b (xs ++ [x]) = f (foldl f b xs) x

Tactic:
simp only [List.foldl_append, List.foldl]

Premises used: List.foldl, List.foldl_append
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → β → β
b : β
x : α
xs : List α
⊢ foldr f b (xs ++ [x]) = foldr f (f x b) xs

Tactic:
simp only [List.foldr_append, List.foldr]

Premises used: List.foldr_append, List.foldr
-- Module: Mathlib.Data.List.Basic
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
rw₂ rw₃ : a = a
⊢ foldl f a (b :: l) = a

Tactic:
rw [foldl_cons, hf b, foldl_fixed' hf l]

Premises used: List.foldl_cons
-- Module: Mathlib.Data.List.Basic
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
rw₂ rw₃ : b = b
⊢ foldr f b (a :: l) = b

Tactic:
rw [foldr_cons, foldr_fixed' hf l, hf a]

Premises used: List.foldr_cons
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
a : α
⊢ ∀ (l : List β), foldl (fun (a : α) (x : β) ↦ a) a l = a

Tactic:
foldl_fixed' fun _ => rfl

Premises used: List.foldl_fixed', rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
b : β
⊢ ∀ (l : List α), foldr (fun (x : α) (b : β) ↦ b) b l = b

Tactic:
foldr_fixed' fun _ => rfl

Premises used: List.foldr_fixed', rfl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
l : List α
⊢ reverse (foldl (fun (t : List α) (h : α) ↦ h :: t) [] l) = l

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
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
revert : ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l
⊢ f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l

Tactic:
revert a b
-- Module: Mathlib.Data.List.Basic
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) []
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)
⊢ ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l

Tactic:
induction l
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
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 []) (foldl op₂ b []) = foldl op₃ (f a b) []

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
head : ι
tail : List ι
tail_ih : ∀ (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:
simp only [*, foldl]

Premises used: List.foldl
-- Module: Mathlib.Data.List.Basic
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) []
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)
nil₁ : ∀ (a : α) (b : β), f (foldl op₁ a []) (foldl op₂ b []) = foldl op₃ (f a b) []
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)
nil₂ : ∀ (a : α) (b : β), f (foldl op₁ a []) (foldl op₂ b []) = foldl op₃ (f a b) []
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)
nil₃ : ∀ (a : α) (b : β), f (foldl op₁ a []) (foldl op₂ b []) = foldl op₃ (f a b) []
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)
nil₄ : ∀ (a : α) (b : β), f (foldl op₁ a []) (foldl op₂ b []) = foldl op₃ (f a b) []
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)
nil₅ : ∀ (a : α) (b : β), f (foldl op₁ a []) (foldl op₂ b []) = foldl op₃ (f a b) []
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)
⊢ ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l

Tactic:
induction l <;> intros <;> [rfl; simp only [*, foldl]]

Premises used: List.foldl
-- Module: Mathlib.Data.List.Basic
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)
revert : ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)
⊢ foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Tactic:
revert a
-- Module: Mathlib.Data.List.Basic
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 [])
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))
⊢ ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Tactic:
induction l
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
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) [] = f (foldr op₁ a []) (foldr op₂ b [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
Goal:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
f : α → β → γ
op₁ : ι → α → α
op₂ : ι → β → β
op₃ : ι → γ → γ
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)
head : ι
tail : List ι
tail_ih : ∀ (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:
simp only [*, foldr]

Premises used: List.foldr
-- Module: Mathlib.Data.List.Basic
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 [])
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))
nil₁ : ∀ (a : α), foldr op₃ (f a b) [] = f (foldr op₁ a []) (foldr op₂ b [])
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))
nil₂ : ∀ (a : α), foldr op₃ (f a b) [] = f (foldr op₁ a []) (foldr op₂ b [])
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))
nil₃ : ∀ (a : α), foldr op₃ (f a b) [] = f (foldr op₁ a []) (foldr op₂ b [])
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))
nil₄ : ∀ (a : α), foldr op₃ (f a b) [] = f (foldr op₁ a []) (foldr op₂ b [])
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))
nil₅ : ∀ (a : α), foldr op₃ (f a b) [] = f (foldr op₁ a []) (foldr op₂ b [])
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))
⊢ ∀ (a : α), foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

Tactic:
induction l <;> intros <;> [rfl; simp only [*, foldr]]

Premises used: List.foldr
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
f : α → α
hl : ∀ (f : α → α), Membership.mem (γ := List (α → α)) [] f → Injective f
hf : Injective f
⊢ Injective (foldl comp f [])

Tactic:
hf

Premises used: List.foldl
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
f : α → α
hl : ∀ (f : α → α), Membership.mem (γ := List (α → α)) [] f → Injective f
hf : Injective f
⊢ Injective (foldl comp f [])

Tactic:
exact hf
-- Module: Mathlib.Data.List.Basic
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
cons : Injective (f ∘ lh)
⊢ Injective (foldl comp f (lh :: lt))

Tactic:
apply l_ih fun _ h => hl _ (List.mem_cons_of_mem _ h)

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.List.Basic
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
cons : Injective lh
⊢ Injective (f ∘ lh)

Tactic:
apply Function.Injective.comp hf

Premises used: Function.Injective.comp
-- Module: Mathlib.Data.List.Basic
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 lh

Tactic:
apply hl _ mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.Data.List.Basic
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 [])
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))
⊢ Injective (foldl comp f l)

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

Premises used: List.cons, Function.Injective.comp, List.nil
-- Module: Mathlib.Data.List.Basic
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₂
mpr : x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂ → x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Tactic:
constructor
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
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₂
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ → x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Tactic:
simp only [append_eq_append_iff, cons_eq_append_iff, cons_eq_cons]

Premises used: List.cons_eq_cons, List.cons_eq_append_iff, List.append_eq_append_iff
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x₁ z₂ : List α
a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₂
⊢ x₁ = x₁ ++ [] ∧ a₂ = a₂ ∧ z₂ = z₂

Tactic:
simp_all
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
d : List α
notin_z : ¬a₂ ∈ d ++ a₂ :: z₂
⊢ x₁ = x₁ ++ a₁ :: d ∧ a₁ = a₂ ∧ d ++ a₂ :: z₂ = z₂

Tactic:
simp_all
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x₂ z₁ : List α
a₁ : α
notin_z : ¬a₁ ∈ z₁
notin_x : ¬a₁ ∈ x₂ ++ []
⊢ x₂ ++ [] = x₂ ∧ a₁ = a₁ ∧ z₁ = z₁

Tactic:
simp_all
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x₂ z₁ : List α
a₁ a₂ : α
notin_z : ¬a₂ ∈ z₁
d : List α
notin_x : ¬a₂ ∈ x₂ ++ a₂ :: d
⊢ x₂ ++ a₂ :: d = x₂ ∧ a₁ = a₂ ∧ z₁ = d ++ a₁ :: z₁

Tactic:
simp_all
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
x₁ z₁ : List α
a₁ : α
notin_x : ¬a₁ ∈ x₁
notin_z : ¬a₁ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₁ ++ a₁ :: z₁

Tactic:
rfl
-- Module: Mathlib.Data.List.Basic
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) []
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)
⊢ foldrM f b l = foldr (fun (a : α) (mb : m β) ↦ mb >>= f a) (pure b) l

Tactic:
induction l
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
m : Type v → Type w
inst : Monad m
inst_1 : LawfulMonad m
f : α → β → m β
b : β
⊢ foldrM f b [] = foldr (fun (a : α) (mb : m β) ↦ mb >>= f a) (pure b) []

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
m : Type v → Type w
inst : Monad m
inst_1 : LawfulMonad m
f : α → β → m β
b : β
head : α
tail : List α
tail_ih : 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:
simp [*]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
m : Type v → Type w
inst : Monad m
inst_1 : LawfulMonad m
f : β → α → m β
b : β
l : List α
h :
  ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b l) =
      foldl
        (fun (mb : m β) (a : α) ↦ do
          let b ← mb
          f b a)
        mb l
⊢ foldlM f b l =
    foldl
      (fun (mb : m β) (a : α) ↦ do
        let b ← mb
        f b a)
      (pure b) l

Tactic:
simp [← h (pure b)]

Premises used: Pure.pure
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
m : Type v → Type w
inst : Monad m
inst_1 : LawfulMonad m
f : β → α → m β
b : β
l : List α
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
⊢ foldlM f b l =
    foldl
      (fun (mb : m β) (a : α) ↦ do
        let b ← mb
        f b a)
      (pure b) 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)]
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
m : Type v → Type w
inst : Monad m
inst_1 : LawfulMonad m
f : β → α → m β
b : β
⊢ ∀ (mb : m β),
    (do
        let b ← mb
        foldlM f b []) =
      foldl
        (fun (mb : m β) (a : α) ↦ do
          let b ← mb
          f b a)
        mb []

Tactic:
simp
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
m : Type v → Type w
inst : Monad m
inst_1 : LawfulMonad m
f : β → α → m β
b : β
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:
simp only [List.foldlM, foldl, ← l_ih, functor_norm]

Premises used: List.foldlM, List.foldl
-- Module: Mathlib.Data.List.Basic
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 []
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)
⊢ ∀ (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:
induction l with
  | nil => simp
  | cons _ _ l_ih => intro; simp only [List.foldlM, foldl, ← l_ih, functor_norm]

Premises used: List.foldlM, List.foldl, List.cons, List.nil
-- Module: Mathlib.Data.List.Basic
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
simp_rw₂ : countP f l + countP (fun (a : α) ↦ decide (f a = false)) l = countP f l + countP (fun (x : α) ↦ !f x) l
⊢ l.length = (filter f l).length + (filter (fun (x : α) ↦ !f x) l).length

Tactic:
simp_rw [← List.countP_eq_length_filter, l.length_eq_countP_add_countP f, Bool.not_eq_true,
    Bool.decide_eq_false]

Premises used: List.length_eq_countP_add_countP, List.countP_eq_length_filter, Bool.not_eq_true, Bool.decide_eq_false
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → Option β
⊢ filterMap f [] = flatMap (fun (a : α) ↦ (f a).toList) []

Tactic:
?_
-- 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
⊢ filterMap f (a :: l) = flatMap (fun (a : α) ↦ (f a).toList) (a :: l)

Tactic:
?_
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → Option β
l : List α
nil : filterMap f [] = flatMap (fun (a : α) ↦ (f a).toList) []
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)
⊢ filterMap f l = flatMap (fun (a : α) ↦ (f a).toList) l

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

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Basic
Goal:
α : Type u
β : Type v
f : α → Option β
⊢ filterMap f [] = flatMap (fun (a : α) ↦ (f a).toList) []

Tactic:
simp [filterMap_cons]

Premises used: List.filterMap_cons