awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₂ :
  Eq (α := WithInitial.of y ⟶ WithInitial.of z)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
      (inr (WithInitial.of x) (WithInitial.of y)) f)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
      (inr (WithInitial.of x) (WithInitial.of y)) g)
h₁ : inl' x y ≫ f = inl' x y ≫ g
⊢ f = g
have h₃ : inr' x y ≫ f = inr' x y ≫ g
Tactic: change inr' _ _ ≫ f = inr' _ _ ≫ g at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
⊢ f = g
have h : ∀ (i : Fin ((tensorObjOf x y).len + 1)),
  (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          i) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) g :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          i) :
      ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          i) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) g :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          i) :
      ℕ)
have this : i = Fin.cast sorry j
Tactic: have : i = j.cast (Nat.succ_add x.len (y.len + 1)) := rfl
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          i) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) g :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          i) :
      ℕ)
have h : (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
        (Fin.cast sorry j)) :
    ℕ) =
  (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) g :
          (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
        (Fin.cast sorry j)) :
    ℕ)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j_1 : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j_1
j : Fin (x.len + 1)
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j))) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) g :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j))) :
      ℕ)
have h : ∀
  (h₁ :
    Eq (α := (a : Fin (x.len + 1)) → Fin (z.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ f)) : (a : Fin (x.len + 1)) → Fin (z.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ g)) : (a : Fin (x.len + 1)) → Fin (z.len + 1)))
  (h₂ : inr' x y ≫ f = inr' x y ≫ g) (i : Fin ((tensorObjOf x y).len + 1)),
  let j := Fin.cast sorry i;
  ∀ (this : i = Fin.cast sorry j) (j : Fin (x.len + 1)),
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
              (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
            (Fin.cast sorry (Fin.castAdd (y.len + 1) j))) :
        ℕ) =
      (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) g :
              (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
            (Fin.cast sorry (Fin.castAdd (y.len + 1) j))) :
        ℕ)
Tactic: rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₁
Cleared hypotheses: h₁, h₂, i, j_1, this, j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j_1 : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j_1
j : Fin (y.len + 1)
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j))) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) g :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j))) :
      ℕ)
have h : ∀
  (h₂ :
    Eq (α := (a : Fin (y.len + 1)) → Fin (z.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ f)) : (a : Fin (y.len + 1)) → Fin (z.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ g)) : (a : Fin (y.len + 1)) → Fin (z.len + 1)))
  (i : Fin ((tensorObjOf x y).len + 1)),
  let j := Fin.cast sorry i;
  ∀ (this : i = Fin.cast sorry j) (j : Fin (y.len + 1)),
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
              (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
            (Fin.cast sorry (Fin.natAdd (x.len + 1) j))) :
        ℕ) =
      (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) g :
              (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
            (Fin.cast sorry (Fin.natAdd (x.len + 1) j))) :
        ℕ)
Tactic: rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₂
Cleared hypotheses: h₂, i, j_1, this, j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y_1 ⟶ z_1
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          (Fin.cast ⋯ j)) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) g :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          (Fin.cast ⋯ j)) :
      ℕ)
have h : ∀ (x_2 : Fin (x.len + 1 + (y.len + 1))),
  (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          (Fin.cast sorry x_2)) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) g :
            (a : Fin ((tensorObjOf x y).len + 1)) → Fin (z.len + 1))
          (Fin.cast sorry x_2)) :
      ℕ)
Tactic: cases j using Fin.addCases (m := x.len + 1) (n := y.len + 1) with
    | left j =>
      rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₁
      simpa [← inl'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₁ j
    | right j =>
      rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₂
      simpa [← inr'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₂ j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x_1 y z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x_1 y ⟶ z_1
x z : SimplexCategory
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) WithInitial.star ⟶
    WithInitial.of z
h₁ : inl (WithInitial.of x) WithInitial.star ≫ f = inl (WithInitial.of x) WithInitial.star ≫ g
h₂ : inr (WithInitial.of x) WithInitial.star ≫ f = inr (WithInitial.of x) WithInitial.star ≫ g
⊢ f = g
have h₃ : 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) WithInitial.star) ≫ f =
  𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) WithInitial.star) ≫ g
Tactic: simp only [inl, Category.assoc, Iso.cancel_iso_inv_left, Limits.IsInitial.to_self,
        whiskerLeft_id_star] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x y_1 z_1 : AugmentedSimplexCategory
f_1 g_1 : MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y_1 ⟶ z_1
y z : SimplexCategory
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of y) ⟶
    WithInitial.of z
h₁ : inl WithInitial.star (WithInitial.of y) ≫ f = inl WithInitial.star (WithInitial.of y) ≫ g
h₂ : inr WithInitial.star (WithInitial.of y) ≫ f = inr WithInitial.star (WithInitial.of y) ≫ g
⊢ f = g
have h₃ : 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of y)) ≫ f =
  𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of y)) ≫ g
Tactic: simp only [inr, Category.assoc, Iso.cancel_iso_inv_left, Limits.IsInitial.to_self,
        id_star_whiskerRight] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inl (WithInitial.of x₁) (WithInitial.of x₂) ≫ (f₁ ⊗ₘ f₂) = f₁ ≫ inl (WithInitial.of y₁) (WithInitial.of y₂)
have change : inl' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₁ ≫ inl' y₁ y₂
Tactic: change inl' _ _ ≫ tensorHomOf _ _ = WithInitial.down f₁ ≫ inl' _ _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inl' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₁ ≫ inl' y₁ y₂
have a : ∀ (i : Fin (x₁.len + 1)),
  Eq (α := Fin ((tensorObjOf y₁ y₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂ ≫ tensorHomOf f₁ f₂) :
          (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
        i :
      Fin ((tensorObjOf y₁ y₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁ ≫ inl' y₁ y₂) :
          (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
        i :
      Fin ((tensorObjOf y₁ y₂).len + 1))
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
⊢ Eq (α := Fin ((tensorObjOf y₁ y₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂ ≫ tensorHomOf f₁ f₂) :
          (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
        i :
      Fin ((tensorObjOf y₁ y₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁ ≫ inl' y₁ y₂) :
          (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
        i :
      Fin ((tensorObjOf y₁ y₂).len + 1))
have a : Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
  ((SimplexCategory.Hom.toOrderHom (eqToHom sorry) : (a : Fin (y₁.len + 1 + y₂.len + 1)) → Fin (y₁.len + y₂.len + 1 + 1))
      (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
        (fun (i : Fin (x₁.len + 1)) ↦
          Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
        (fun (i : Fin (x₂.len + 1)) ↦
          Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
        ((SimplexCategory.Hom.toOrderHom (eqToHom sorry) :
            (a : Fin (x₁.len + x₂.len + 1 + 1)) → Fin (x₁.len + 1 + x₂.len + 1))
          ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂) : (a : Fin (x₁.len + 1)) → Fin (x₁.len + x₂.len + 1 + 1)) i))) :
    Fin (y₁.len + y₂.len + 1 + 1))
  ((SimplexCategory.Hom.toOrderHom (inl' y₁ y₂) : (a : Fin (y₁.len + 1)) → Fin (y₁.len + y₂.len + 1 + 1))
      ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) :
    Fin (y₁.len + y₂.len + 1 + 1))
Tactic: dsimp [tensorHomOf]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
⊢ Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯) : (a : Fin (y₁.len + 1 + y₂.len + 1)) → Fin (y₁.len + y₂.len + 1 + 1))
        (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
          (fun (i : Fin (x₁.len + 1)) ↦
            Fin.castAdd (y₂.len + 1)
              ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
          (fun (i : Fin (x₂.len + 1)) ↦
            Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
          ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯) :
              (a : Fin (x₁.len + x₂.len + 1 + 1)) → Fin (x₁.len + 1 + x₂.len + 1))
            ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂) : (a : Fin (x₁.len + 1)) → Fin (x₁.len + x₂.len + 1 + 1))
              i))) :
      Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y₁ y₂) : (a : Fin (y₁.len + 1)) → Fin (y₁.len + y₂.len + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) :
      Fin (y₁.len + y₂.len + 1 + 1))
have e₁ : Eq (α := Fin ((tensorObjOf x₁ x₂).len + 1))
  ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂) : (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf x₁ x₂).len + 1)) i :
    Fin ((tensorObjOf x₁ x₂).len + 1))
  (Fin.cast sorry (Fin.castAdd (x₂.len + 1) i) : Fin (x₁.len + (x₂.len + 1)).succ)
Tactic: have e₁ := inl'_eval x₁ x₂ i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
e₁ :
  Eq (α := Fin ((tensorObjOf x₁ x₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂) : (a : Fin (x₁.len + 1)) → Fin ((tensorObjOf x₁ x₂).len + 1)) i :
      Fin ((tensorObjOf x₁ x₂).len + 1))
    (Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i) : Fin (x₁.len + (x₂.len + 1)).succ)
⊢ Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯) : (a : Fin (y₁.len + 1 + y₂.len + 1)) → Fin (y₁.len + y₂.len + 1 + 1))
        (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
          (fun (i : Fin (x₁.len + 1)) ↦
            Fin.castAdd (y₂.len + 1)
              ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
          (fun (i : Fin (x₂.len + 1)) ↦
            Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
          ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯) :
              (a : Fin (x₁.len + x₂.len + 1 + 1)) → Fin (x₁.len + 1 + x₂.len + 1))
            ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂) : (a : Fin (x₁.len + 1)) → Fin (x₁.len + x₂.len + 1 + 1))
              i))) :
      Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y₁ y₂) : (a : Fin (y₁.len + 1)) → Fin (y₁.len + y₂.len + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) :
      Fin (y₁.len + y₂.len + 1 + 1))
have e₂ : Eq (α := Fin ((tensorObjOf y₁ y₂).len + 1))
  ((SimplexCategory.Hom.toOrderHom (inl' y₁ y₂) : (a : Fin (y₁.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
      ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) :
    Fin ((tensorObjOf y₁ y₂).len + 1))
  (Fin.cast sorry
      (Fin.castAdd (y₂.len + 1)
        ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i)) :
    Fin (y₁.len + (y₂.len + 1)).succ)
Tactic: have e₂ := inl'_eval y₁ y₂ <| (WithInitial.down f₁).toOrderHom i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x₁_1 y₁_1 x₂_1 y₂_1 : AugmentedSimplexCategory
f₁_1 : x₁_1 ⟶ y₁_1
f₂_1 : x₂_1 ⟶ y₂_1
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
e₁ :
  Eq (α := Fin (x₁.len + x₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂) : (a : Fin (x₁.len + 1)) → Fin (x₁.len + x₂.len + 1 + 1)) i :
      Fin (x₁.len + x₂.len + 1 + 1))
    (Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i) : Fin (x₁.len + (x₂.len + 1)).succ)
e₂ :
  Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inl' y₁ y₂) : (a : Fin (y₁.len + 1)) → Fin (y₁.len + y₂.len + 1 + 1))
        ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) :
      Fin (y₁.len + y₂.len + 1 + 1))
    (Fin.cast ⋯
        (Fin.castAdd (y₂.len + 1)
          ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i)) :
      Fin (y₁.len + (y₂.len + 1)).succ)
⊢ Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯) : (a : Fin (y₁.len + 1 + y₂.len + 1)) → Fin (y₁.len + y₂.len + 1 + 1))
        (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
          (fun (i : Fin (x₁.len + 1)) ↦
            Fin.castAdd (y₂.len + 1)
              ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
          (fun (i : Fin (x₂.len + 1)) ↦
            Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
          ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯) :
              (a : Fin (x₁.len + x₂.len + 1 + 1)) → Fin (x₁.len + 1 + x₂.len + 1))
            (Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i)))) :
      Fin (y₁.len + y₂.len + 1 + 1))
    (Fin.cast ⋯
        (Fin.castAdd (y₂.len + 1)
          ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i)) :
      Fin (y₁.len + (y₂.len + 1)).succ)
have a : Eq (α := Fin (y₁.len + 1 + y₂.len + 1))
  (Fin.addCases (motive := fun (x : Fin (x₁.len + 1 + (x₂.len + 1))) ↦ Fin (y₁.len + 1 + (y₂.len + 1)))
      (fun (i : Fin (x₁.len + 1)) ↦
        Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
      (fun (i : Fin (x₂.len + 1)) ↦
        Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
      (Fin.castAdd (x₂.len + 1) i) :
    Fin (y₁.len + 1 + (y₂.len + 1)))
  (Fin.castAdd (y₂.len + 1)
      ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) :
    Fin (y₁.len + 1 + (y₂.len + 1)))
Tactic: simp only [SimplexCategory.eqToHom_toOrderHom, SimplexCategory.len_mk,
      OrderEmbedding.toOrderHom_coe, OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply,
      Fin.cast_cast, Fin.cast_eq_self, Fin.cast_inj]