awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
succ :
  ∀ (x : α),
    (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
        hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
          (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x) =
      Fix.approx (β := β) f (n + 1) x
⊢ (fun (x : α) ↦
      assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
        hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
          (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x) =
    Fix.approx (β := β) f (n + 1)

Tactic:
ext : 1
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x_1 : α
apply : (↑z : ℕ) < Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h'
⊢ ¬(Fix.approx (β := β) f (↑z : ℕ) x).Dom

Tactic:
apply Nat.find_min h'

Premises used: Nat.find_min
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x_1 : α
⊢ (↑z : ℕ) < Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h'

Tactic:
lia
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x_1 : α
⊢ ¬(Fix.approx (β := β) f (↑z : ℕ) x).Dom

Tactic:
have hh : ¬(Fix.approx f z.val x).Dom := by
      apply Nat.find_min h'
      lia
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + 1 + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x_1 : α
hh : ¬(Fix.approx (β := β) f (↑z : ℕ) x).Dom
succ :
  ∀ (_this : p (n + (↑z : ℕ).succ))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ).succ) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y) (x_2 : α) (hh : ¬(Fix.approx (β := β) f (↑z : ℕ) x).Dom),
    (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
        hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
          (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x_2) =
      Fix.approx (β := β) f (n + 1) x_2
⊢ (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x_1) =
    Fix.approx (β := β) f (n + 1) x_1

Tactic:
rw [succ_add_eq_add_succ] at _this hk

Premises used: Nat.succ_add_eq_add_succ
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f n.succ x'
z : Upto p
_this : p (n + (↑z : ℕ).succ)
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ).succ
x' : α
hwf : WellFounded fun (y x : Upto p) ↦ x < y
x_1 : α
hh : ¬(Fix.approx (β := β) f (↑z : ℕ) x).Dom
succ :
  hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y) (fixAux (β := β) f (p := p))
      (z.succ (p := p) hh) x_1 =
    Fix.approx (β := β) f (n + 1) x_1
succ₁ succ₂ : Fix.approx (β := β) f n.succ x_1 = Fix.approx (β := β) f (n + 1) x_1
⊢ (assert (¬p (↑z : ℕ)) fun (h : ¬p (↑z : ℕ)) ↦
      hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) (z.succ (p := p) h) x_1) =
    Fix.approx (β := β) f (n + 1) x_1

Tactic:
rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]

Premises used: Nat.Upto.succ, Part.assert_pos
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
p : (i : ℕ) → Prop := fun (i : ℕ) ↦ (Fix.approx (β := β) f i x).Dom
k : ℕ
z : Upto p
_this : p (k + (↑z : ℕ))
hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = k + (↑z : ℕ)
zero :
  ∀ (z : Upto p) (_this : p (0 + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = 0 + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f (Nat.succ 0) x'
succ :
  ∀ (n : ℕ)
    (n_ih :
      ∀ (z : Upto p) (_this : p (n + (↑z : ℕ)))
        (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + (↑z : ℕ)) (x' : α)
        (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
        hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
            (fixAux (β := β) f (p := p)) z x' =
          Fix.approx (β := β) f n.succ x')
    (z : Upto p) (_this : p (n + 1 + (↑z : ℕ)))
    (hk : Nat.find (p := fun (n : ℕ) ↦ (Fix.approx (β := β) f n x).Dom) h' = n + 1 + (↑z : ℕ)) (x' : α)
    (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f (n + 1).succ x'
⊢ ∀ (x' : α) (hwf : WellFounded fun (y x : Upto p) ↦ x < y),
    hwf.fix (C := fun (y : Upto p) ↦ (a : α) → Part (β a)) (r := fun (y x : Upto p) ↦ x < y)
        (fixAux (β := β) f (p := p)) z x' =
      Fix.approx (β := β) f k.succ x'

Tactic:
induction k generalizing z with
  | zero =>
    intro x' _
    rw [Fix.approx, WellFounded.fix_eq, fixAux]
    congr
    ext x : 1
    rw [assert_neg]
    · rfl
    · rw [Nat.zero_add] at _this
      simpa only [not_not, Coe]
  | succ n n_ih =>
    intro x' _
    rw [Fix.approx, WellFounded.fix_eq, fixAux]
    congr
    ext : 1
    have hh : ¬(Fix.approx f z.val x).Dom := by
      apply Nat.find_min h'
      lia
    rw [succ_add_eq_add_succ] at _this hk
    rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]

Premises used: Classical.not_not, Part.assert_neg, WellFounded.fix_eq, Part.Fix.approx, Nat.zero_add, Coe, Nat.succ_add_eq_add_succ, Part.fixAux
-- Module: Mathlib.Control.Fix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ¬∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom
rw rw₁ : Eq.{u_2 + 1} (α := Part (β x)) none none
⊢ Eq.{u_2 + 1} (α := Part (β x))
    (assert (∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom) fun (h : ∃ (i : ℕ), (Fix.approx (β := β) f i x).Dom) ↦
      ⋯.fix (C := fun (y : Upto fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom) ↦ (a : α) → Part (β a)) (r :=
        Upto.GT fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)
        (fixAux (β := β) f (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom))
        (Upto.zero (p := fun (x_1 : ℕ) ↦ (Fix.approx (β := β) f x_1 x).Dom)) x)
    none

Tactic:
rw [assert_neg h']

Premises used: Part.assert_neg
-- Module: Mathlib.Control.Fold
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
f : β → α → β
x y : FreeMonoid α
simp :
  op
      (↾fun (a : β) ↦
        List.foldl f (List.foldl f a ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x))
          ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)) =
    HMul.hMul (α := Foldl β) (op (↾fun (a : β) ↦ List.foldl f a ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)))
      (op (↾fun (a : β) ↦ List.foldl f a ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)))
⊢ op (↾flip (List.foldl f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y))) =
    op (↾flip (List.foldl f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)) *
      op (↾flip (List.foldl f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y))

Tactic:
simp only [FreeMonoid.toList_mul, List.foldl_append, Function.flip_def]

Premises used: FreeMonoid.toList_mul, Function.flip_def, List.foldl_append
-- Module: Mathlib.Control.Fold
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
f : β → α → β
x y : FreeMonoid α
⊢ op
      (↾fun (a : β) ↦
        List.foldl f (List.foldl f a ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x))
          ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)) =
    HMul.hMul (α := Foldl β) (op (↾fun (a : β) ↦ List.foldl f a ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)))
      (op (↾fun (a : β) ↦ List.foldl f a ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)))

Tactic:
rfl
-- Module: Mathlib.Control.Fold
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
f : α → β → β
x x_1 : FreeMonoid α
h :
  ConcreteCategory.hom (FC := TypeCat.Fun)
      (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * x_1))) =
    ConcreteCategory.hom (FC := TypeCat.Fun)
      (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
        ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x_1))
⊢ ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * x_1)) =
    ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
      ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x_1)

Tactic:
apply ConcreteCategory.ext

Premises used: CategoryTheory.ConcreteCategory.ext
-- Module: Mathlib.Control.Fold
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
f : α → β → β
x x_1 : FreeMonoid α
h :
  ∀ (x_2 : β),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * x_1)))).toFun
        x_2 =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
              ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x_1))).toFun
        x_2
⊢ ConcreteCategory.hom (FC := TypeCat.Fun)
      (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * x_1))) =
    ConcreteCategory.hom (FC := TypeCat.Fun)
      (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
        ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x_1))

Tactic:
ext
-- Module: Mathlib.Control.Fold
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
f : α → β → β
x x_1 : FreeMonoid α
x_2 : β
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * x_1)))).toFun
      x_2 =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
            ↾flip (List.foldr f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x_1))).toFun
      x_2

Tactic:
apply List.foldr_append

Premises used: List.foldr_append
-- Module: Mathlib.Control.Fold
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
inst_1 : LawfulMonad m
f : β → α → m β
x y : FreeMonoid α
a :
  unop (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y)))) =
    unop
      (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)) *
        op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)))
⊢ op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y))) =
    op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)) *
      op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y))

Tactic:
apply unop_injective

Premises used: MulOpposite.unop_injective
-- Module: Mathlib.Control.Fold
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
inst_1 : LawfulMonad m
f : β → α → m β
x y : FreeMonoid α
a :
  ∀ (x_1 : KleisliCat.mk m β),
    unop (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y)))) x_1 =
      unop
        (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)) *
          op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)))
        x_1
⊢ unop (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y)))) =
    unop
      (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)) *
        op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)))

Tactic:
funext
-- Module: Mathlib.Control.Fold
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
inst_1 : LawfulMonad m
f : β → α → m β
x y : FreeMonoid α
x_1 : KleisliCat.mk m β
⊢ unop (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y)))) x_1 =
    unop
      (op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x)) *
        op (flip (List.foldlM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)))
      x_1

Tactic:
apply List.foldlM_append

Premises used: List.foldlM_append
-- Module: Mathlib.Control.Fold
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
inst_1 : LawfulMonad m
f : α → β → m β
x y : FreeMonoid α
h :
  ∀ (x_1 : KleisliCat.mk m β),
    flip (List.foldrM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y)) x_1 =
      (flip (List.foldrM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
          flip (List.foldrM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y))
        x_1
⊢ flip (List.foldrM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y)) =
    flip (List.foldrM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
      flip (List.foldrM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y)

Tactic:
funext
-- Module: Mathlib.Control.Fold
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
inst_1 : LawfulMonad m
f : α → β → m β
x y : FreeMonoid α
x_1 : KleisliCat.mk m β
⊢ flip (List.foldrM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (x * y)) x_1 =
    (flip (List.foldrM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) x) *
        flip (List.foldrM f) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) y))
      x_1

Tactic:
apply List.foldrM_append

Premises used: List.foldrM_append
-- Module: Mathlib.Control.Fold
Goal:
α β γ : Type u
inst : Monoid α
inst_1 : Monoid β
f : α →* β
α_1 : Type u_1
x : α_1
⊢ Eq (α := Const β α_1) ((f : (a : α) → β) (pure x : Const α α_1) : β) (pure x : Const β α_1)

Tactic:
simp only [map_one, pure]

Premises used: Pure.pure, map_one
-- Module: Mathlib.Control.Fold
Goal:
α β γ : Type u
inst : Monoid α
inst_1 : Monoid β
f : α →* β
α_1 β_1 : Type u_1
x : Const.{u, u_1} α (α_1 → β_1)
y : Const α α_1
⊢ Eq (α := Const β β_1) ((f : (a : α) → β) (x <*> y) : β) ((f : (a : α) → β) x <*> (f : (a : α) → β) y : Const β β_1)

Tactic:
simp only [Seq.seq, map_mul]

Premises used: Seq.seq, map_mul
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
f : α → β
xs : List α
⊢ f <$> xs =
    (FreeMonoid.toList : (a : FreeMonoid β) → List β)
      ((FreeMonoid.map f : (a : FreeMonoid α) → FreeMonoid β)
          ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) xs : FreeMonoid α) :
        FreeMonoid β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
f : β → α → β
xs : FreeMonoid α
a : β
⊢ (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (unop ((Foldl.ofFreeMonoid f : (a : FreeMonoid α) → Foldl β) xs)) :
        (a : β) → β)
      a =
    List.foldl f a ((FreeMonoid.toList : (a : FreeMonoid α) → List α) xs)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Fold
Goal:
α β γ : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Monoid α
inst_3 : Monoid β
f : α →* β
g : γ → α
x : t γ
⊢ Eq (α := β) ((f : (a : α) → β) (foldMap g x) : β) (foldMap ((⇑f : (a : α) → β) ∘ g) x : β)

Tactic:
calc
    f (foldMap g x) = f (traverse (Const.mk' ∘ g) x) := rfl
    _ = (mapFold f).app _ (traverse (Const.mk' ∘ g) x) := rfl
    _ = traverse ((mapFold f).app _ ∘ Const.mk' ∘ g) x := naturality (mapFold f) _ _
    _ = foldMap (f ∘ g) x := rfl

Premises used: Trans.trans, Traversable.mapFold, Functor.Const, LawfulTraversable.naturality, rfl
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Monoid β
f : FreeMonoid α →* β
x : t α
⊢ Eq (α := β) ((f : (a : FreeMonoid α) → β) (foldMap FreeMonoid.of x) : β)
    (foldMap ((⇑f : (a : FreeMonoid α) → β) ∘ FreeMonoid.of) x : β)

Tactic:
foldMap_hom f _ x

Premises used: Traversable.foldMap_hom
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
f : α → β → α
⊢ (⇑(Foldl.ofFreeMonoid f) : (a : FreeMonoid β) → Foldl α) ∘ FreeMonoid.of = Foldl.mk ∘ flip f

Tactic:
rfl

Premises used: List.foldl, Monoid.Foldl.mk, rfl, MulOpposite.op
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
f : β → α → α
⊢ (⇑(Foldr.ofFreeMonoid f) : (a : FreeMonoid β) → Foldr α) ∘ FreeMonoid.of = Foldr.mk ∘ f

Tactic:
rfl

Premises used: Monoid.Foldr.mk, List.foldr, rfl
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
f : α → β → m α
h :
  ∀ (x : β),
    Eq (α := foldlM m α) (((⇑(foldlM.ofFreeMonoid f) : (a : FreeMonoid β) → foldlM m α) ∘ FreeMonoid.of) x)
      ((foldlM.mk ∘ flip f) x)
⊢ Eq (α := β → foldlM m α) ((⇑(foldlM.ofFreeMonoid f) : (a : FreeMonoid β) → foldlM m α) ∘ FreeMonoid.of)
    (foldlM.mk ∘ flip f)

Tactic:
ext1 x
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
f : α → β → m α
x : β
h : Eq.{u + 1} (α := End (KleisliCat.mk m α)) (fun (a : KleisliCat.mk m α) ↦ f a x) fun (a : α) ↦ f a x
⊢ Eq (α := foldlM m α) (((⇑(foldlM.ofFreeMonoid f) : (a : FreeMonoid β) → foldlM m α) ∘ FreeMonoid.of) x)
    ((foldlM.mk ∘ flip f) x)

Tactic:
simp only [foldlM.ofFreeMonoid, Function.flip_def, MonoidHom.coe_mk, OneHom.coe_mk,
    Function.comp_apply, FreeMonoid.toList_of, List.foldlM_cons, List.foldlM_nil, bind_pure,
    foldlM.mk, op_inj]

Premises used: List.foldlM_cons, List.foldlM_nil, OneHom.coe_mk, FreeMonoid.toList_of, bind_pure, Function.flip_def, MonoidHom.coe_mk, MulOpposite.op_inj, Monoid.foldlM.mk, Monoid.foldlM.ofFreeMonoid, Function.comp_apply
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
f : α → β → m α
x : β
⊢ Eq.{u + 1} (α := End (KleisliCat.mk m α)) (fun (a : KleisliCat.mk m α) ↦ f a x) fun (a : α) ↦ f a x

Tactic:
rfl
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
f : β → α → m α
h :
  ∀ (x : β),
    Eq (α := foldrM m α) (((⇑(foldrM.ofFreeMonoid f) : (a : FreeMonoid β) → foldrM m α) ∘ FreeMonoid.of) x)
      ((foldrM.mk ∘ f) x)
⊢ Eq (α := β → foldrM m α) ((⇑(foldrM.ofFreeMonoid f) : (a : FreeMonoid β) → foldrM m α) ∘ FreeMonoid.of)
    (foldrM.mk ∘ f)

Tactic:
ext
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
f : β → α → m α
x : β
⊢ Eq (α := foldrM m α) (((⇑(foldrM.ofFreeMonoid f) : (a : FreeMonoid β) → foldrM m α) ∘ FreeMonoid.of) x)
    ((foldrM.mk ∘ f) x)

Tactic:
simp [(· ∘ ·), foldrM.ofFreeMonoid, foldrM.mk, Function.flip_def]

Premises used: Monoid.foldrM.mk, Function.comp, Function.flip_def, Monoid.foldrM.ofFreeMonoid
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
⊢ Eq (α := List α) ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α)
    ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs).reverse.reverse : List α)

Tactic:
simp only [FreeMonoid.reverse_reverse]

Premises used: FreeMonoid.reverse_reverse
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
⊢ Eq (α := List α)
    ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs).reverse.reverse : List α)
    (List.reverse
        (List.foldr cons []
          (List.reverse ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs)))) :
      List α)

Tactic:
simp