awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
⊢ Eq.{u + 1} (α := List α)
    (List.reverse
      (List.foldr cons []
        (List.reverse ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (foldMap FreeMonoid.of xs)))))
    (List.reverse
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (unop ((Foldl.ofFreeMonoid (flip cons) : (a : FreeMonoid α) → Foldl (List α)) (foldMap FreeMonoid.of xs))) :
          (a : List α) → List α)
        []))

Tactic:
simp [Function.flip_def, List.foldr_reverse, Foldl.ofFreeMonoid, unop_op]

Premises used: List.foldr_reverse, Monoid.Foldl.ofFreeMonoid, Function.flip_def, MulOpposite.unop_op
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
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
⊢ 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

Tactic:
rw [foldMap_hom_free (Foldl.ofFreeMonoid (flip <| @cons α))]

Premises used: Traversable.foldMap_hom_free, Monoid.Foldl.ofFreeMonoid, flip, List.cons
-- Module: Mathlib.Control.Fold
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
              (foldMap ((⇑(Foldl.ofFreeMonoid (flip cons)) : (a : FreeMonoid α) → Foldl (List α)) ∘ FreeMonoid.of)
                xs)) :
          (a : List α) → List α)
        []) =
    toList xs

Tactic:
simp only [toList, foldl, Foldl.get, foldl.ofFreeMonoid_comp_of,
              Function.comp_apply]

Premises used: Monoid.Foldl.get, Traversable.foldl.ofFreeMonoid_comp_of, Function.comp_apply, Traversable.foldl, Traversable.toList
-- Module: Mathlib.Control.Fold
Goal:
α β γ : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
inst_2 : Monoid γ
f : α → β
g : β → γ
xs : t α
⊢ foldMap g (f <$> xs) = foldMap (g ∘ f) xs

Tactic:
simp only [foldMap, traverse_map, Function.comp_def]

Premises used: Traversable.foldMap, Traversable.traverse_map, Function.comp_def
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β → α
xs : t β
x : α
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
⊢ foldl f x xs = List.foldl f x (toList xs)

Tactic:
rw [← FreeMonoid.toList_ofList (toList xs), ← foldl.unop_ofFreeMonoid]

Premises used: FreeMonoid.toList_ofList, Traversable.foldl.unop_ofFreeMonoid, Traversable.toList
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ 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:
simp only [foldl, toList_spec, foldMap_hom_free, foldl.ofFreeMonoid_comp_of, Foldl.get,
    FreeMonoid.ofList_toList]

Premises used: Traversable.foldMap_hom_free, FreeMonoid.ofList_toList, Monoid.Foldl.get, Traversable.foldl.ofFreeMonoid_comp_of, Traversable.foldl, Traversable.toList_spec
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β → β
xs : t α
x : β
change :
  foldr f x xs =
    (TypeCat.Hom.hom
          ((Foldr.ofFreeMonoid f : (a : FreeMonoid α) → Foldr β)
            ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) (toList xs) : FreeMonoid α)) :
        (a : β) → β)
      x
⊢ foldr f x xs = List.foldr f x (toList xs)

Tactic:
change _ = (Foldr.ofFreeMonoid _ (FreeMonoid.ofList <| toList xs)).hom _

Premises used: FreeMonoid.ofList, TypeCat.Hom.hom, Traversable.toList, DFunLike.coe, Monoid.Foldr.ofFreeMonoid
-- Module: Mathlib.Control.Fold
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 :
      β)
rw₅ rw₆ :
  Eq (α := β) ((ConcreteCategory.hom (FC := TypeCat.Fun) (foldMap (Foldr.mk ∘ f) xs) : (a : β) → β) x : β)
    ((TypeCat.Hom.hom (foldMap (Foldr.mk ∘ f) 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

Tactic:
rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free,
    foldr.ofFreeMonoid_comp_of]

Premises used: Traversable.foldMap_hom_free, Traversable.foldr, FreeMonoid.ofList_toList, Traversable.foldr.ofFreeMonoid_comp_of, Traversable.toList_spec, Monoid.Foldr.get
-- Module: Mathlib.Control.Fold
Goal:
α β : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
f : α → β
xs : t α
⊢ toList (f <$> xs) = f <$> toList xs

Tactic:
simp only [toList_spec, Free.map_eq_map, foldMap_hom, foldMap_map, FreeMonoid.ofList_toList,
    FreeMonoid.map_of, Function.comp_def]

Premises used: FreeMonoid.ofList_toList, Traversable.foldMap_map, Function.comp_def, Traversable.Free.map_eq_map, Traversable.foldMap_hom, FreeMonoid.map_of, Traversable.toList_spec
-- Module: Mathlib.Control.Fold
Goal:
α β γ : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
g : β → γ
f : α → γ → α
a : α
l : t β
⊢ foldl f a (g <$> l) = foldl (fun (x : α) (y : β) ↦ f x (g y)) a l

Tactic:
simp only [foldl, foldMap_map, Function.comp_def, Function.flip_def]

Premises used: Function.flip_def, Traversable.foldMap_map, Function.comp_def, Traversable.foldl
-- Module: Mathlib.Control.Fold
Goal:
α β γ : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
g : β → γ
f : γ → α → α
a : α
l : t β
⊢ foldr f a (g <$> l) = foldr (f ∘ g) a l

Tactic:
simp only [foldr, foldMap_map, Function.comp_def]

Premises used: Traversable.foldr, Traversable.foldMap_map, Function.comp_def
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
xs : List α
simp : (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs
⊢ toList xs = xs

Tactic:
simp only [toList_spec, foldMap, traverse]

Premises used: Traversable.foldMap, Traversable.traverse, Traversable.toList_spec
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List α)
    ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) []) : List α)
    ([] : List α)

Tactic:
rfl
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
head : α
tail : List α
ih : (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) tail) = tail
rw : head :: (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) tail)
| head :: tail

Tactic:
rw [← ih]
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
head : α
tail : List α
ih : (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) tail) = tail
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)
⊢ (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) (head :: tail)) =
    head :: tail

Tactic:
conv_rhs => rw [← ih]
-- Module: Mathlib.Control.Fold
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 :: (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) tail)

Tactic:
rfl
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
xs : List α
nil :
  Eq.{u + 1} (α := List α)
    ((FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) []) : List α)
    ([] : List α)
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
⊢ (FreeMonoid.toList : (a : FreeMonoid α) → List α) (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs

Tactic:
induction xs with
  | nil => rfl
  | cons _ _ ih => (conv_rhs => rw [← ih]); rfl

Premises used: List.cons
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
rw :
  down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } (toList xs)) =
    (toList xs).length
⊢ down.{u, 0} (foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } xs) = (toList xs).length

Tactic:
rw [foldl_toList]

Premises used: Traversable.foldl_toList
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
generalize :
  ∀ (ys : List α),
    down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } ys) = ys.length
⊢ down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } (toList xs)) =
    (toList xs).length

Tactic:
generalize toList xs = ys

Premises used: Traversable.toList
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
ys : List α
rw :
  down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } ys) = ys.length + 0
⊢ down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } ys) = ys.length

Tactic:
rw [← Nat.add_zero ys.length]

Premises used: Nat.add_zero, List.length
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
ys : List α
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
⊢ down.{u, 0} (List.foldl (fun (l : ULift.{u, 0} ℕ) (x : α) ↦ { down := l.down + 1 }) { down := 0 } ys) = ys.length + 0

Tactic:
generalize 0 = n
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
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:
simp
-- Module: Mathlib.Control.Fold
Goal:
α : Type u
t : Type u → Type u
inst : Traversable t
inst_1 : LawfulTraversable t
xs : t α
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:
simp +arith [ih]
-- Module: Mathlib.Control.Fold
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
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
⊢ 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:
induction ys generalizing n with
  | nil => simp
  | cons _ _ ih => simp +arith [ih]

Premises used: List.cons
-- Module: Mathlib.Control.Fold
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 β
⊢ foldlm f x xs =
    unop
      ((foldlM.ofFreeMonoid f : (a : FreeMonoid β) → foldlM m α)
        ((FreeMonoid.ofList : (a : List β) → FreeMonoid β) (toList xs) : FreeMonoid β))
      x

Tactic:
simp only [foldlm, toList_spec, foldMap_hom_free (foldlM.ofFreeMonoid f),
        foldlm.ofFreeMonoid_comp_of, foldlM.get, FreeMonoid.ofList_toList]

Premises used: Traversable.foldMap_hom_free, Traversable.foldlm.ofFreeMonoid_comp_of, Monoid.foldlM.get, Traversable.foldlm, FreeMonoid.ofList_toList, Monoid.foldlM.ofFreeMonoid, Traversable.toList_spec
-- Module: Mathlib.Control.Fold
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 β
⊢ unop
      ((foldlM.ofFreeMonoid f : (a : FreeMonoid β) → foldlM m α)
        ((FreeMonoid.ofList : (a : List β) → FreeMonoid β) (toList xs) : FreeMonoid β))
      x =
    List.foldlM f x (toList xs)

Tactic:
simp [foldlM.ofFreeMonoid, unop_op, flip]

Premises used: flip, Monoid.foldlM.ofFreeMonoid, MulOpposite.unop_op
-- Module: Mathlib.Control.Fold
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 α
change :
  foldrm f x xs =
    (foldrM.ofFreeMonoid f : (a : FreeMonoid α) → foldrM m β)
      ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) (toList xs) : FreeMonoid α) x
⊢ foldrm f x xs = List.foldrM f x (toList xs)

Tactic:
change _ = foldrM.ofFreeMonoid f (FreeMonoid.ofList <| toList xs) x

Premises used: FreeMonoid.ofList, Monoid.foldrM.ofFreeMonoid, Traversable.toList, DFunLike.coe
-- Module: Mathlib.Control.Fold
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 =
    (foldrM.ofFreeMonoid f : (a : FreeMonoid α) → foldrM m β)
      ((FreeMonoid.ofList : (a : List α) → FreeMonoid α) (toList xs) : FreeMonoid α) x

Tactic:
simp only [foldrm, toList_spec, foldMap_hom_free (foldrM.ofFreeMonoid f),
    foldrm.ofFreeMonoid_comp_of, foldrM.get, FreeMonoid.ofList_toList]

Premises used: Traversable.foldMap_hom_free, Traversable.foldrm, Monoid.foldrM.get, FreeMonoid.ofList_toList, Traversable.foldrm.ofFreeMonoid_comp_of, Monoid.foldrM.ofFreeMonoid, Traversable.toList_spec
-- Module: Mathlib.Control.Fold
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
g : β → γ
f : α → γ → m α
a : α
l : t β
⊢ foldlm f a (g <$> l) = foldlm (fun (x : α) (y : β) ↦ f x (g y)) a l

Tactic:
simp only [foldlm, foldMap_map, Function.comp_def, Function.flip_def]

Premises used: Traversable.foldlm, Function.flip_def, Traversable.foldMap_map, Function.comp_def
-- Module: Mathlib.Control.Fold
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
g : β → γ
f : γ → α → m α
a : α
l : t β
⊢ foldrm f a (g <$> l) = foldrm (f ∘ g) a l

Tactic:
simp only [foldrm, foldMap_map, Function.comp_def]

Premises used: Traversable.foldrm, Traversable.foldMap_map, Function.comp_def
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} n → Type v
inst : MvFunctor F
α : TypeVec.{u} n
x : F α
P : ⦃i : Fin2 n⦄ → α i → Prop
h : LiftP (F := F) (α := α) P x
i : Fin2 n
⊢ ∀ y ∈ supp (F := F) (α := α) x i, P y

Tactic:
fun _y hy => hy h
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
x : F α
⊢ map (F := F) (α := α) (β := α) (TypeVec.id (α := α)) x = x

Tactic:
LawfulMvFunctor.id_map x

Premises used: LawfulMvFunctor.id_map
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
x : F α
⊢ map (F := F) (α := α) (β := α) (fun (_i : Fin2 n) (a : α _i) ↦ a) x = x

Tactic:
id_map x

Premises used: MvFunctor.id_map, TypeVec.id
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
α β γ : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
g : α ⟹ β
h : β ⟹ γ
x : F α
⊢ map (F := F) (α := β) (β := γ) h (map (F := F) (α := α) (β := β) g x) =
    map (F := F) (α := α) (β := γ) (comp (α := α) (β := β) (γ := γ) h g) x

Tactic:
Eq.symm <| comp_map _ _ _

Premises used: LawfulMvFunctor.comp_map, Eq.symm
-- Module: Mathlib.Control.Functor.Multivariate
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
mpr : (∃ (u : F β), q u) → ∃ (u : F α), P u
⊢ (∃ (u : F α), P u) ↔ ∃ (u : F β), q u

Tactic:
constructor
-- Module: Mathlib.Control.Functor.Multivariate
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

Tactic:
⟨f <$$> u, ?_⟩

Premises used: Exists.intro, MvFunctor.map
-- Module: Mathlib.Control.Functor.Multivariate
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
mp : q (map (F := F) (α := α) (β := β) f u)
⊢ ∃ (u : F β), q u

Tactic:
refine ⟨f <$$> u, ?_⟩
-- Module: Mathlib.Control.Functor.Multivariate
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
⊢ q (map (F := F) (α := α) (β := β) f u)

Tactic:
apply (h₁ u).mp h₂

Premises used: Iff.mp
-- Module: Mathlib.Control.Functor.Multivariate
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

Tactic:
⟨g <$$> u, ?_⟩

Premises used: Exists.intro, MvFunctor.map
-- Module: Mathlib.Control.Functor.Multivariate
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
mpr : P (map (F := F) (α := β) (β := α) g u)
⊢ ∃ (u : F α), P u

Tactic:
refine ⟨g <$$> u, ?_⟩
-- Module: Mathlib.Control.Functor.Multivariate
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
mpr : q (map (F := F) (α := α) (β := β) f (map (F := F) (α := β) (β := α) g u))
⊢ P (map (F := F) (α := β) (β := α) g u)

Tactic:
rw [h₁]
-- Module: Mathlib.Control.Functor.Multivariate
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
⊢ q (map (F := F) (α := α) (β := β) f (map (F := F) (α := β) (β := α) g u))

Tactic:
simp only [MvFunctor.map_map, h₀, LawfulMvFunctor.id_map, h₂]

Premises used: LawfulMvFunctor.id_map, MvFunctor.map_map
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst : MvFunctor F
P : α ⟹ TypeVec.repeat n Prop
inst_1 : LawfulMvFunctor F
x : F α
⊢ ∀ (u : F fun (i : Fin2 n) ↦ Subtype (α := α i) ((fun (i : Fin2 n) (x : α i) ↦ ofRepeat (P i x)) i)),
    map (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) ((fun (i : Fin2 n) (x : α i) ↦ ofRepeat (P i x)) i)) (β :=
          α) (fun (i : Fin2 n) ↦ Subtype.val (p := (fun (i : Fin2 n) (x : α i) ↦ ofRepeat (P i x)) i)) u =
        x ↔
      map (F := F) (α := Subtype_ (α := α) P) (β := α) (subtypeVal (α := α) P)
          (map (F := F) (α := fun (i : Fin2 n) ↦ Subtype (α := α i) ((fun (i : Fin2 n) (x : α i) ↦ ofRepeat (P i x)) i))
            (β := Subtype_ (α := α) P) (toSubtype (α := α) P) u) =
        x

Tactic:
simp [MvFunctor.map_map]

Premises used: MvFunctor.map_map