Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case left.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₁.len + 1)
h : ↑(Fin.castAdd (x₂.len + 1) i✝¹) ≤ ↑(Fin.castAdd (x₂.len + 1) i✝)
⊢ ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝¹)) ≤
    ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝))

pp: case left.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₁.len + 1)
i✝ : Fin (x₂.len + 1)
h : ↑(Fin.castAdd (x₂.len + 1) i✝¹) ≤ ↑(Fin.natAdd (x₁.len + 1) i✝)
⊢ ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝¹)) ≤
    ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.natAdd (x₁.len + 1) i✝))

pp: case right.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₂.len + 1)
i✝ : Fin (x₁.len + 1)
h : ↑(Fin.natAdd (x₁.len + 1) i✝¹) ≤ ↑(Fin.castAdd (x₂.len + 1) i✝)
⊢ ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.natAdd (x₁.len + 1) i✝¹)) ≤
    ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝))

pp: case right.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₂.len + 1)
h : ↑(Fin.natAdd (x₁.len + 1) i✝¹) ≤ ↑(Fin.natAdd (x₁.len + 1) i✝)
⊢ ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.natAdd (x₁.len + 1) i✝¹)) ≤
    ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.natAdd (x₁.len + 1) i✝))

Tactic:
<;>

Goal state after:
case left.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₁.len + 1)
h : ↑(Fin.castAdd (x₂.len + 1) i✝¹) ≤ ↑(Fin.castAdd (x₂.len + 1) i✝)
⊢ ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝¹)) ≤
    ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝))

case left.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₁.len + 1)
i✝ : Fin (x₂.len + 1)
h : ↑(Fin.castAdd (x₂.len + 1) i✝¹) ≤ ↑(Fin.natAdd (x₁.len + 1) i✝)
⊢ ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝¹)) ≤
    ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.natAdd (x₁.len + 1) i✝))

case right.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₂.len + 1)
i✝ : Fin (x₁.len + 1)
h : ↑(Fin.natAdd (x₁.len + 1) i✝¹) ≤ ↑(Fin.castAdd (x₂.len + 1) i✝)
⊢ ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.natAdd (x₁.len + 1) i✝¹)) ≤
    ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝))

case right.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₂.len + 1)
h : ↑(Fin.natAdd (x₁.len + 1) i✝¹) ≤ ↑(Fin.natAdd (x₁.len + 1) i✝)
⊢ ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.natAdd (x₁.len + 1) i✝¹)) ≤
    ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.natAdd (x₁.len + 1) i✝))