awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
e₁ :
  Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x y) : (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1)) i :
      Fin (x.len + y.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i) : Fin (x.len + (y.len + 1)).succ)
e₂ :
  Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z)) :
          (a : Fin (x.len + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        i :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i) : Fin (x.len + (y.len + z.len + 1 + 1)).succ)
e₃ :
  Eq (α := Fin (x.len + y.len + 1 + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
          (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.castAdd (y.len + 1) i)) :
      Fin (x.len + y.len + 1 + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.castAdd (y.len + 1) i))) :
      Fin (x.len + y.len + 1 + (z.len + 1)).succ)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.castAdd (y.len + 1) i)))) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i) : Fin (x.len + (y.len + z.len + 1 + 1)).succ)
have a : (↑((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom sorry)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        (Fin.cast sorry
          (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) sorry (Fin.castAdd (y.len + 1) i))))) :
    ℕ) =
  (↑(Fin.cast sorry (Fin.castAdd (y.len + z.len + 1 + 1) i) : Fin (x.len + (y.len + z.len + 1 + 1)).succ) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ Eq (α :=
    WithInitial.of y ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x)
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of y) (WithInitial.of z)))
    (inr (WithInitial.of x) (WithInitial.of y) ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y)).inl
          (WithInitial.of z) ≫
        Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))
    (inl (WithInitial.of y) (WithInitial.of z) ≫
      inr (WithInitial.of x)
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of y) (WithInitial.of z)))
have change : inr' x y ≫
    inl' (tensorObjOf x y) z ≫
      WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z))) =
  inl' y z ≫ inr' x (tensorObjOf y z)
Tactic: change inr' _ _ ≫ inl' _ _ ≫ WithInitial.down _ = inl' _ _ ≫ inr' _ _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ inr' x y ≫
      inl' (tensorObjOf x y) z ≫
        WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z))) =
    inl' y z ≫ inr' x (tensorObjOf y z)
have a : ∀ (i : Fin (y.len + 1)),
  Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (inr' x y ≫
              inl' (tensorObjOf x y) z ≫
                WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))) :
          (a : Fin (y.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z ≫ inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
⊢ Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (inr' x y ≫
              inl' (tensorObjOf x y) z ≫
                WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))) :
          (a : Fin (y.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z ≫ inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
have a : Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
  ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom sorry)) :
        (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
          (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
    Fin (x.len + (y.len + z.len + 1) + 1 + 1))
  ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
        (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
      ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i) :
    Fin (x.len + (y.len + z.len + 1) + 1 + 1))
Tactic: dsimp [MonoidalCategoryStruct.associator, associator]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
            (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
          ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
have e₁ : Eq (α := Fin ((tensorObjOf y z).len + 1))
  ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
    Fin ((tensorObjOf y z).len + 1))
  (Fin.cast sorry (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
Tactic: have e₁ := inl'_eval y z i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf y z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
      Fin ((tensorObjOf y z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
            (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
          ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
have e₂ : Eq (α := Fin ((tensorObjOf x y).len + 1))
  ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf x y).len + 1)) i :
    Fin ((tensorObjOf x y).len + 1))
  (Fin.cast sorry (Fin.natAdd x.len.succ i) : Fin (x.len + (y.len + 1)).succ)
Tactic: have e₂ := inr'_eval x y i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf y z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
      Fin ((tensorObjOf y z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
e₂ :
  Eq (α := Fin ((tensorObjOf x y).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf x y).len + 1)) i :
      Fin ((tensorObjOf x y).len + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ i) : Fin (x.len + (y.len + 1)).succ)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
            (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
          ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
have e₃ : Eq (α := Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
  ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
        (a : Fin ((tensorObjOf x y).len + 1)) → Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
      (Fin.cast (n := x.len + 1 + (y.len + 1)) sorry (Fin.natAdd (x.len + 1) i)) :
    Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
  (Fin.cast sorry (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) sorry (Fin.natAdd (x.len + 1) i))) :
    Fin ((tensorObjOf x y).len + (z.len + 1)).succ)
Tactic: have e₃ := inl'_eval (tensorObjOf x y) z <| Fin.cast (by simp +arith) <| i.natAdd (x.len + 1)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf y z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
      Fin ((tensorObjOf y z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
e₂ :
  Eq (α := Fin ((tensorObjOf x y).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf x y).len + 1)) i :
      Fin ((tensorObjOf x y).len + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ i) : Fin (x.len + (y.len + 1)).succ)
e₃ :
  Eq (α := Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
          (a : Fin ((tensorObjOf x y).len + 1)) → Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
        (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)) :
      Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i))) :
      Fin ((tensorObjOf x y).len + (z.len + 1)).succ)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
            (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
          ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
have e₄ : Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
  ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
        (a : Fin ((tensorObjOf y z).len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
      (Fin.cast (n := y.len + 1 + (z.len + 1)) sorry (Fin.castAdd (z.len + 1) i)) :
    Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
  (Fin.cast sorry (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) sorry (Fin.castAdd (z.len + 1) i))) :
    Fin (x.len + ((tensorObjOf y z).len + 1)).succ)
Tactic: have e₄ := inr'_eval x (tensorObjOf y z) <| Fin.cast (by simp +arith) <| i.castAdd (z.len + 1)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin (y.len + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i :
      Fin (y.len + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
e₂ :
  Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1)) i :
      Fin (x.len + y.len + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ i) : Fin (x.len + (y.len + 1)).succ)
e₃ :
  Eq (α := Fin (x.len + y.len + 1 + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
          (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)) :
      Fin (x.len + y.len + 1 + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i))) :
      Fin (x.len + y.len + 1 + (z.len + 1)).succ)
e₄ :
  Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i))) :
      Fin (x.len + (y.len + z.len + 1 + 1)).succ)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
            (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
          ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
have a : Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
  ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom sorry)) :
        (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
      (Fin.cast sorry (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) sorry (Fin.natAdd (x.len + 1) i)))) :
    Fin (x.len + (y.len + z.len + 1) + 1 + 1))
  (Fin.cast sorry (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) sorry (Fin.castAdd (z.len + 1) i))) :
    Fin (x.len + (y.len + z.len + 1 + 1)).succ)
Tactic: rw [e₁, e₂, e₃, e₄]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ :
  Eq (α := Fin (y.len + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y z) : (a : Fin (y.len + 1)) → Fin (y.len + z.len + 1 + 1)) i :
      Fin (y.len + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i) : Fin (y.len + (z.len + 1)).succ)
e₂ :
  Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1)) i :
      Fin (x.len + y.len + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ i) : Fin (x.len + (y.len + 1)).succ)
e₃ :
  Eq (α := Fin (x.len + y.len + 1 + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z) :
          (a : Fin (x.len + y.len + 1 + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)) :
      Fin (x.len + y.len + 1 + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i))) :
      Fin (x.len + y.len + 1 + (z.len + 1)).succ)
e₄ :
  Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z)) :
          (a : Fin (y.len + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i)) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i))) :
      Fin (x.len + (y.len + z.len + 1 + 1)).succ)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) ⋯ (Fin.natAdd (x.len + 1) i)))) :
      Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.castAdd (z.len + 1) i))) :
      Fin (x.len + (y.len + z.len + 1 + 1)).succ)
have a : (↑((SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom sorry)) :
          (a : Fin (x.len + y.len + 1 + z.len + 1 + 1)) → Fin (x.len + (y.len + z.len + 1) + 1 + 1))
        (Fin.cast sorry (Fin.castAdd (z.len + 1) (Fin.cast (n := x.len + 1 + (y.len + 1)) sorry (Fin.natAdd (x.len + 1) i))))) :
    ℕ) =
  (↑(Fin.cast sorry (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) sorry (Fin.castAdd (z.len + 1) i)))) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x y : AugmentedSimplexCategory
⊢ 𝟙 x ⊗ₘ 𝟙 y = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y)
have h₁ : x.inl y ≫ (𝟙 x ⊗ₘ 𝟙 y) = x.inl y ≫ 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x y : AugmentedSimplexCategory
h₁ : x.inl y ≫ (𝟙 x ⊗ₘ 𝟙 y) = x.inl y ≫ 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y)
⊢ 𝟙 x ⊗ₘ 𝟙 y = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y)
have h₂ : x.inr y ≫ (𝟙 x ⊗ₘ 𝟙 y) = x.inr y ≫ 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
w x y z : AugmentedSimplexCategory
⊢ (Iso.hom (α_ w x y) ⊗ₘ 𝟙 z) ≫
      Iso.hom (α_ w (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y) z) ≫
        (𝟙 w ⊗ₘ Iso.hom (α_ x y z)) =
    Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y z) ≫
      Iso.hom (α_ w x (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) y z))
have h₁ : w.inl x ≫
    (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inl y ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
              (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inl
          z ≫
        (Iso.hom (α_ w x y) ⊗ₘ 𝟙 z) ≫
          Iso.hom (α_ w (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y) z) ≫
            (𝟙 w ⊗ₘ Iso.hom (α_ x y z)) =
  w.inl x ≫
    (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inl y ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
              (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inl
          z ≫
        Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y z) ≫
          Iso.hom (α_ w x (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) y z))
Tactic: ext