awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (Discrete J) (Type u_2)
cond :
  ∀ {i j k : Discrete J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fi) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj i)) → (fun (X : Type u_2) ↦ X) (F.obj k))
            xi :
          (fun (X : Type u_2) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fj) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj j)) → (fun (X : Type u_2) ↦ X) (F.obj k))
            xj :
          (fun (X : Type u_2) ↦ X) (F.obj k)) →
      ∃ (l : Discrete J) (fli : l ⟶ i) (flj : l ⟶ j) (x : F.obj l),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj i))
              x =
            xi ∧
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj j))
              x =
            xj
⊢ F.IsLocallyDirected

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (Discrete J) (Type u_2)
i : J
x : F.obj { as := i }
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 { as := i : Discrete J })) :
          (a : F.obj { as := i }) → F.obj { as := i })
        x =
      x ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 { as := i : Discrete J })) :
          (a : F.obj { as := i }) → F.obj { as := i })
        x =
      x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (Discrete J) (Type u_2)
i : J
⊢ ∀ (xi xj : F.obj { as := i }),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj { as := i }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.map
                  { down := { down := ⋯ : PLift ({ as := i : Discrete J }.as = { as := i : Discrete J }.as) } :
                    ULift.{u_1, 0} (PLift ({ as := i : Discrete J }.as = { as := i : Discrete J }.as)) }) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj { as := i })) → (fun (X : Type u_2) ↦ X) (F.obj { as := i }))
            xi :
          (fun (X : Type u_2) ↦ X) (F.obj { as := i }))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.map
                  { down := { down := ⋯ : PLift ({ as := i : Discrete J }.as = { as := i : Discrete J }.as) } :
                    ULift.{u_1, 0} (PLift ({ as := i : Discrete J }.as = { as := i : Discrete J }.as)) }) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj { as := i })) → (fun (X : Type u_2) ↦ X) (F.obj { as := i }))
            xj :
          (fun (X : Type u_2) ↦ X) (F.obj { as := i })) →
      ∃ (l : Discrete J) (fli : l ⟶ { as := i }) (flj : l ⟶ { as := i }) (x : F.obj l),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj { as := i }))
              x =
            xi ∧
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj { as := i }))
              x =
            xj

Tactic:
simpa using fun x ↦ ⟨i, 𝟙 _, 𝟙 _, x, by simp⟩
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
cond :
  ∀ {i j k : WidePushoutShape J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fi) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj i)) → (fun (X : Type u_2) ↦ X) (F.obj k))
            xi :
          (fun (X : Type u_2) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fj) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj j)) → (fun (X : Type u_2) ↦ X) (F.obj k))
            xj :
          (fun (X : Type u_2) ↦ X) (F.obj k)) →
      ∃ (l : WidePushoutShape J) (fli : l ⟶ i) (flj : l ⟶ j) (x : F.obj l),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj i))
              x =
            xi ∧
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj j))
              x =
            xj
⊢ F.IsLocallyDirected

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : WidePushoutShape J
x : F.obj i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 i)) : (a : F.obj i) → F.obj i) x = x ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 i)) : (a : F.obj i) → F.obj i) x = x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : WidePushoutShape J
⊢ ∀ (xi xj : F.obj i),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.id i)) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj i)) → (fun (X : Type u_2) ↦ X) (F.obj i))
            xi :
          (fun (X : Type u_2) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.id i)) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj i)) → (fun (X : Type u_2) ↦ X) (F.obj i))
            xj :
          (fun (X : Type u_2) ↦ X) (F.obj i)) →
      ∃ (l : WidePushoutShape J) (fli : l ⟶ i) (flj : l ⟶ i) (x : F.obj l),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj i))
              x =
            xi ∧
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj i))
              x =
            xj

Tactic:
simpa using fun x ↦ ⟨_, 𝟙 _, 𝟙 _, x, by simp⟩
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
j : J
cond :
  ∀ (b : F.obj none),
    ∃ (l : WidePushoutShape J) (fli : l ⟶ some j) (flj : l ⟶ none) (x : F.obj l),
      Eq (α := F.obj (some j))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) : (a : F.obj l) → F.obj (some j)) x : F.obj (some j))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init j)) :
                (a : F.obj none) → F.obj (some j))
              b :
            F.obj (some j)) ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) : (a : F.obj l) → F.obj none) x = b
⊢ ∀ (xi : F.obj (some j)) (xj : F.obj none),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (some j)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.id (some j))) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (some j))) → (fun (X : Type u_2) ↦ X) (F.obj (some j)))
            xi :
          (fun (X : Type u_2) ↦ X) (F.obj (some j)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init j)) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj none)) → (fun (X : Type u_2) ↦ X) (F.obj (some j)))
            xj :
          (fun (X : Type u_2) ↦ X) (F.obj (some j))) →
      ∃ (l : WidePushoutShape J) (fli : l ⟶ some j) (flj : l ⟶ none) (x : F.obj l),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj (some j)))
              x =
            xi ∧
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj none))
              x =
            xj

Tactic:
simp only [WidePushoutShape.hom_id, Functor.map_id, id_apply, forall_comm, forall_eq]

Premises used: forall_eq, forall_comm, CategoryTheory.Limits.WidePushoutShape.hom_id, CategoryTheory.id_apply, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
j : J
x : F.obj none
⊢ Eq (α := F.obj (some j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init j)) :
            (a : F.obj none) → F.obj (some j))
          x :
        F.obj (some j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init j)) :
            (a : F.obj none) → F.obj (some j))
          x :
        F.obj (some j)) ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 none)) : (a : F.obj none) → F.obj none) x = x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
j : J
⊢ ∀ (b : F.obj none),
    ∃ (l : WidePushoutShape J) (fli : l ⟶ some j) (flj : l ⟶ none) (x : F.obj l),
      Eq (α := F.obj (some j))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) : (a : F.obj l) → F.obj (some j)) x : F.obj (some j))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init j)) :
                (a : F.obj none) → F.obj (some j))
              b :
            F.obj (some j)) ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) : (a : F.obj l) → F.obj none) x = b

Tactic:
exact fun x ↦ ⟨_, .init _, 𝟙 _, x, by simp⟩
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
cond :
  ∀ (xi : F.obj none),
    ∃ (l : WidePushoutShape J) (fli : l ⟶ none) (flj : l ⟶ some i) (x : F.obj l),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) : (a : F.obj l) → F.obj none) x = xi ∧
        Eq (α := F.obj (some i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) : (a : F.obj l) → F.obj (some i)) x : F.obj (some i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init i)) :
                (a : F.obj none) → F.obj (some i))
              xi :
            F.obj (some i))
⊢ ∀ (xi : F.obj none) (xj : F.obj (some i)),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (some i)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init i)) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj none)) → (fun (X : Type u_2) ↦ X) (F.obj (some i)))
            xi :
          (fun (X : Type u_2) ↦ X) (F.obj (some i)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.id (some i))) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (some i))) → (fun (X : Type u_2) ↦ X) (F.obj (some i)))
            xj :
          (fun (X : Type u_2) ↦ X) (F.obj (some i))) →
      ∃ (l : WidePushoutShape J) (fli : l ⟶ none) (flj : l ⟶ some i) (x : F.obj l),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj none))
              x =
            xi ∧
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj (some i)))
              x =
            xj

Tactic:
simp only [WidePushoutShape.hom_id, Functor.map_id, id_apply, forall_eq']

Premises used: forall_eq', CategoryTheory.Limits.WidePushoutShape.hom_id, CategoryTheory.id_apply, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
x : F.obj none
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 none)) : (a : F.obj none) → F.obj none) x = x ∧
    Eq (α := F.obj (some i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init i)) :
            (a : F.obj none) → F.obj (some i))
          x :
        F.obj (some i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init i)) :
            (a : F.obj none) → F.obj (some i))
          x :
        F.obj (some i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi : F.obj none),
    ∃ (l : WidePushoutShape J) (fli : l ⟶ none) (flj : l ⟶ some i) (x : F.obj l),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) : (a : F.obj l) → F.obj none) x = xi ∧
        Eq (α := F.obj (some i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) : (a : F.obj l) → F.obj (some i)) x : F.obj (some i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init i)) :
                (a : F.obj none) → F.obj (some i))
              xi :
            F.obj (some i))

Tactic:
exact fun x ↦ ⟨_, 𝟙 _, .init _, x, by simp⟩
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
cond :
  ∀ (xi : F.obj none),
    ∃ (l : WidePushoutShape J) (fli : l ⟶ none) (flj : l ⟶ none) (x : F.obj l),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) : (a : F.obj l) → F.obj none) x = xi ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) : (a : F.obj l) → F.obj none) x = xi
⊢ ∀ (xi xj : F.obj none),
    Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (some i)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init i)) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj none)) → (fun (X : Type u_2) ↦ X) (F.obj (some i)))
            xi :
          (fun (X : Type u_2) ↦ X) (F.obj (some i)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (WidePushoutShape.Hom.init i)) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj none)) → (fun (X : Type u_2) ↦ X) (F.obj (some i)))
            xj :
          (fun (X : Type u_2) ↦ X) (F.obj (some i))) →
      ∃ (l : WidePushoutShape J) (fli : l ⟶ none) (flj : l ⟶ none) (x : F.obj l),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj none))
              x =
            xi ∧
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj l)) → (fun (X : Type u_2) ↦ X) (F.obj none))
              x =
            xj

Tactic:
simp only [((CategoryTheory.mono_iff_injective (F.map (.init i))).mp inferInstance).eq_iff,
      forall_eq']

Premises used: CategoryTheory.mono_iff_injective, Function.Injective.eq_iff, CategoryTheory.Limits.WidePushoutShape.Hom.init, inferInstance, forall_eq', CategoryTheory.Functor.map, Iff.mp
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
x : F.obj none
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 none)) : (a : F.obj none) → F.obj none) x = x ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 none)) : (a : F.obj none) → F.obj none) x = x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.LocallyDirected
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
F : Functor.{u_1, u_2, u_1, u_2 + 1} (WidePushoutShape J) (Type u_2)
inst_1 : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi : F.obj none),
    ∃ (l : WidePushoutShape J) (fli : l ⟶ none) (flj : l ⟶ none) (x : F.obj l),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map fli) : (a : F.obj l) → F.obj none) x = xi ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map flj) : (a : F.obj l) → F.obj none) x = xi

Tactic:
exact fun x ↦ ⟨_, 𝟙 _, 𝟙 _, x, by simp⟩
-- Module: Mathlib.CategoryTheory.MarkovCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MarkovCategory.{v, u} C
X : C
f : X ⟶ tensorUnit.{v, u} C (𝒞 := inst)
rw : f ≫ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) = ε
rw₁ : Eq (α := X ⟶ tensorUnit.{v, u} C (𝒞 := inst)) (f ≫ ε) ε
rw₂ rw₃ : Eq.{v + 1} (α := X ⟶ tensorUnit.{v, u} C (𝒞 := inst)) ε ε
⊢ f = ε

Tactic:
rw [← Category.comp_id f, ← discard_unit, discard_natural]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.CopyDiscardCategory.discard_unit, CategoryTheory.MarkovCategory.discard_natural
-- Module: Mathlib.CategoryTheory.MarkovCategory.Positive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : PositiveCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
⊢ Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y))
    ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MarkovCategory.Positive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : PositiveCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
rw : Deterministic.{v, u} (𝟙 X)
⊢ Deterministic (f ≫ inv f)

Tactic:
rw [IsIso.hom_inv_id]

Premises used: CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.CategoryTheory.MarkovCategory.Positive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : PositiveCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
⊢ Deterministic.{v, u} (𝟙 X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MarkovCategory.Positive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : PositiveCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
rw :
  Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((Δ ≫ (f ≫ inv f ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y))
⊢ Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y)) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y))

Tactic:
rw [copy_comp_natural (h := by rw [IsIso.hom_inv_id]; infer_instance)]

Premises used: CategoryTheory.PositiveCategory.copy_comp_natural
-- Module: Mathlib.CategoryTheory.MarkovCategory.Positive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : PositiveCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
⊢ Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((Δ ≫ (f ≫ inv f ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MarkovCategory.Positive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : PositiveCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
⊢ Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)) (Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MarkovCategory.Positive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : PositiveCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
rw rw₁ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y)) (Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y))
⊢ Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y)) (Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y))

Tactic:
rw [MonoidalCategory.tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom
-- Module: Mathlib.CategoryTheory.MarkovCategory.Positive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : PositiveCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : IsIso f
_ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ) (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y))
_₁ :
  Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y))
    ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y))
_₂ :
  Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y)) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y))
_₃ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)) (Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y))
_₄ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y)) (Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y))
_₅ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y)) (Δ ≫ (f ⊗ₘ f))
⊢ Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ) (Δ ≫ (f ⊗ₘ f))

Tactic:
calc
    _ = f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y) := by
      cat_disch
    _ = (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y) := by
      simp
    _ = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y) := by
      rw [copy_comp_natural (h := by rw [IsIso.hom_inv_id]; infer_instance)]
      simp
    _ = Δ ≫ (𝟙 X ⊗ₘ f) ≫ (f ⊗ₘ 𝟙 Y) := by
      simp
    _ = Δ ≫ ((𝟙 X ≫ f) ⊗ₘ (f ≫ 𝟙 Y)) := by
      rw [MonoidalCategory.tensorHom_comp_tensorHom]
    _ = Δ ≫ (f ⊗ₘ f) := by cat_disch

Premises used: CategoryTheory.ComonObj.comul, CategoryTheory.CategoryStruct.id, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, CategoryTheory.MonoidalCategoryStruct.tensorHom
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : C
dsimp :
  Eq (α := R.obj (L.obj (R.obj (L.obj (R.obj (L.obj X))))) ⟶ R.obj (L.obj X))
    (R.map (L.map (R.map (h.counit.app (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)))
    (R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)))
⊢ (L ⋙ R).map ((whiskerRight (L.whiskerLeft h.counit) R).app X) ≫ (whiskerRight (L.whiskerLeft h.counit) R).app X =
    (whiskerRight (L.whiskerLeft h.counit) R).app ((L ⋙ R).obj X) ≫ (whiskerRight (L.whiskerLeft h.counit) R).app X

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : C
rw :
  Eq (α := R.obj (L.obj (R.obj (L.obj (R.obj (L.obj X))))) ⟶ R.obj (L.obj X))
    (R.map (L.map (R.map (h.counit.app (L.obj X))) ≫ h.counit.app (L.obj X)))
    (R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)))
⊢ Eq (α := R.obj (L.obj (R.obj (L.obj (R.obj (L.obj X))))) ⟶ R.obj (L.obj X))
    (R.map (L.map (R.map (h.counit.app (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)))
    (R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)))

Tactic:
rw [← R.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monad.Adjunction
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
X : C
⊢ Eq (α := R.obj (L.obj (R.obj (L.obj (R.obj (L.obj X))))) ⟶ R.obj (L.obj X))
    (R.map (L.map (R.map (h.counit.app (L.obj X))) ≫ h.counit.app (L.obj X)))
    (R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)))

Tactic:
simp