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
⊢ CategoryStruct.comp (Y := tensorObjOf (tensorObjOf x y) z) (inr' (tensorObjOf x y) z)
      (WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))) =
    inr' y z ≫ inr' x (tensorObjOf y z)
have a : ∀ (i : Fin (z.len + 1)),
  Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (CategoryStruct.comp (Y := tensorObjOf (tensorObjOf x y) z) (inr' (tensorObjOf x y) z)
              (WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z))))) :
          (a : Fin (z.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' y z ≫ inr' x (tensorObjOf y z)) :
          (a : Fin (z.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 (z.len + 1)
⊢ Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (CategoryStruct.comp (Y := tensorObjOf (tensorObjOf x y) z) (inr' (tensorObjOf x y) z)
              (WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z))))) :
          (a : Fin (z.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' y z ≫ inr' x (tensorObjOf y z)) :
          (a : Fin (z.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 (inr' (tensorObjOf x y) z) :
          (a : Fin (z.len + 1)) → Fin (x.len + y.len + 1 + z.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 (inr' y z) : (a : Fin (z.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 (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.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 (inr' (tensorObjOf x y) z) :
            (a : Fin (z.len + 1)) → Fin (x.len + y.len + 1 + z.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 (inr' y z) : (a : Fin (z.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))
  (Fin.cast sorry
    ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z) :
        (a : Fin (z.len + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
      i))
  ((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 (inr' y z) : (a : Fin (z.len + 1)) → Fin (y.len + z.len + 1 + 1)) i))
Tactic: simp only [eqToHom_toOrderHom, SimplexCategory.len_mk, OrderEmbedding.toOrderHom_coe,
      OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply]
-- 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 (z.len + 1)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯
      ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z) :
          (a : Fin (z.len + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        i))
    ((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 (inr' y z) : (a : Fin (z.len + 1)) → Fin (y.len + z.len + 1 + 1)) i))
have e₁ : Eq (α := Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
  ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z) :
        (a : Fin (z.len + 1)) → Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
      i :
    Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
  (Fin.cast sorry (Fin.natAdd (tensorObjOf x y).len.succ i) : Fin ((tensorObjOf x y).len + (z.len + 1)).succ)
Tactic: have e₁ := inr'_eval (tensorObjOf x 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 (z.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z) :
          (a : Fin (z.len + 1)) → Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
        i :
      Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    (Fin.cast ⋯ (Fin.natAdd (tensorObjOf x y).len.succ i) : Fin ((tensorObjOf x y).len + (z.len + 1)).succ)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯
      ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z) :
          (a : Fin (z.len + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        i))
    ((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 (inr' y z) : (a : Fin (z.len + 1)) → Fin (y.len + z.len + 1 + 1)) i))
have e₂ : Eq (α := Fin ((tensorObjOf y z).len + 1))
  ((SimplexCategory.Hom.toOrderHom (inr' y z) : (a : Fin (z.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
    Fin ((tensorObjOf y z).len + 1))
  (Fin.cast sorry (Fin.natAdd y.len.succ i) : Fin (y.len + (z.len + 1)).succ)
Tactic: have e₂ := inr'_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 (z.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z) :
          (a : Fin (z.len + 1)) → Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
        i :
      Fin ((tensorObjOf (tensorObjOf x y) z).len + 1))
    (Fin.cast ⋯ (Fin.natAdd (tensorObjOf x y).len.succ i) : Fin ((tensorObjOf x y).len + (z.len + 1)).succ)
e₂ :
  Eq (α := Fin ((tensorObjOf y z).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' y z) : (a : Fin (z.len + 1)) → Fin ((tensorObjOf y z).len + 1)) i :
      Fin ((tensorObjOf y z).len + 1))
    (Fin.cast ⋯ (Fin.natAdd y.len.succ i) : Fin (y.len + (z.len + 1)).succ)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯
      ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z) :
          (a : Fin (z.len + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        i))
    ((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 (inr' y z) : (a : Fin (z.len + 1)) → Fin (y.len + z.len + 1 + 1)) i))
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.natAdd (y.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.natAdd (y.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.natAdd (y.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 (z.len + 1)
e₁ :
  Eq (α := Fin (x.len + y.len + 1 + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z) :
          (a : Fin (z.len + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        i :
      Fin (x.len + y.len + 1 + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i) : Fin (x.len + y.len + 1 + (z.len + 1)).succ)
e₂ :
  Eq (α := Fin (y.len + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' y z) : (a : Fin (z.len + 1)) → Fin (y.len + z.len + 1 + 1)) i :
      Fin (y.len + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd y.len.succ i) : Fin (y.len + (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.natAdd (y.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.natAdd (y.len + 1) i))) :
      Fin (x.len + (y.len + z.len + 1 + 1)).succ)
⊢ Eq (α := Fin (x.len + (y.len + z.len + 1) + 1 + 1))
    (Fin.cast ⋯
      ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z) :
          (a : Fin (z.len + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        i))
    ((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 (inr' y z) : (a : Fin (z.len + 1)) → Fin (y.len + z.len + 1 + 1)) i))
have a : Fin.cast sorry (Fin.cast sorry (Fin.natAdd (x.len + y.len + 1).succ i)) =
  Fin.cast sorry (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) sorry (Fin.natAdd (y.len + 1) i)))
Tactic: rw [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 (z.len + 1)
e₁ :
  Eq (α := Fin (x.len + y.len + 1 + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z) :
          (a : Fin (z.len + 1)) → Fin (x.len + y.len + 1 + z.len + 1 + 1))
        i :
      Fin (x.len + y.len + 1 + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i) : Fin (x.len + y.len + 1 + (z.len + 1)).succ)
e₂ :
  Eq (α := Fin (y.len + z.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' y z) : (a : Fin (z.len + 1)) → Fin (y.len + z.len + 1 + 1)) i :
      Fin (y.len + z.len + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd y.len.succ i) : Fin (y.len + (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.natAdd (y.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.natAdd (y.len + 1) i))) :
      Fin (x.len + (y.len + z.len + 1 + 1)).succ)
⊢ Fin.cast ⋯ (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) ⋯ (Fin.natAdd (y.len + 1) i)))
have a : (↑(Fin.cast sorry (Fin.cast sorry (Fin.natAdd (x.len + y.len + 1).succ i))) : ℕ) =
  (↑(Fin.cast sorry (Fin.natAdd x.len.succ (Fin.cast (n := y.len + 1 + (z.len + 1)) sorry (Fin.natAdd (y.len + 1) i)))) : ℕ)
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 x ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x)
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of y) (WithInitial.of z)))
    (inl (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 x)
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of y) (WithInitial.of z)))
have change : Eq (α := x ⟶ tensorObjOf x (tensorObjOf y z))
  (inl' x y ≫
    inl' (tensorObjOf x y) z ≫ WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z))))
  (inl' x (tensorObjOf y z))
Tactic: change inl' _ _ ≫ inl' _ _ ≫ WithInitial.down _ = inl' _ _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ Eq (α := x ⟶ tensorObjOf x (tensorObjOf y z))
    (inl' x y ≫
      inl' (tensorObjOf x y) z ≫
        WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z))))
    (inl' x (tensorObjOf y z))
have a : ∀ (i : Fin (x.len + 1)),
  Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (inl' x y ≫
              inl' (tensorObjOf x y) z ≫
                WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))) :
          (a : Fin (x.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z)) :
          (a : Fin (x.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 (x.len + 1)
⊢ Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (inl' x y ≫
              inl' (tensorObjOf x y) z ≫
                WithInitial.down (Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))) :
          (a : Fin (x.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z)) :
          (a : Fin (x.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 (inl' x y) : (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
    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))
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 (x.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 (inl' x y) : (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      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))
have e₁ : Eq (α := Fin ((tensorObjOf x y).len + 1))
  ((SimplexCategory.Hom.toOrderHom (inl' x y) : (a : Fin (x.len + 1)) → Fin ((tensorObjOf x y).len + 1)) i :
    Fin ((tensorObjOf x y).len + 1))
  (Fin.cast sorry (Fin.castAdd (y.len + 1) i) : Fin (x.len + (y.len + 1)).succ)
Tactic: have e₁ := inl'_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 (x.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf x y).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x y) : (a : Fin (x.len + 1)) → Fin ((tensorObjOf x y).len + 1)) i :
      Fin ((tensorObjOf x y).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (y.len + 1) 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 (inl' x y) : (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      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))
have e₂ : Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
  ((SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z)) :
        (a : Fin (x.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
      i :
    Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
  (Fin.cast sorry (Fin.castAdd ((tensorObjOf y z).len + 1) i) : Fin (x.len + ((tensorObjOf y z).len + 1)).succ)
Tactic: have e₂ := inl'_eval x (tensorObjOf 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 (x.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf x y).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x y) : (a : Fin (x.len + 1)) → Fin ((tensorObjOf x y).len + 1)) i :
      Fin ((tensorObjOf x y).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i) : Fin (x.len + (y.len + 1)).succ)
e₂ :
  Eq (α := Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z)) :
          (a : Fin (x.len + 1)) → Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
        i :
      Fin ((tensorObjOf x (tensorObjOf y z)).len + 1))
    (Fin.cast ⋯ (Fin.castAdd ((tensorObjOf y z).len + 1) i) : Fin (x.len + ((tensorObjOf y 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 (inl' x y) : (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      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))
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.castAdd (y.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.castAdd (y.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.castAdd (y.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 (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))
        ((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 (inl' x y) : (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1)) i)) :
      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))
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.castAdd (y.len + 1) i)))) :
    Fin (x.len + (y.len + z.len + 1) + 1 + 1))
  (Fin.cast sorry (Fin.castAdd (y.len + z.len + 1 + 1) i) : Fin (x.len + (y.len + z.len + 1 + 1)).succ)
Tactic: rw [e₁, e₂, e₃]