awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
α' : Type t'
A' B' : α' → C
g' : (i' : α') → A' i' ⟶ B' i'
a : α → α'
ha : (i : α) → Arrow.mk (g i) ≅ Arrow.mk (X := A' (a i)) (g' (a i))
e : Iso (C := CategoryTheory.Functor.{w, v, w, u} (Discrete c.ι) C) (Discrete.functor fun (i : c.ι) ↦ B (c.π i))
  (Discrete.functor fun (i : c.ι) ↦ B' (a (c.π i))) :=
  Discrete.natIso fun (x : Discrete c.ι) ↦
    match (motive :=
      (x : Discrete c.ι) →
        Iso.{v, u} (C := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x)
          (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B' (a (c.π i))) x))
      x with
    | { as := i } => Functor.mapIso Arrow.rightFunc (ha (c.π i))
⊢ IsColimit.{w, v, w, u} (J := Discrete c.ι) (F := Discrete.functor fun (i : c.ι) ↦ B' ((a ∘ c.π) i))
    (Cofan.mk c.cofan₂.pt fun (i : c.ι) ↦
      CategoryTheory.Functor.map Arrow.rightFunc (Iso.inv (ha (c.π i))) ≫ c.cofan₂.inj i)
have refine : ∀ (i : c.ι),
  c.cofan₂.inj i ≫ Iso.hom (Iso.refl c.cofan₂.pt) =
    Cofan.inj
      ((Cocone.precompose e.hom).obj
        (Cofan.mk c.cofan₂.pt fun (i : c.ι) ↦
          CategoryTheory.Functor.map Arrow.rightFunc (Iso.inv (ha (c.π i))) ≫ c.cofan₂.inj i))
      i
Tactic: refine (IsColimit.precomposeHomEquiv e _).1
      (IsColimit.ofIsoColimit c.isColimit₂ (Cofan.ext (Iso.refl _) (fun i ↦ ?_)))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ Nonempty (AttachCells.{w, t, v, u} g f) ↔ (coproducts.{w, v, u} (ofHoms g)).pushouts f
have mp : Nonempty (AttachCells.{w, t, v, u} g f) → (coproducts.{w, v, u} (ofHoms g)).pushouts f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
mp : Nonempty (AttachCells.{w, t, v, u} g f) → (coproducts.{w, v, u} (ofHoms g)).pushouts f
⊢ Nonempty (AttachCells.{w, t, v, u} g f) ↔ (coproducts.{w, v, u} (ofHoms g)).pushouts f
have mpr : (coproducts.{w, v, u} (ofHoms g)).pushouts f → Nonempty (AttachCells.{w, t, v, u} g f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
m : Y₁ ⟶ Y₂
g₁ : Y₁ ⟶ X₁
g₂ : Y₂ ⟶ X₂
h : coproducts.{w, v, u} (ofHoms g) m
sq : IsPushout g₁ m f g₂
⊢ Nonempty (AttachCells.{w, t, v, u} g f)
have h₁ : ∃ (J : Type w), colimitsOfShape.{v, u, w, w} (ofHoms g) (Discrete J) m
Tactic: rw [coproducts_iff] at h
Cleared hypotheses: h, sq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
m : Y₁ ⟶ Y₂
g₁ : Y₁ ⟶ X₁
g₂ : Y₂ ⟶ X₂
h : ∃ (J : Type w), colimitsOfShape.{v, u, w, w} (ofHoms g) (Discrete J) m
sq : IsPushout g₁ m f g₂
⊢ Nonempty (AttachCells.{w, t, v, u} g f)
have mpr : ∀ (ι : Type w) ⦃X Y : C⦄ (F₁ F₂ : CategoryTheory.Functor.{w, v, w, u} (Discrete ι) C) (c₁ : Cocone F₁) (c₂ : Cocone F₂)
  (h₁ : IsColimit c₁) (h₂ : IsColimit c₂) (φ : F₁ ⟶ F₂) (hφ : (ofHoms g).functorCategory (Discrete ι) φ)
  (g₁ : c₁.pt ⟶ X₁) (g₂ : { pt := c₂.pt, ι := φ ≫ c₂.ι : Cocone F₁ }.pt ⟶ X₂)
  (sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂), Nonempty (AttachCells.{w, t, v, u} g f)
Tactic: obtain ⟨ι, ⟨F₁, F₂, c₁, c₂, h₁, h₂, φ, hφ⟩⟩ := h
Cleared hypotheses: Y₁, Y₂, m, g₁, g₂, h, sq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w'
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex.{u_1, w', t, v, u} (α := α) basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells (α := α)), γ.ι (α := α) ≫ φ₁ = γ.ι (α := α) ≫ φ₂
⊢ φ₁ = φ₂
have refine : ∀ (j : J),
  { pt := Y, ι := c.toTransfiniteCompositionOfShape (α := α).incl :
              Limits.Cocone c.toTransfiniteCompositionOfShape (α := α).F }.ι.app
        j ≫
      φ₁ =
    { pt := Y, ι := c.toTransfiniteCompositionOfShape (α := α).incl :
              Limits.Cocone c.toTransfiniteCompositionOfShape (α := α).F }.ι.app
        j ≫
      φ₂
Tactic: refine c.isColimit.hom_ext (fun j ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w'
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex.{u_1, w', t, v, u} (α := α) basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells (α := α)), γ.ι (α := α) ≫ φ₁ = γ.ι (α := α) ≫ φ₂
j : J
⊢ { pt := Y, ι := c.toTransfiniteCompositionOfShape (α := α).incl :
              Limits.Cocone c.toTransfiniteCompositionOfShape (α := α).F }.ι.app
        j ≫
      φ₁ =
    { pt := Y, ι := c.toTransfiniteCompositionOfShape (α := α).incl :
              Limits.Cocone c.toTransfiniteCompositionOfShape (α := α).F }.ι.app
        j ≫
      φ₂
have dsimp : c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ = c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w'
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex.{u_1, w', t, v, u} (α := α) basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells (α := α)), γ.ι (α := α) ≫ φ₁ = γ.ι (α := α) ≫ φ₂
j : J
hj : IsMin j
⊢ c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂
have isMin : ∀ (hj : IsMin.{w'} (α := J) ⊥),
  Eq (α := c.toTransfiniteCompositionOfShape (α := α).F.obj ⊥ ⟶ Z)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app ⊥ ≫ φ₁)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app ⊥ ≫ φ₂)
Tactic: obtain rfl := hj.eq_bot
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w'
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex.{u_1, w', t, v, u} (α := α) basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells (α := α)), γ.ι (α := α) ≫ φ₁ = γ.ι (α := α) ≫ φ₂
j : J
hj : ¬IsMax j
hj' :
  c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂
⊢ Eq (α := c.toTransfiniteCompositionOfShape (α := α).F.obj (Order.succ j) ⟶ Z)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₁)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₂)
have succ : CategoryStruct.comp (Y := c.toTransfiniteCompositionOfShape (α := α).F.obj (Order.succ j))
    (c.toTransfiniteCompositionOfShape (α := α).F.map (homOfLE sorry))
    (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₁) =
  CategoryStruct.comp (Y := c.toTransfiniteCompositionOfShape (α := α).F.obj (Order.succ j))
    (c.toTransfiniteCompositionOfShape (α := α).F.map (homOfLE sorry))
    (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₂)
Tactic: apply (c.attachCells j hj).hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w'
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex.{u_1, w', t, v, u} (α := α) basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells (α := α)), γ.ι (α := α) ≫ φ₁ = γ.ι (α := α) ≫ φ₂
j : J
hj : ¬IsMax j
hj' :
  c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂
succ :
  CategoryStruct.comp (Y := c.toTransfiniteCompositionOfShape (α := α).F.obj (Order.succ j))
      (c.toTransfiniteCompositionOfShape (α := α).F.map (homOfLE ⋯))
      (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₁) =
    CategoryStruct.comp (Y := c.toTransfiniteCompositionOfShape (α := α).F.obj (Order.succ j))
      (c.toTransfiniteCompositionOfShape (α := α).F.map (homOfLE ⋯))
      (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₂)
⊢ Eq (α := c.toTransfiniteCompositionOfShape (α := α).F.obj (Order.succ j) ⟶ Z)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₁)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₂)
have succ₁ : ∀ (i : (c.attachCells (α := α) j hj).ι),
  (c.attachCells (α := α) j hj).cell i ≫ c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₁ =
    (c.attachCells (α := α) j hj).cell i ≫ c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₂
Tactic: apply (c.attachCells j hj).hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w'
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex.{u_1, w', t, v, u} (α := α) basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells (α := α)), γ.ι (α := α) ≫ φ₁ = γ.ι (α := α) ≫ φ₂
j : J
⊢ c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂
have isMin : ∀ (j : J) (hj : IsMin j),
  c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    obtain rfl := hj.eq_bot
    simpa [← cancel_epi c.isoBot.inv] using h₀
  | succ j hj hj' =>
    apply (c.attachCells j hj).hom_ext
    · simpa using hj'
    · intro i
      simpa only [Category.assoc, Cells.ι] using h ({ hj := hj, k := i, .. })
  | isSuccLimit j hj hj' =>
    exact (c.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
      (fun ⟨k, hk⟩ ↦ by simpa using hj' k hk)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w'
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex.{u_1, w', t, v, u} (α := α) basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells (α := α)), γ.ι (α := α) ≫ φ₁ = γ.ι (α := α) ≫ φ₂
j : J
isMin :
  ∀ (j : J) (hj : IsMin j),
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
      c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂
⊢ c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂
have succ : ∀ (j : J) (hj : ¬IsMax j)
  (hj' :
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
      c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂),
  Eq (α := c.toTransfiniteCompositionOfShape (α := α).F.obj (Order.succ j) ⟶ Z)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₁)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₂)
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    obtain rfl := hj.eq_bot
    simpa [← cancel_epi c.isoBot.inv] using h₀
  | succ j hj hj' =>
    apply (c.attachCells j hj).hom_ext
    · simpa using hj'
    · intro i
      simpa only [Category.assoc, Cells.ι] using h ({ hj := hj, k := i, .. })
  | isSuccLimit j hj hj' =>
    exact (c.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
      (fun ⟨k, hk⟩ ↦ by simpa using hj' k hk)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w'
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex.{u_1, w', t, v, u} (α := α) basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells (α := α)), γ.ι (α := α) ≫ φ₁ = γ.ι (α := α) ≫ φ₂
j : J
isMin :
  ∀ (j : J) (hj : IsMin j),
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
      c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂
succ :
  ∀ (j : J) (hj : ¬IsMax j)
    (hj' :
      c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
        c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂),
    Eq (α := c.toTransfiniteCompositionOfShape (α := α).F.obj (Order.succ j) ⟶ Z)
      (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₁)
      (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₂)
⊢ c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂
have isSuccLimit : ∀ (j : J) (hj : Order.IsSuccLimit j)
  (hj' :
    ∀ b < j,
      c.toTransfiniteCompositionOfShape (α := α).incl.app b ≫ φ₁ =
        c.toTransfiniteCompositionOfShape (α := α).incl.app b ≫ φ₂),
  c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    obtain rfl := hj.eq_bot
    simpa [← cancel_epi c.isoBot.inv] using h₀
  | succ j hj hj' =>
    apply (c.attachCells j hj).hom_ext
    · simpa using hj'
    · intro i
      simpa only [Category.assoc, Cells.ι] using h ({ hj := hj, k := i, .. })
  | isSuccLimit j hj hj' =>
    exact (c.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
      (fun ⟨k, hk⟩ ↦ by simpa using hj' k hk)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (hypothesis)
Goal:
x y : SimplexCategory
h : WithInitial.of x = WithInitial.of y
⊢ x.len = y.len
have h₁ : x = y
Tactic: injection h with h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x y : SimplexCategory
h : x = y
⊢ x.len = y.len
have rw : y.len = y.len
Tactic: rw [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 j : Fin (x₁.len + 1 + (x₂.len + 1))
h : i ≤ j
⊢ 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))))
      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))))
      j)
have left : ∀ (i : Fin (x₁.len + 1)) (h : Fin.castAdd (x₂.len + 1) i ≤ j),
  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))))
      j)
Tactic: cases i using Fin.addCases
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
j : Fin (x₁.len + 1 + (x₂.len + 1))
i : Fin (x₁.len + 1)
h : Fin.castAdd (x₂.len + 1) i ≤ j
⊢ 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))))
      j)
have left : ∀ (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))
Tactic: cases j using Fin.addCases
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
j : Fin (x₁.len + 1 + (x₂.len + 1))
i : Fin (x₂.len + 1)
h : Fin.natAdd (x₁.len + 1) i ≤ j
⊢ 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))))
      j)
have right : ∀ (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))
Tactic: cases j using Fin.addCases
Cleared hypotheses: j, h