awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.Sections (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
X : Over.{v₁, u₁} I
A : C
u : Functor.obj (toOver I) A ⟶ X
⊢ homMk
      (Iso.hom (β_ A I) ≫
        uncurry
          (CategoryStruct.comp (Y :=
            pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
              (curryRightUnitorHom I))
            (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) ⋯)
            (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curryRightUnitorHom I))))
      ⋯ =
    u
have h : Hom.left
    (homMk
      (Iso.hom (β_ A I) ≫
        uncurry
          (CategoryStruct.comp (Y :=
            pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
              (curryRightUnitorHom I))
            (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) sorry)
            (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curryRightUnitorHom I))))
      sorry) =
  Hom.left u
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.Sections (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
A' A : C
X : Over.{v₁, u₁} I
g : A' ⟶ A
v : A ⟶ Functor.obj (sections I) X
⊢ Eq (α := Functor.obj (toOver I) A' ⟶ X)
    ((Equiv.symm { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } :
          (a : A' ⟶ (sections I).obj X) → (toOver I).obj A' ⟶ X)
        (g ≫ v) :
      Functor.obj (toOver I) A' ⟶ X)
    (Functor.map (toOver I) g ≫
        (Equiv.symm { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } :
            (a : A ⟶ (sections I).obj X) → (toOver I).obj A ⟶ X)
          v :
      Functor.obj (toOver I) A' ⟶ X)
have dsimp : homMk
    (Iso.hom (β_ A' I) ≫
      uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
    sorry =
  Functor.map (toOver I) g ≫
    homMk
      (Iso.hom (β_ A I) ≫ uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      sorry
Tactic: dsimp [sectionsCurry, sectionsUncurry, curryRightUnitorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.Sections (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
A' A : C
X : Over.{v₁, u₁} I
g : A' ⟶ A
v : A ⟶ Functor.obj (sections I) X
⊢ homMk
      (Iso.hom (β_ A' I) ≫
        uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯ =
    Functor.map (toOver I) g ≫
      homMk
        (Iso.hom (β_ A I) ≫
          uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
        ⋯
have simp : homMk
    (Iso.hom (β_ A' I) ≫
      uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
    sorry =
  homMk (g ▷ I) sorry ≫
    homMk
      (Iso.hom (β_ A I) ≫ uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      sorry
Tactic: simp only [toOver_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.Sections (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
A' A : C
X : Over.{v₁, u₁} I
g : A' ⟶ A
v : A ⟶ Functor.obj (sections I) X
⊢ homMk
      (Iso.hom (β_ A' I) ≫
        uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯ =
    homMk (g ▷ I) ⋯ ≫
      homMk
        (Iso.hom (β_ A I) ≫
          uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
        ⋯
have rw : homMk
    (Iso.hom (β_ A' I) ≫
      uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
    sorry =
  homMk
    (g ▷ I ≫
      Iso.hom (β_ A I) ≫ uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
    sorry
Tactic: rw [← Over.homMk_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.Sections (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
A' A : C
X : Over.{v₁, u₁} I
g : A' ⟶ A
v : A ⟶ Functor.obj (sections I) X
⊢ homMk
      (Iso.hom (β_ A' I) ≫
        uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯ =
    homMk
      (g ▷ I ≫
        Iso.hom (β_ A I) ≫ uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))))
      ⋯
have e_f : Iso.hom (β_ A' I) ≫ uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))) =
  g ▷ I ≫
    Iso.hom (β_ A I) ≫ uncurry (v ≫ ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.Sections (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
A : C
X' X : Over.{v₁, u₁} I
u : Functor.obj (toOver I) A ⟶ X'
g : X' ⟶ X
⊢ Eq (α := A ⟶ Functor.obj (sections I) X)
    (({ toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } :
          (a : (toOver I).obj A ⟶ X) → A ⟶ (sections I).obj X)
        (u ≫ g) :
      A ⟶ Functor.obj (sections I) X)
    (({ toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } :
            (a : (toOver I).obj A ⟶ X') → A ⟶ (sections I).obj X')
          u ≫
        Functor.map (sections I) g :
      A ⟶ Functor.obj (sections I) X)
have dsimp : Eq (α :=
  A ⟶
    pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
      (curry (Iso.hom (ρ_ I))))
  (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u ≫ Hom.left g)) (toUnit A) sorry)
  (CategoryStruct.comp (Y :=
    pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X'.left) (Functor.map (ihom I) X'.hom)
      (curry (Iso.hom (ρ_ I))))
    (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) sorry)
    (pullbackMap (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) X'.hom)
      (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) (Hom.left g)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)) sorry sorry))
Tactic: dsimp [sectionsCurry, sectionsUncurry, curryRightUnitorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.Sections (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
A : C
X' X : Over.{v₁, u₁} I
u : Functor.obj (toOver I) A ⟶ X'
g : X' ⟶ X
⊢ Eq (α :=
    A ⟶
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
        (curry (Iso.hom (ρ_ I))))
    (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯)
    (CategoryStruct.comp (Y :=
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X'.left) (Functor.map (ihom I) X'.hom)
        (curry (Iso.hom (ρ_ I))))
      (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) ⋯)
      (pullbackMap (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) X'.hom)
        (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) (Hom.left g)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)) ⋯ ⋯))
have h₁ : CategoryStruct.comp (Y :=
    pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
      (curry (Iso.hom (ρ_ I))))
    (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u ≫ Hom.left g)) (toUnit A) sorry)
    (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))) =
  CategoryStruct.comp (Y :=
    pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
      (curry (Iso.hom (ρ_ I))))
    (CategoryStruct.comp (Y :=
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X'.left) (Functor.map (ihom I) X'.hom)
        (curry (Iso.hom (ρ_ I))))
      (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) sorry)
      (pullbackMap (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) X'.hom)
        (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) (Hom.left g)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)) sorry sorry))
    (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))))
Tactic: apply ChosenPullbacksAlong.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyDirected (goal)
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)
⊢ F.IsLocallyDirected
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyDirected (goal)
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))
⊢ F.IsLocallyDirected
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyDirected (goal)
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
⊢ ∀ (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
have 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
Tactic: simp only [WidePushoutShape.hom_id, Functor.map_id, id_apply, forall_comm, forall_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyDirected (goal)
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) (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
have 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))
Tactic: simp only [WidePushoutShape.hom_id, Functor.map_id, id_apply, forall_eq']
-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyDirected (goal)
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 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
have 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
Tactic: simp only [((CategoryTheory.mono_iff_injective (F.map (.init i))).mp inferInstance).eq_iff,
      forall_eq']
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Basic (goal)
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)
⊢ f = ε
have rw : f ≫ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) = ε
Tactic: rw [← Category.comp_id f, ← discard_unit, discard_natural]
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Basic (goal)
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)) = ε
⊢ f = ε
have rw₁ : Eq (α := X ⟶ tensorUnit.{v, u} C (𝒞 := inst)) (f ≫ ε) ε
Tactic: rw [← Category.comp_id f, ← discard_unit, discard_natural]
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Basic (goal)
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 ≫ ε) ε
⊢ f = ε
have rw₂ : Eq.{v + 1} (α := X ⟶ tensorUnit.{v, u} C (𝒞 := inst)) ε ε
Tactic: rw [← Category.comp_id f, ← discard_unit, discard_natural]
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Positive (goal)
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 (f ≫ inv f)
have rw : Deterministic.{v, u} (𝟙 X)
Tactic: rw [IsIso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Positive (goal)
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)) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y))
have rw : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((Δ ≫ (f ≫ inv f ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y))
Tactic: rw [copy_comp_natural (h := by rw [IsIso.hom_inv_id]; infer_instance)]
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Positive (goal)
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))
have rw : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y)) (Δ ≫ (𝟙 X ≫ f ⊗ₘ f ≫ 𝟙 Y))
Tactic: rw [MonoidalCategory.tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Positive (goal)
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 ⊗ₘ f))
have _ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ) (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y))
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
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Positive (goal)
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 ≫ Δ) (Δ ≫ (f ⊗ₘ f))
have _₁ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y) ≫ (f ⊗ₘ 𝟙 Y))
  ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y))
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
-- Lean 4 proof step from Mathlib.CategoryTheory.MarkovCategory.Positive (goal)
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 ≫ Δ) (Δ ≫ (f ⊗ₘ f))
have _₂ : Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y) ((f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y)) ((Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y))
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