awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
| (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)))
have rw : Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i)
Tactic: rw [Fin.addCases_left]
-- 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)
| (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)))
have change : Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i)
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.castAdd (x₂.len + 1) i)
      rw [Fin.addCases_left]
-- 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 + 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)))
have 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))
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]
-- 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₂
⊢ inr (WithInitial.of x₁) (WithInitial.of x₂) ≫ (f₁ ⊗ₘ f₂) = f₂ ≫ inr (WithInitial.of y₁) (WithInitial.of y₂)
have change : inr' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₂ ≫ inr' y₁ y₂
Tactic: change inr' _ _ ≫ tensorHomOf _ _ = WithInitial.down f₂ ≫ inr' _ _
-- 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₂
⊢ inr' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₂ ≫ inr' y₁ y₂
have 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))
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 (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))
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 (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))
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 (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))
have 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 sorry (Fin.natAdd x₁.len.succ i) : Fin (x₁.len + (x₂.len + 1)).succ)
Tactic: have e₁ := inr'_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 (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 (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))
have e₂ : 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 sorry
      (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
-- 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 (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 + 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.natAdd x₁.len.succ 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)
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.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: simp only [SimplexCategory.eqToHom_toOrderHom, SimplexCategory.len_mk,
      Nat.succ_eq_add_one, OrderEmbedding.toOrderHom_coe,
      OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply,
      Fin.cast_cast, Fin.cast_eq_self, Fin.cast_inj]
-- 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 (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)
| (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)))
have rw : Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i)
Tactic: rw [Fin.addCases_right]
-- 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 (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)
| (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)))
have change : Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i)
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]
-- 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 (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.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)))
have 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))
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]
-- 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 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)))
have 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)
Tactic: change inr' _ _ ≫ WithInitial.down _ = inr' _ _ ≫ inr' _ _