awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i i_1 : Fin (x₁.len + 1)
h : LE.le (α := Fin (x₁.len + 1 + (x₂.len + 1))) (Fin.castAdd (x₂.len + 1) i) (Fin.castAdd (x₂.len + 1) i_1)
⊢ LE.le (α := Fin (y₁.len + 1 + (y₂.len + 1)))
    ((fun (i : Fin (x₁.len + 1 + (x₂.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))
            i :
          Fin (y₁.len + 1 + (y₂.len + 1))))
      (Fin.castAdd (x₂.len + 1) i))
    ((fun (i : Fin (x₁.len + 1 + (x₂.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))
            i :
          Fin (y₁.len + 1 + (y₂.len + 1))))
      (Fin.castAdd (x₂.len + 1) i_1))
have h₁ : (↑(Fin.castAdd (x₂.len + 1) i) : ℕ) ≤ (↑(Fin.castAdd (x₂.len + 1) i_1) : ℕ)
Tactic: rw [Fin.le_def] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i : Fin (x₁.len + 1)
i_1 : Fin (x₂.len + 1)
h : Fin.castAdd (x₂.len + 1) i ≤ Fin.natAdd (x₁.len + 1) i_1
⊢ LE.le (α := Fin (y₁.len + 1 + (y₂.len + 1)))
    ((fun (i : Fin (x₁.len + 1 + (x₂.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))
            i :
          Fin (y₁.len + 1 + (y₂.len + 1))))
      (Fin.castAdd (x₂.len + 1) i))
    ((fun (i : Fin (x₁.len + 1 + (x₂.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))
            i :
          Fin (y₁.len + 1 + (y₂.len + 1))))
      (Fin.natAdd (x₁.len + 1) i_1))
have h₁ : (↑(Fin.castAdd (x₂.len + 1) i) : ℕ) ≤ (↑(Fin.natAdd (x₁.len + 1) i_1) : ℕ)
Tactic: rw [Fin.le_def] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i : Fin (x₂.len + 1)
i_1 : Fin (x₁.len + 1)
h : Fin.natAdd (x₁.len + 1) i ≤ Fin.castAdd (x₂.len + 1) i_1
⊢ LE.le (α := Fin (y₁.len + 1 + (y₂.len + 1)))
    ((fun (i : Fin (x₁.len + 1 + (x₂.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))
            i :
          Fin (y₁.len + 1 + (y₂.len + 1))))
      (Fin.natAdd (x₁.len + 1) i))
    ((fun (i : Fin (x₁.len + 1 + (x₂.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))
            i :
          Fin (y₁.len + 1 + (y₂.len + 1))))
      (Fin.castAdd (x₂.len + 1) i_1))
have h₁ : (↑(Fin.natAdd (x₁.len + 1) i) : ℕ) ≤ (↑(Fin.castAdd (x₂.len + 1) i_1) : ℕ)
Tactic: rw [Fin.le_def] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i i_1 : Fin (x₂.len + 1)
h : LE.le (α := Fin (x₁.len + 1 + (x₂.len + 1))) (Fin.natAdd (x₁.len + 1) i) (Fin.natAdd (x₁.len + 1) i_1)
⊢ LE.le (α := Fin (y₁.len + 1 + (y₂.len + 1)))
    ((fun (i : Fin (x₁.len + 1 + (x₂.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))
            i :
          Fin (y₁.len + 1 + (y₂.len + 1))))
      (Fin.natAdd (x₁.len + 1) i))
    ((fun (i : Fin (x₁.len + 1 + (x₂.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))
            i :
          Fin (y₁.len + 1 + (y₂.len + 1))))
      (Fin.natAdd (x₁.len + 1) i_1))
have h₁ : (↑(Fin.natAdd (x₁.len + 1) i) : ℕ) ≤ (↑(Fin.natAdd (x₁.len + 1) i_1) : ℕ)
Tactic: rw [Fin.le_def] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i i_1 : Fin (x₁.len + 1)
h : (↑(Fin.castAdd (x₂.len + 1) i) : ℕ) ≤ (↑(Fin.castAdd (x₂.len + 1) i_1) : ℕ)
⊢ (↑((fun (i : Fin (x₁.len + 1 + (x₂.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))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.castAdd (x₂.len + 1) i)) :
      ℕ) ≤
    (↑((fun (i : Fin (x₁.len + 1 + (x₂.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))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.castAdd (x₂.len + 1) i_1)) :
      ℕ)
have left : ∀ (h : i ≤ i_1),
  LE.le (α := Fin (y₁.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i : Fin (y₁.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i_1 : Fin (y₁.len + 1))
Tactic: simp at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i : Fin (x₁.len + 1)
i_1 : Fin (x₂.len + 1)
h : (↑(Fin.castAdd (x₂.len + 1) i) : ℕ) ≤ (↑(Fin.natAdd (x₁.len + 1) i_1) : ℕ)
⊢ (↑((fun (i : Fin (x₁.len + 1 + (x₂.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))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.castAdd (x₂.len + 1) i)) :
      ℕ) ≤
    (↑((fun (i : Fin (x₁.len + 1 + (x₂.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))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.natAdd (x₁.len + 1) i_1)) :
      ℕ)
have left : (↑((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i) : ℕ) ≤
  y₁.len + 1 + (↑((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i_1) : ℕ)
Tactic: simp at h ⊢
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i : Fin (x₂.len + 1)
i_1 : Fin (x₁.len + 1)
h : (↑(Fin.natAdd (x₁.len + 1) i) : ℕ) ≤ (↑(Fin.castAdd (x₂.len + 1) i_1) : ℕ)
⊢ (↑((fun (i : Fin (x₁.len + 1 + (x₂.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))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.natAdd (x₁.len + 1) i)) :
      ℕ) ≤
    (↑((fun (i : Fin (x₁.len + 1 + (x₂.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))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.castAdd (x₂.len + 1) i_1)) :
      ℕ)
have right : y₁.len + 1 + (↑((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i) : ℕ) ≤
  (↑((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (x₁.len + 1)) → Fin (y₁.len + 1)) i_1) : ℕ)
Tactic: simp at h ⊢
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i i_1 : Fin (x₂.len + 1)
h : (↑(Fin.natAdd (x₁.len + 1) i) : ℕ) ≤ (↑(Fin.natAdd (x₁.len + 1) i_1) : ℕ)
⊢ (↑((fun (i : Fin (x₁.len + 1 + (x₂.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))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.natAdd (x₁.len + 1) i)) :
      ℕ) ≤
    (↑((fun (i : Fin (x₁.len + 1 + (x₂.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))
                i :
              Fin (y₁.len + 1 + (y₂.len + 1))))
          (Fin.natAdd (x₁.len + 1) i_1)) :
      ℕ)
have right : ∀ (h : i ≤ i_1),
  LE.le (α := Fin (y₂.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i : Fin (y₂.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (x₂.len + 1)) → Fin (y₂.len + 1)) i_1 : Fin (y₂.len + 1))
Tactic: simp at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x : AugmentedSimplexCategory
⊢ x ◁ 𝟙 WithInitial.star = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x WithInitial.star)
have of : ∀ (a : SimplexCategory),
  WithInitial.of a ◁ 𝟙 WithInitial.star =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of a) WithInitial.star)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x : AugmentedSimplexCategory
of :
  ∀ (a : SimplexCategory),
    WithInitial.of a ◁ 𝟙 WithInitial.star =
      𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of a) WithInitial.star)
⊢ x ◁ 𝟙 WithInitial.star = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x WithInitial.star)
have star : Eq (α :=
  Quiver.Hom (V := AugmentedSimplexCategory)
    (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star)
    (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))
  (WithInitial.star ◁ 𝟙 WithInitial.star)
  (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x : AugmentedSimplexCategory
⊢ 𝟙 WithInitial.star ▷ x = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star x)
have of : ∀ (a : SimplexCategory),
  𝟙 WithInitial.star ▷ WithInitial.of a =
    𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of a))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x : AugmentedSimplexCategory
of :
  ∀ (a : SimplexCategory),
    𝟙 WithInitial.star ▷ WithInitial.of a =
      𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star (WithInitial.of a))
⊢ 𝟙 WithInitial.star ▷ x = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star x)
have star : Eq (α :=
  Quiver.Hom (V := WithInitial SimplexCategory)
    (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star)
    (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))
  (𝟙 WithInitial.star ▷ WithInitial.star)
  (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) WithInitial.star WithInitial.star))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x y : SimplexCategory
i : Fin (x.len + 1)
⊢ 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)
have dsimp : Eq (α := Fin (x.len + y.len + 1 + 1))
  ((SimplexCategory.Hom.toOrderHom
          (𝟙 (WithInitial.of x) ≫
            𝟙 (WithInitial.of x) ≫
              SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.castAddOrderEmb (y.len + 1))) ≫ eqToHom sorry) :
        (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1))
      i :
    Fin (x.len + y.len + 1 + 1))
  (Fin.cast sorry (Fin.castAdd (y.len + 1) i) : Fin (x.len + (y.len + 1) + 1))
Tactic: dsimp [inl', inl, MonoidalCategoryStruct.rightUnitor, MonoidalCategoryStruct.whiskerLeft,
    tensorHom, WithInitial.down, rightUnitor, tensorObj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x y : SimplexCategory
i : Fin (x.len + 1)
⊢ Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom
            (𝟙 (WithInitial.of x) ≫
              𝟙 (WithInitial.of x) ≫
                SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.castAddOrderEmb (y.len + 1))) ≫ eqToHom ⋯) :
          (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) + 1))
have h : (↑((SimplexCategory.Hom.toOrderHom
            (𝟙 (WithInitial.of x) ≫
              𝟙 (WithInitial.of x) ≫
                SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.castAddOrderEmb (y.len + 1))) ≫ eqToHom sorry) :
          (a : Fin (x.len + 1)) → Fin (x.len + y.len + 1 + 1))
        i) :
    ℕ) =
  (↑(Fin.cast sorry (Fin.castAdd (y.len + 1) i) : Fin (x.len + (y.len + 1) + 1)) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x y : SimplexCategory
i : Fin (y.len + 1)
⊢ Eq (α := Fin ((tensorObjOf x y).len + 1))
    ((SimplexCategory.Hom.toOrderHom (inr' x y) : (a : Fin (y.len + 1)) → Fin ((tensorObjOf x y).len + 1)) i :
      Fin ((tensorObjOf x y).len + 1))
    (Fin.cast ⋯ (Fin.natAdd x.len.succ i) : Fin (x.len + (y.len + 1)).succ)
have dsimp : Eq (α := Fin (x.len + y.len + 1 + 1))
  ((SimplexCategory.Hom.toOrderHom
          (𝟙 (WithInitial.of y) ≫
            𝟙 (WithInitial.of y) ≫
              SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.natAddOrderEmb (x.len + 1))) ≫ eqToHom sorry) :
        (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1))
      i :
    Fin (x.len + y.len + 1 + 1))
  (Fin.cast sorry (Fin.natAdd (x.len + 1) i) : Fin (x.len + (y.len + 1) + 1))
Tactic: dsimp [inr', inr, MonoidalCategoryStruct.leftUnitor, MonoidalCategoryStruct.whiskerRight,
    tensorHom, WithInitial.down, leftUnitor, tensorObj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x y : SimplexCategory
i : Fin (y.len + 1)
⊢ Eq (α := Fin (x.len + y.len + 1 + 1))
    ((SimplexCategory.Hom.toOrderHom
            (𝟙 (WithInitial.of y) ≫
              𝟙 (WithInitial.of y) ≫
                SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.natAddOrderEmb (x.len + 1))) ≫ eqToHom ⋯) :
          (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1))
        i :
      Fin (x.len + y.len + 1 + 1))
    (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i) : Fin (x.len + (y.len + 1) + 1))
have h : (↑((SimplexCategory.Hom.toOrderHom
            (𝟙 (WithInitial.of y) ≫
              𝟙 (WithInitial.of y) ≫
                SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.natAddOrderEmb (x.len + 1))) ≫ eqToHom sorry) :
          (a : Fin (y.len + 1)) → Fin (x.len + y.len + 1 + 1))
        i) :
    ℕ) =
  (↑(Fin.cast sorry (Fin.natAdd (x.len + 1) i)) : ℕ)
Tactic: ext
-- 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 :
  MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y) ⟶
    WithInitial.of z
h₁ : inl (WithInitial.of x) (WithInitial.of y) ≫ f = inl (WithInitial.of x) (WithInitial.of y) ≫ g
h₂ : inr (WithInitial.of x) (WithInitial.of y) ≫ f = inr (WithInitial.of x) (WithInitial.of y) ≫ g
⊢ f = g
have change : ∀ (f g : tensorObjOf x y ⟶ z)
  (h₁ :
    Eq (α := WithInitial.of x ⟶ WithInitial.of z)
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
        (inl (WithInitial.of x) (WithInitial.of y)) f)
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
        (inl (WithInitial.of x) (WithInitial.of y)) g))
  (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)),
  f = g
Tactic: change (tensorObjOf x y) ⟶ z at f g
Cleared hypotheses: f, g, h₁, h₂
-- 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 x ⟶ WithInitial.of z)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
      (inl (WithInitial.of x) (WithInitial.of y)) f)
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) (WithInitial.of x) (WithInitial.of y))
      (inl (WithInitial.of x) (WithInitial.of y)) g)
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)
⊢ f = g
have h₃ : inl' x y ≫ f = inl' x y ≫ g
Tactic: change inl' _ _ ≫ f = inl' _ _ ≫ g at h₁
Cleared hypotheses: h₁