awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
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₂
ι : 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₂
π : (i : ι) → α :=
  fun (i : ι) ↦
    Exists.choose (p := fun (i_1 : α) ↦
      Arrow.mk (X := F₁.obj { as := i : Discrete ι }) (φ.app { as := i : Discrete ι }) = Arrow.mk (g i_1)) ⋯
e : (i : ι) →
  Arrow.mk (X := F₁.obj { as := i : Discrete ι }) (φ.app { as := i : Discrete ι }) ≅
    Arrow.mk (X := A (π i)) (g (π i)) :=
  fun (i : ι) ↦ eqToIso ⋯
e₁ : (i : ι) → F₁.obj { as := i : Discrete ι } ≅ A (π i) := fun (i : ι) ↦ Functor.mapIso Arrow.leftFunc (e i)
e₂ : (i : ι) → F₂.obj { as := i : Discrete ι } ≅ B (π i) := fun (i : ι) ↦ Functor.mapIso Arrow.rightFunc (e i)
i : ι
⊢ Eq.{v + 1} (α :=
    A (π i) ⟶
      Cocone.pt.{w, v, w, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ B (π i))
        (Cofan.mk c₂.pt fun (i : ι) ↦ (e₂ i).inv ≫ c₂.ι.app { as := i }))
    (CategoryStruct.comp (Y :=
        Cocone.pt.{w, v, w, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ A (π i))
          (Cofan.mk c₁.pt fun (i : ι) ↦ (e₁ i).inv ≫ c₁.ι.app { as := i }))
        (Cofan.inj.{w, v, u} (f := fun (i : ι) ↦ A (π i))
          (Cofan.mk c₁.pt fun (i : ι) ↦ (e₁ i).inv ≫ c₁.ι.app { as := i }) i)
        (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) :
      A (π i) ⟶
        Cocone.pt.{w, v, w, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ B (π i))
          (Cofan.mk c₂.pt fun (i : ι) ↦ (e₂ i).inv ≫ c₂.ι.app { as := i }))
    (g (π i) ≫
        Cofan.inj.{w, v, u} (f := fun (i : ι) ↦ B (π i))
          (Cofan.mk c₂.pt fun (i : ι) ↦ (e₂ i).inv ≫ c₂.ι.app { as := i }) i :
      A (π i) ⟶
        Cocone.pt.{w, v, w, u} (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ B (π i))
          (Cofan.mk c₂.pt fun (i : ι) ↦ (e₂ i).inv ≫ c₂.ι.app { as := i }))

Tactic:
simp [e₁, e₂]
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
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₂
ι : 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₂
π : (i : ι) → α :=
  fun (i : ι) ↦
    Exists.choose (p := fun (i_1 : α) ↦
      Arrow.mk (X := F₁.obj { as := i : Discrete ι }) (φ.app { as := i : Discrete ι }) = Arrow.mk (g i_1)) ⋯
e : (i : ι) →
  Arrow.mk (X := F₁.obj { as := i : Discrete ι }) (φ.app { as := i : Discrete ι }) ≅
    Arrow.mk (X := A (π i)) (g (π i)) :=
  fun (i : ι) ↦ eqToIso ⋯
e₁ : (i : ι) → F₁.obj { as := i : Discrete ι } ≅ A (π i) := fun (i : ι) ↦ Functor.mapIso Arrow.leftFunc (e i)
e₂ : (i : ι) → F₂.obj { as := i : Discrete ι } ≅ B (π i) := fun (i : ι) ↦ Functor.mapIso Arrow.rightFunc (e i)
⊢ Nonempty (AttachCells.{w, t, v, u} g f)

Tactic:
exact ⟨{
      ι := ι
      π := π
      cofan₁ := Cofan.mk c₁.pt (fun i ↦ (e₁ i).inv ≫ c₁.ι.app ⟨i⟩)
      cofan₂ := Cofan.mk c₂.pt (fun i ↦ (e₂ i).inv ≫ c₂.ι.app ⟨i⟩)
      isColimit₁ :=
        (IsColimit.precomposeHomEquiv (Discrete.natIso (fun ⟨i⟩ ↦ e₁ i)) _).1
          (IsColimit.ofIsoColimit h₁ (Cocone.ext (Iso.refl _) (by simp)))
      isColimit₂ :=
        (IsColimit.precomposeHomEquiv (Discrete.natIso (fun ⟨i⟩ ↦ e₂ i)) _).1
          (IsColimit.ofIsoColimit h₂ (Cocone.ext (Iso.refl _) (by simp)))
      hm i := by simp [e₁, e₂]
      isPushout := sq, .. }⟩
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
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 (α := α)), γ.ι (α := α) ≫ φ₁ = γ.ι (α := α) ≫ φ₂
⊢ φ₁ = φ₂

Tactic:
c.isColimit.hom_ext (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.TransfiniteCompositionOfShape.isColimit, HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
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 (α := α)), γ.ι (α := α) ≫ φ₁ = γ.ι (α := α) ≫ φ₂
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 ↦ ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.TransfiniteCompositionOfShape.isColimit, HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
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
dsimp :
  c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
    c.toTransfiniteCompositionOfShape (α := α).incl.app 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:
dsimp
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
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
isMin :
  ∀ (hj : IsMin.{w'} (α := J) ⊥),
    Eq (α := c.toTransfiniteCompositionOfShape (α := α).F.obj ⊥ ⟶ Z)
      (c.toTransfiniteCompositionOfShape (α := α).incl.app ⊥ ≫ φ₁)
      (c.toTransfiniteCompositionOfShape (α := α).incl.app ⊥ ≫ φ₂)
⊢ c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁ =
    c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂

Tactic:
obtain rfl := hj.eq_bot

Premises used: IsMin.eq_bot, rfl
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
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 (α := α)), γ.ι (α := α) ≫ φ₁ = γ.ι (α := α) ≫ φ₂
hj : IsMin.{w'} (α := J) ⊥
⊢ Eq (α := c.toTransfiniteCompositionOfShape (α := α).F.obj ⊥ ⟶ Z)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app ⊥ ≫ φ₁)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app ⊥ ≫ φ₂)

Tactic:
simpa [← cancel_epi c.isoBot.inv] using h₀

Premises used: CategoryTheory.TransfiniteCompositionOfShape.isoBot, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
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) ≫ φ₂)
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) ≫ φ₂
⊢ Eq (α := c.toTransfiniteCompositionOfShape (α := α).F.obj (Order.succ j) ⟶ Z)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₁)
    (c.toTransfiniteCompositionOfShape (α := α).incl.app (Order.succ j) ≫ φ₂)

Tactic:
apply (c.attachCells j hj).hom_ext

Premises used: HomotopicalAlgebra.RelativeCellComplex.attachCells, HomotopicalAlgebra.AttachCells.hom_ext
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
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 ≫ φ₂
⊢ 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) ≫ φ₂)

Tactic:
simpa using hj'
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
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 ≫ φ₂
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:
simpa only [Category.assoc, Cells.ι] using h ({ hj := hj, k := i, .. })

Premises used: HomotopicalAlgebra.RelativeCellComplex.Cells.mk, CategoryTheory.Category.assoc, HomotopicalAlgebra.RelativeCellComplex.Cells.ι
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
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 : Order.IsSuccLimit j
hj' :
  ∀ b < j,
    c.toTransfiniteCompositionOfShape (α := α).incl.app b ≫ φ₁ =
      c.toTransfiniteCompositionOfShape (α := α).incl.app b ≫ φ₂
x : (↑(Set.Iio j) : Type w')
k : J
hk : k ∈ Set.Iio j
⊢ Eq (α :=
    Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w')) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w')) → J))
            ⋯ ⋙
          c.toTransfiniteCompositionOfShape (α := α).F)
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) k hk) ⟶
      Z)
    (NatTrans.app
        (Limits.Cocone.ι (PrincipalSeg.cocone (Set.principalSegIio j) c.toTransfiniteCompositionOfShape (α := α).F))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) k hk) ≫
      c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₁)
    (NatTrans.app
        (Limits.Cocone.ι (PrincipalSeg.cocone (Set.principalSegIio j) c.toTransfiniteCompositionOfShape (α := α).F))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) k hk) ≫
      c.toTransfiniteCompositionOfShape (α := α).incl.app j ≫ φ₂)

Tactic:
simpa using hj' k hk
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
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 : 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:
exact (c.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
      (fun ⟨k, hk⟩ ↦ by simpa using hj' k hk)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Functor.isColimitOfIsWellOrderContinuous, CategoryTheory.TransfiniteCompositionOfShape.F, CategoryTheory.Limits.Cocone.ι, _private.0.HomotopicalAlgebra.RelativeCellComplex.hom_ext.match_2, CategoryTheory.CategoryStruct.comp, Set.principalSegIio, Eq, PrincipalSeg.cocone, HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
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) ≫ φ₂)
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 ≫ φ₂
⊢ 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)

Premises used: CategoryTheory.Category.assoc, HomotopicalAlgebra.RelativeCellComplex.Cells.ι, CategoryTheory.TransfiniteCompositionOfShape.isoBot, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ inclusion.Full

Tactic:
inferInstanceAs WithInitial.incl.Full

Premises used: _private.0.AugmentedSimplexCategory.instFullSimplexCategoryInclusion._proof_1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ inclusion.Faithful

Tactic:
inferInstanceAs WithInitial.incl.Faithful

Premises used: _private.0.AugmentedSimplexCategory.instFaithfulSimplexCategoryInclusion._proof_1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ Limits.HasInitial AugmentedSimplexCategory

Tactic:
inferInstanceAs <| Limits.HasInitial <| WithInitial _

Premises used: _private.0.AugmentedSimplexCategory.instHasInitial._proof_1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : SimplexCategory
h : WithInitial.of x = WithInitial.of y
⊢ x = y

Tactic:
injection h with h
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : SimplexCategory
h : x = y
rw rw₁ : y.len = y.len
⊢ x.len = y.len

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
x y : SimplexCategory
h : WithInitial.of x = WithInitial.of y
⊢ x = y

Tactic:
injection h
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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)
⊢ (↑(Fin.castAdd (x₂.len + 1) i) : ℕ) ≤ (↑(Fin.castAdd (x₂.len + 1) i_1) : ℕ)

Tactic:
rw [Fin.le_def] at h ⊢

Premises used: Fin.le_def
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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
⊢ (↑(Fin.castAdd (x₂.len + 1) i) : ℕ) ≤ (↑(Fin.natAdd (x₁.len + 1) i_1) : ℕ)

Tactic:
rw [Fin.le_def] at h ⊢

Premises used: Fin.le_def
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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
⊢ (↑(Fin.natAdd (x₁.len + 1) i) : ℕ) ≤ (↑(Fin.castAdd (x₂.len + 1) i_1) : ℕ)

Tactic:
rw [Fin.le_def] at h ⊢

Premises used: Fin.le_def
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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)
⊢ (↑(Fin.natAdd (x₁.len + 1) i) : ℕ) ≤ (↑(Fin.natAdd (x₁.len + 1) i_1) : ℕ)

Tactic:
rw [Fin.le_def] at h ⊢

Premises used: Fin.le_def
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
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) : ℕ)
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))
⊢ (↑((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:
simp at h ⊢