awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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)
a :
  Eq (α := Fin (y₁.len + 1 + y₂.len + 1))
    (Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
    (Fin.castAdd (y₂.len + 1)
      ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
⊢ 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:
conv_lhs =>
      change Fin.addCases
        (fun i ↦ Fin.castAdd (y₂.len + 1) (f₁.toOrderHom i))
        (fun i ↦ Fin.natAdd (y₁.len + 1) (f₂.toOrderHom i))
        (Fin.castAdd (x₂.len + 1) i)
      rw [Fin.addCases_left]

Premises used: Fin.addCases_left
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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 + 1 + y₂.len + 1))
    (Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))
    (Fin.castAdd (y₂.len + 1)
      ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁) : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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₂
change : inr' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₂ ≫ inr' y₁ y₂
⊢ inr (WithInitial.of x₁) (WithInitial.of x₂) ≫ (f₁ ⊗ₘ f₂) = f₂ ≫ inr (WithInitial.of y₁) (WithInitial.of y₂)

Tactic:
change inr' _ _ ≫ tensorHomOf _ _ = WithInitial.down f₂ ≫ inr' _ _

Premises used: AugmentedSimplexCategory.inr', AugmentedSimplexCategory.tensorHomOf, CategoryTheory.WithInitial.down
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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₂
a :
  ∀ (i : Fin (x₂.len + 1)),
    Eq (α := Fin ((tensorObjOf y₁ y₂).len + 1))
      ((SimplexCategory.Hom.toOrderHom (inr' 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₂ ≫ inr' y₁ y₂) :
            (a : Fin (x₂.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
          i :
        Fin ((tensorObjOf y₁ y₂).len + 1))
⊢ inr' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₂ ≫ inr' y₁ y₂

Tactic:
ext i : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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)
a :
  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 (inr' 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 (inr' 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))
⊢ Eq (α := Fin ((tensorObjOf y₁ y₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' 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₂ ≫ inr' y₁ y₂) :
          (a : Fin (x₂.len + 1)) → Fin ((tensorObjOf y₁ y₂).len + 1))
        i :
      Fin ((tensorObjOf y₁ y₂).len + 1))

Tactic:
dsimp [tensorHomOf]

Premises used: AugmentedSimplexCategory.tensorHomOf
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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 x₁ x₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x₁ x₂) : (a : Fin (x₂.len + 1)) → Fin ((tensorObjOf x₁ x₂).len + 1)) i :
      Fin ((tensorObjOf x₁ x₂).len + 1))
    (Fin.cast ⋯ (Fin.natAdd x₁.len.succ i) : Fin (x₁.len + (x₂.len + 1)).succ)

Tactic:
have e₁ := inr'_eval x₁ x₂ i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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 (inr' x₁ x₂) : (a : Fin (x₂.len + 1)) → Fin ((tensorObjOf x₁ x₂).len + 1)) i :
      Fin ((tensorObjOf x₁ x₂).len + 1))
    (Fin.cast ⋯ (Fin.natAdd x₁.len.succ i) : Fin (x₁.len + (x₂.len + 1)).succ)
⊢ Eq (α := Fin ((tensorObjOf y₁ y₂).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' 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 ⋯
        (Fin.natAdd y₁.len.succ
          ((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₂ := inr'_eval y₁ y₂ <| (WithInitial.down f₂).toOrderHom i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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 (inr' 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.natAdd x₁.len.succ i) : Fin (x₁.len + (x₂.len + 1)).succ)
e₂ :
  Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' 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.natAdd y₁.len.succ
          ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂) : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i)) :
      Fin (y₁.len + (y₂.len + 1)).succ)
rw : Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i)
| (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.natAdd (x₁.len + 1) i) :
    Fin (y₁.len + 1 + (y₂.len + 1)))

Tactic:
rw [Fin.addCases_right]

Premises used: Fin.addCases_right
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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 (inr' 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.natAdd x₁.len.succ i) : Fin (x₁.len + (x₂.len + 1)).succ)
e₂ :
  Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' 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.natAdd y₁.len.succ
          ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂) : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i)) :
      Fin (y₁.len + (y₂.len + 1)).succ)
change : Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i)
| (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.natAdd (x₁.len + 1) i) :
    Fin (y₁.len + 1 + (y₂.len + 1)))

Tactic:
change Fin.addCases
        (fun i ↦ Fin.castAdd (y₂.len + 1) (f₁.toOrderHom i))
        (fun i ↦ Fin.natAdd (y₁.len + 1) (f₂.toOrderHom i))
        (Fin.natAdd (x₁.len + 1) i)
      rw [Fin.addCases_right]

Premises used: Fin.addCases_right
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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 (inr' 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.natAdd x₁.len.succ i) : Fin (x₁.len + (x₂.len + 1)).succ)
e₂ :
  Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' 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.natAdd y₁.len.succ
          ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂) : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i)) :
      Fin (y₁.len + (y₂.len + 1)).succ)
a :
  Eq (α := Fin (y₁.len + 1 + y₂.len + 1))
    (Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
    (Fin.natAdd (y₁.len + 1)
      ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂) : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
⊢ 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.natAdd (x₁.len + 1) i) :
      Fin (y₁.len + 1 + (y₂.len + 1)))
    (Fin.natAdd (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:
conv_lhs =>
      change Fin.addCases
        (fun i ↦ Fin.castAdd (y₂.len + 1) (f₁.toOrderHom i))
        (fun i ↦ Fin.natAdd (y₁.len + 1) (f₂.toOrderHom i))
        (Fin.natAdd (x₁.len + 1) i)
      rw [Fin.addCases_right]

Premises used: Fin.addCases_right
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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 (inr' 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.natAdd x₁.len.succ i) : Fin (x₁.len + (x₂.len + 1)).succ)
e₂ :
  Eq (α := Fin (y₁.len + y₂.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' 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.natAdd y₁.len.succ
          ((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 + 1 + y₂.len + 1))
    (Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))
    (Fin.natAdd (y₁.len + 1)
      ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂) : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
change :
  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)
⊢ Eq (α :=
    WithInitial.of z ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x)
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of y) (WithInitial.of z)))
    ((MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y)).inr
        (WithInitial.of z) ≫
      Iso.hom (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)))
    (inr (WithInitial.of y) (WithInitial.of z) ≫
      inr (WithInitial.of x)
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of y) (WithInitial.of z)))

Tactic:
change inr' _ _ ≫ WithInitial.down _ = inr' _ _ ≫ inr' _ _

Premises used: AugmentedSimplexCategory.inr', CategoryTheory.WithInitial.down
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
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))
⊢ 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)

Tactic:
ext i : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
a :
  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))
⊢ 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:
dsimp [MonoidalCategoryStruct.associator, associator]

Premises used: AugmentedSimplexCategory.associator, CategoryTheory.MonoidalCategoryStruct.associator
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
a :
  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))
⊢ 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))

Tactic:
simp only [eqToHom_toOrderHom, SimplexCategory.len_mk, OrderEmbedding.toOrderHom_coe,
      OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply]

Premises used: SimplexCategory.len_mk, AugmentedSimplexCategory.eqToHom_toOrderHom, OrderEmbedding.toOrderHom_coe, OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x_1 y_1 z_1 : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
⊢ 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)

Tactic:
have e₁ := inr'_eval (tensorObjOf x y) z i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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 ((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)

Tactic:
have e₂ := inr'_eval y z i