awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
m : Type u → Type u
inst : Monad m
α β : Type u
inst_1 : LawfulMonad m
f : α → β → m β
x y : FreeMonoid α
⊢ 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)
have 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
Tactic: funext
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
f : α → β → m α
⊢ Eq (α := β → foldlM m α) ((⇑(foldlM.ofFreeMonoid f) : (a : FreeMonoid β) → foldlM m α) ∘ FreeMonoid.of)
    (foldlM.mk ∘ flip f)
have h : ∀ (x : β),
  Eq (α := foldlM m α) (((⇑(foldlM.ofFreeMonoid f) : (a : FreeMonoid β) → foldlM m α) ∘ FreeMonoid.of) x)
    ((foldlM.mk ∘ flip f) x)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
f : α → β → m α
x : β
⊢ Eq (α := foldlM m α) (((⇑(foldlM.ofFreeMonoid f) : (a : FreeMonoid β) → foldlM m α) ∘ FreeMonoid.of) x)
    ((foldlM.mk ∘ flip f) x)
have h : Eq.{u + 1} (α := End (KleisliCat.mk m α)) (fun (a : KleisliCat.mk m α) ↦ f a x) fun (a : α) ↦ f a 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]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
f : β → α → m α
⊢ Eq (α := β → foldrM m α) ((⇑(foldrM.ofFreeMonoid f) : (a : FreeMonoid β) → foldrM m α) ∘ FreeMonoid.of)
    (foldrM.mk ∘ f)
have h : ∀ (x : β),
  Eq (α := foldrM m α) (((⇑(foldrM.ofFreeMonoid f) : (a : FreeMonoid β) → foldrM m α) ∘ FreeMonoid.of) x)
    ((foldrM.mk ∘ f) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
⊢ List.reverse
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (unop ((Foldl.ofFreeMonoid (flip cons) : (a : FreeMonoid α) → Foldl (List α)) (foldMap FreeMonoid.of xs))) :
          (a : List α) → List α)
        []) =
    toList xs
have rw : List.reverse
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (unop
            (foldMap ((⇑(Foldl.ofFreeMonoid (flip cons)) : (a : FreeMonoid α) → Foldl (List α)) ∘ FreeMonoid.of) xs)) :
        (a : List α) → List α)
      []) =
  toList xs
Tactic: rw [foldMap_hom_free (Foldl.ofFreeMonoid (flip <| @cons α))]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = List.foldl f x (toList xs)
have rw : foldl f x xs =
  (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (unop
          ((Foldl.ofFreeMonoid f : (a : FreeMonoid β) → Foldl α)
            ((FreeMonoid.ofList : (a : List β) → FreeMonoid β) (toList xs) : FreeMonoid β))) :
      (a : α) → α)
    x
Tactic: rw [← FreeMonoid.toList_ofList (toList xs), ← foldl.unop_ofFreeMonoid]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = List.foldr f x (toList xs)
have change : foldr f x xs =
  (TypeCat.Hom.hom
        ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
          ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) (toList xs) : FreeMonoid α)) :
      (a : β) → β)
    x
Tactic: change _ = (Foldr.ofFreeMonoid _ (FreeMonoid.ofList <| toList xs)).hom _
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) (toList xs) : FreeMonoid α)) :
        (a : β) → β)
      x
have rw : foldr f x xs =
  (TypeCat.Hom.hom
        ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
          ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
              ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
            FreeMonoid α)) :
      (a : β) → β)
    x
Tactic: rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free,
    foldr.ofFreeMonoid_comp_of]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β → β
xs : t α
x : β
rw :
  foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
              FreeMonoid α)) :
        (a : β) → β)
      x
⊢ foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) (toList xs) : FreeMonoid α)) :
        (a : β) → β)
      x
have rw₁ : (foldMap (Foldr.mk ∘ f) xs).get x =
  (TypeCat.Hom.hom
        ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
          ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
              ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
            FreeMonoid α)) :
      (a : β) → β)
    x
Tactic: rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free,
    foldr.ofFreeMonoid_comp_of]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β → β
xs : t α
x : β
rw :
  foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
              FreeMonoid α)) :
        (a : β) → β)
      x
rw₁ :
  (foldMap (Foldr.mk ∘ f) xs).get x =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
              FreeMonoid α)) :
        (a : β) → β)
      x
⊢ foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) (toList xs) : FreeMonoid α)) :
        (a : β) → β)
      x
have rw₂ : Eq (α := β) ((ConcreteCategory.hom (FC := TypeCat.Fun) (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
  ((TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
              FreeMonoid α)) :
        (a : β) → β)
      x :
    β)
Tactic: rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free,
    foldr.ofFreeMonoid_comp_of]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β → β
xs : t α
x : β
rw :
  foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
              FreeMonoid α)) :
        (a : β) → β)
      x
rw₁ :
  (foldMap (Foldr.mk ∘ f) xs).get x =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
              FreeMonoid α)) :
        (a : β) → β)
      x
rw₂ :
  Eq (α := β) ((ConcreteCategory.hom (FC := TypeCat.Fun) (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
    ((TypeCat.Hom.hom
            ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
              ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                  ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
                FreeMonoid α)) :
          (a : β) → β)
        x :
      β)
⊢ foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) (toList xs) : FreeMonoid α)) :
        (a : β) → β)
      x
have rw₃ : Eq (α := β) ((ConcreteCategory.hom (FC := TypeCat.Fun) (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
  ((TypeCat.Hom.hom ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β) (foldMap FreeMonoid.of xs)) : (a : β) → β)
      x :
    β)
Tactic: rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free,
    foldr.ofFreeMonoid_comp_of]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β → β
xs : t α
x : β
rw :
  foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
              FreeMonoid α)) :
        (a : β) → β)
      x
rw₁ :
  (foldMap (Foldr.mk ∘ f) xs).get x =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
              FreeMonoid α)) :
        (a : β) → β)
      x
rw₂ :
  Eq (α := β) ((ConcreteCategory.hom (FC := TypeCat.Fun) (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
    ((TypeCat.Hom.hom
            ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
              ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                  ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
                FreeMonoid α)) :
          (a : β) → β)
        x :
      β)
rw₃ :
  Eq (α := β) ((ConcreteCategory.hom (FC := TypeCat.Fun) (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
    ((TypeCat.Hom.hom ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β) (foldMap FreeMonoid.of xs)) : (a : β) → β)
        x :
      β)
⊢ foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) (toList xs) : FreeMonoid α)) :
        (a : β) → β)
      x
have rw₄ : Eq (α := β) ((ConcreteCategory.hom (FC := TypeCat.Fun) (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
  ((TypeCat.Hom.hom (foldMap ((⇑(Foldr.ofFreeMonoid f) : (a : FreeMonoid α) → Foldr β) ∘ FreeMonoid.of) xs) :
        (a : β) → β)
      x :
    β)
Tactic: rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free,
    foldr.ofFreeMonoid_comp_of]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β → β
xs : t α
x : β
rw :
  foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
              FreeMonoid α)) :
        (a : β) → β)
      x
rw₁ :
  (foldMap (Foldr.mk ∘ f) xs).get x =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
              FreeMonoid α)) :
        (a : β) → β)
      x
rw₂ :
  Eq (α := β) ((ConcreteCategory.hom (FC := TypeCat.Fun) (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
    ((TypeCat.Hom.hom
            ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
              ((FreeMonoid.ofList : (a : List α) → FreeMonoid α)
                  ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs) : List α) :
                FreeMonoid α)) :
          (a : β) → β)
        x :
      β)
rw₃ :
  Eq (α := β) ((ConcreteCategory.hom (FC := TypeCat.Fun) (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
    ((TypeCat.Hom.hom ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β) (foldMap FreeMonoid.of xs)) : (a : β) → β)
        x :
      β)
rw₄ :
  Eq (α := β) ((ConcreteCategory.hom (FC := TypeCat.Fun) (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
    ((TypeCat.Hom.hom (foldMap ((⇑(Foldr.ofFreeMonoid f) : (a : FreeMonoid α) → Foldr β) ∘ FreeMonoid.of) xs) :
          (a : β) → β)
        x :
      β)
⊢ foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) (toList xs) : FreeMonoid α)) :
        (a : β) → β)
      x
have rw₅ : Eq (α := β) ((ConcreteCategory.hom (FC := TypeCat.Fun) (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
  ((TypeCat.Hom.hom (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
Tactic: rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free,
    foldr.ofFreeMonoid_comp_of]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
xs : List α
⊢ toList xs = xs
have simp : (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs
Tactic: simp only [toList_spec, foldMap, traverse]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
head : α
tail : List α
ih : (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) tail) = tail
| head :: tail
have rw : head :: (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) tail)
Tactic: rw [← ih]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
head : α
tail : List α
ih : (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) tail) = tail
⊢ (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) (head :: tail)) =
    head :: tail
have cons : (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) (head :: tail)) =
  head :: (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) tail)
Tactic: conv_rhs => rw [← ih]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
xs : List α
⊢ (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs
have nil : Eq.{u + 1} (α := List α)
  ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) []) : List α)
  ([] : List α)
Tactic: induction xs with
  | nil => rfl
  | cons _ _ ih => (conv_rhs => rw [← ih]); rfl
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
xs : List α
nil :
  Eq.{u + 1} (α := List α)
    ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) []) : List α)
    ([] : List α)
⊢ (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs
have cons : ∀ (head : α) (tail : List α)
  (ih : (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) tail) = tail),
  (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) (head :: tail)) =
    head :: tail
Tactic: induction xs with
  | nil => rfl
  | cons _ _ ih => (conv_rhs => rw [← ih]); rfl
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
⊢ down.{u, 0} (foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } xs) = (toList xs).length
have rw : down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } (toList xs)) =
  (toList xs).length
Tactic: rw [foldl_toList]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
⊢ down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } (toList xs)) =
    (toList xs).length
have generalize : ∀ (ys : List α),
  down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } ys) = ys.length
Tactic: generalize toList xs = ys
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
ys : List α
⊢ down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } ys) = ys.length
have rw : down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } ys) = ys.length + 0
Tactic: rw [← Nat.add_zero ys.length]
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
ys : List α
⊢ down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } ys) = ys.length + 0
have generalize : ∀ (n : ℕ),
  down.{u, 0}
      (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 : ULift.{u, 0} ℕ })
        { down := n : ULift.{u, 0} ℕ } ys) =
    ys.length + n
Tactic: generalize 0 = n
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
ys : List α
n : ℕ
⊢ down.{u, 0}
      (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 : ULift.{u, 0} ℕ })
        { down := n : ULift.{u, 0} ℕ } ys) =
    ys.length + n
have nil : ∀ (n : ℕ),
  down.{u, 0}
      (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 : ULift.{u, 0} ℕ })
        { down := n : ULift.{u, 0} ℕ } []) =
    List.length.{u} (α := α) [] + n
Tactic: induction ys generalizing n with
  | nil => simp
  | cons _ _ ih => simp +arith [ih]
Cleared hypotheses: ys, n
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
ys : List α
n : ℕ
nil :
  ∀ (n : ℕ),
    down.{u, 0}
        (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 : ULift.{u, 0} ℕ })
          { down := n : ULift.{u, 0} ℕ } []) =
      List.length.{u} (α := α) [] + n
⊢ down.{u, 0}
      (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 : ULift.{u, 0} ℕ })
        { down := n : ULift.{u, 0} ℕ } ys) =
    ys.length + n
have cons : ∀ (head : α) (tail : List α)
  (ih :
    ∀ (n : ℕ),
      down.{u, 0}
          (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 : ULift.{u, 0} ℕ })
            { down := n : ULift.{u, 0} ℕ } tail) =
        tail.length + n)
  (n : ℕ),
  down.{u, 0}
      (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 : ULift.{u, 0} ℕ })
        { down := n : ULift.{u, 0} ℕ } (head :: tail)) =
    (head :: tail).length + n
Tactic: induction ys generalizing n with
  | nil => simp
  | cons _ _ ih => simp +arith [ih]
Cleared hypotheses: ys, n
-- Lean 4 proof step from Mathlib.Control.Fold (goal)
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
m : Type u → Type u
inst_2 : Monad m
inst_3 : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = List.foldrM f x (toList xs)
have change : foldrm f x xs =
  (foldrM.ofFreeMonoid f : (a : FreeMonoid α) → foldrM m β)
    ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) (toList xs) : FreeMonoid α) x
Tactic: change _ = foldrM.ofFreeMonoid f (FreeMonoid.ofList <| toList xs) x
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
Goal:
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : comp (α := β) (β := α) (γ := β) f g = TypeVec.id (α := β)
h₁ : ∀ (u : F α), P u ↔ q (map (F := F) (α := α) (β := β) f u)
⊢ (∃ (u : F α), P u) ↔ ∃ (u : F β), q u
have mp : (∃ (u : F α), P u) → ∃ (u : F β), q u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
Goal:
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : comp (α := β) (β := α) (γ := β) f g = TypeVec.id (α := β)
h₁ : ∀ (u : F α), P u ↔ q (map (F := F) (α := α) (β := β) f u)
mp : (∃ (u : F α), P u) → ∃ (u : F β), q u
⊢ (∃ (u : F α), P u) ↔ ∃ (u : F β), q u
have mpr : (∃ (u : F β), q u) → ∃ (u : F α), P u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
Goal:
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : comp (α := β) (β := α) (γ := β) f g = TypeVec.id (α := β)
h₁ : ∀ (u : F α), P u ↔ q (map (F := F) (α := α) (β := β) f u)
u : F α
h₂ : P u
⊢ ∃ (u : F β), q u
have mp : q (map (F := F) (α := α) (β := β) f u)
Tactic: refine ⟨f <$$> u, ?_⟩
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
Goal:
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : comp (α := β) (β := α) (γ := β) f g = TypeVec.id (α := β)
h₁ : ∀ (u : F α), P u ↔ q (map (F := F) (α := α) (β := β) f u)
u : F β
h₂ : q u
⊢ ∃ (u : F α), P u
have mpr : P (map (F := F) (α := β) (β := α) g u)
Tactic: refine ⟨g <$$> u, ?_⟩
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
Goal:
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : comp (α := β) (β := α) (γ := β) f g = TypeVec.id (α := β)
h₁ : ∀ (u : F α), P u ↔ q (map (F := F) (α := α) (β := β) f u)
u : F β
h₂ : q u
⊢ P (map (F := F) (α := β) (β := α) g u)
have mpr : q (map (F := F) (α := α) (β := β) f (map (F := F) (α := β) (β := α) g u))
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.Control.Functor.Multivariate (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α_1 : TypeVec.{u} n
β : Type u
pp : β → Prop
x_1 : ℕ
α : TypeVec.{u} x_1
i : Fin2 x_1
x : (fun (i : Fin2 (x_1 + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast pp p_1 }) i.fs
⊢ True = ofRepeat (α.PredLast' pp i.fs (↑x : (α ::: β) i.fs))
have erw : True = True
Tactic: erw [const_iff_true]