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₂
c : AttachCells.{w, t, v, u} g f
this :
  c.m =
    c.isColimit₁.desc
      { pt := c.cofan₂.pt,
        ι :=
          (Discrete.natTrans fun (x : Discrete c.ι) ↦
              match (motive :=
                (x : Discrete c.ι) →
                  Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                    (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                x with
              | { as := i } => g (c.π i)) ≫
            c.cofan₂.ι }
rw :
  ∃ (J : Type w),
    colimitsOfShape.{v, u, w, w} (ofHoms g) (Discrete J) (Y := c.cofan₂.pt)
      (c.isColimit₁.desc
          { pt := c.cofan₂.pt,
            ι :=
              (Discrete.natTrans fun (x : Discrete c.ι) ↦
                  match (motive :=
                    (x : Discrete c.ι) →
                      Quiver.Hom.{v, u} (V := C)
                        (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                        (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                    x with
                  | { as := i } => g (c.π i)) ≫
                c.cofan₂.ι } :
        c.cofan₁.pt ⟶
          Cocone.pt (F := Discrete.functor fun (i : c.ι) ↦ A (c.π i))
            { pt := c.cofan₂.pt,
              ι :=
                (Discrete.natTrans fun (x : Discrete c.ι) ↦
                    match (motive :=
                      (x : Discrete c.ι) →
                        Quiver.Hom.{v, u} (V := C)
                          (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                          (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                      x with
                    | { as := i } => g (c.π i)) ≫
                  c.cofan₂.ι })
⊢ coproducts.{w, v, u} (ofHoms g) c.m

Tactic:
rw [this, coproducts_iff]

Premises used: CategoryTheory.MorphismProperty.coproducts_iff
-- 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₂
c : AttachCells.{w, t, v, u} g f
this :
  c.m =
    c.isColimit₁.desc
      { pt := c.cofan₂.pt,
        ι :=
          (Discrete.natTrans fun (x : Discrete c.ι) ↦
              match (motive :=
                (x : Discrete c.ι) →
                  Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                    (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                x with
              | { as := i } => g (c.π i)) ≫
            c.cofan₂.ι }
⊢ ∃ (J : Type w),
    colimitsOfShape.{v, u, w, w} (ofHoms g) (Discrete J) (Y := c.cofan₂.pt)
      (c.isColimit₁.desc
          { pt := c.cofan₂.pt,
            ι :=
              (Discrete.natTrans fun (x : Discrete c.ι) ↦
                  match (motive :=
                    (x : Discrete c.ι) →
                      Quiver.Hom.{v, u} (V := C)
                        (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                        (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                    x with
                  | { as := i } => g (c.π i)) ≫
                c.cofan₂.ι } :
        c.cofan₁.pt ⟶
          Cocone.pt (F := Discrete.functor fun (i : c.ι) ↦ A (c.π i))
            { pt := c.cofan₂.pt,
              ι :=
                (Discrete.natTrans fun (x : Discrete c.ι) ↦
                    match (motive :=
                      (x : Discrete c.ι) →
                        Quiver.Hom.{v, u} (V := C)
                          (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                          (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                      x with
                    | { as := i } => g (c.π i)) ≫
                  c.cofan₂.ι })

Tactic:
⟨c.ι, ⟨_, _, _, _, c.isColimit₁, c.isColimit₂, _, fun i ↦ ⟨_⟩⟩⟩

Premises used: HomotopicalAlgebra.AttachCells.isColimit₂, HomotopicalAlgebra.AttachCells.π, HomotopicalAlgebra.AttachCells.ι, CategoryTheory.Discrete.as, Exists.intro, CategoryTheory.MorphismProperty.ofHoms.mk, CategoryTheory.MorphismProperty.colimitsOfShape.mk, HomotopicalAlgebra.AttachCells.isColimit₁
-- 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₂
c : AttachCells.{w, t, v, u} g f
this :
  c.m =
    c.isColimit₁.desc
      { pt := c.cofan₂.pt,
        ι :=
          (Discrete.natTrans fun (x : Discrete c.ι) ↦
              match (motive :=
                (x : Discrete c.ι) →
                  Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                    (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                x with
              | { as := i } => g (c.π i)) ≫
            c.cofan₂.ι }
⊢ ∃ (J : Type w),
    colimitsOfShape.{v, u, w, w} (ofHoms g) (Discrete J) (Y := c.cofan₂.pt)
      (c.isColimit₁.desc
          { pt := c.cofan₂.pt,
            ι :=
              (Discrete.natTrans fun (x : Discrete c.ι) ↦
                  match (motive :=
                    (x : Discrete c.ι) →
                      Quiver.Hom.{v, u} (V := C)
                        (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                        (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                    x with
                  | { as := i } => g (c.π i)) ≫
                c.cofan₂.ι } :
        c.cofan₁.pt ⟶
          Cocone.pt (F := Discrete.functor fun (i : c.ι) ↦ A (c.π i))
            { pt := c.cofan₂.pt,
              ι :=
                (Discrete.natTrans fun (x : Discrete c.ι) ↦
                    match (motive :=
                      (x : Discrete c.ι) →
                        Quiver.Hom.{v, u} (V := C)
                          (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                          (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                      x with
                    | { as := i } => g (c.π i)) ≫
                  c.cofan₂.ι })

Tactic:
exact ⟨c.ι, ⟨_, _, _, _, c.isColimit₁, c.isColimit₂, _, fun i ↦ ⟨_⟩⟩⟩
-- 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₂
c : AttachCells.{w, t, v, u} g f
i : c.ι
⊢ c.cell i = c.cofan₂.inj i ≫ c.g₂

Tactic:
rfl

Premises used: HomotopicalAlgebra.AttachCells.cell, rfl
-- 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₂
c : AttachCells.{w, t, v, u} g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
apply : c.g₂ ≫ φ = c.g₂ ≫ φ'
⊢ φ = φ'

Tactic:
apply c.isPushout.hom_ext h₀

Premises used: HomotopicalAlgebra.AttachCells.isPushout, CategoryTheory.IsPushout.hom_ext
-- 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₂
c : AttachCells.{w, t, v, u} g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
h₁ : ∀ (i : c.ι), c.cofan₂.inj i ≫ c.g₂ ≫ φ = c.cofan₂.inj i ≫ c.g₂ ≫ φ'
⊢ c.g₂ ≫ φ = c.g₂ ≫ φ'

Tactic:
apply Cofan.IsColimit.hom_ext c.isColimit₂

Premises used: HomotopicalAlgebra.AttachCells.isColimit₂, CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- 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₂
c : AttachCells.{w, t, v, u} g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ ∀ (i : c.ι), c.cofan₂.inj i ≫ c.g₂ ≫ φ = c.cofan₂.inj i ≫ c.g₂ ≫ φ'

Tactic:
simpa [cell_def] using h

Premises used: HomotopicalAlgebra.AttachCells.cell_def
-- 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₂
c : AttachCells.{w, t, v, u} g f
Y₁ Y₂ : C
f' : Y₁ ⟶ Y₂
e : Arrow.mk f ≅ Arrow.mk f'
⊢ Eq (α := c.cofan₁.pt ⟶ Y₁) (c.g₁ ≫ Iso.hom (Functor.mapIso Arrow.leftFunc e))
    (Iso.hom (Iso.refl c.cofan₁.pt) ≫ c.g₁ ≫ CategoryTheory.Functor.map Arrow.leftFunc e.hom)

Tactic:
simp
-- 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₂
c : AttachCells.{w, t, v, u} g f
Y₁ Y₂ : C
f' : Y₁ ⟶ Y₂
e : Arrow.mk f ≅ Arrow.mk f'
⊢ c.m ≫ Iso.hom (Iso.refl c.cofan₂.pt) = Iso.hom (Iso.refl c.cofan₁.pt) ≫ c.m

Tactic:
simp
-- 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₂
c : AttachCells.{w, t, v, u} g f
Y₁ Y₂ : C
f' : Y₁ ⟶ Y₂
e : Arrow.mk f ≅ Arrow.mk f'
⊢ Eq (α := X₁ ⟶ Y₂) (f ≫ Iso.hom (Functor.mapIso Arrow.rightFunc e)) (Iso.hom (Functor.mapIso Arrow.leftFunc e) ≫ f')

Tactic:
simp
-- 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₂
c : AttachCells.{w, t, v, u} g f
Y₁ Y₂ : C
f' : Y₁ ⟶ Y₂
e : Arrow.mk f ≅ Arrow.mk f'
⊢ Eq (α := c.cofan₂.pt ⟶ Y₂) (c.g₂ ≫ Iso.hom (Functor.mapIso Arrow.rightFunc e))
    (Iso.hom (Iso.refl c.cofan₂.pt) ≫ c.g₂ ≫ CategoryTheory.Functor.map Arrow.rightFunc e.hom)

Tactic:
simp
-- 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₂
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.ι) ↦ A (c.π i))
  (Discrete.functor fun (i : c.ι) ↦ A' (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.ι) ↦ A (c.π i)) x)
          (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A' (a (c.π i))) x))
      x with
    | { as := i } => Functor.mapIso Arrow.leftFunc (ha (c.π i))
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.leftFunc (Iso.inv (ha (c.π i))) ≫ c.cofan₁.inj i))
        i
⊢ IsColimit.{w, v, w, u} (J := Discrete c.ι) (F := Discrete.functor fun (i : c.ι) ↦ A' ((a ∘ c.π) i))
    (Cofan.mk c.cofan₁.pt fun (i : c.ι) ↦
      CategoryTheory.Functor.map Arrow.leftFunc (Iso.inv (ha (c.π i))) ≫ c.cofan₁.inj i)

Tactic:
refine (IsColimit.precomposeHomEquiv e _).1
      (IsColimit.ofIsoColimit c.isColimit₁ (Cofan.ext (Iso.refl _) (fun i ↦ ?_)))

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, Equiv.toFun, CategoryTheory.Limits.Cofan.ext, HomotopicalAlgebra.AttachCells.isColimit₁, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- 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₂
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.ι) ↦ A (c.π i))
  (Discrete.functor fun (i : c.ι) ↦ A' (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.ι) ↦ A (c.π i)) x)
          (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A' (a (c.π i))) x))
      x with
    | { as := i } => Functor.mapIso Arrow.leftFunc (ha (c.π i))
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.leftFunc (Iso.inv (ha (c.π i))) ≫ c.cofan₁.inj i))
      i

Tactic:
simp [Cocone.precompose, e, Cofan.inj]

Premises used: CategoryTheory.Limits.Cocone.precompose, CategoryTheory.Limits.Cofan.inj
-- 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₂
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))
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
⊢ 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)

Tactic:
refine (IsColimit.precomposeHomEquiv e _).1
      (IsColimit.ofIsoColimit c.isColimit₂ (Cofan.ext (Iso.refl _) (fun i ↦ ?_)))

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, HomotopicalAlgebra.AttachCells.isColimit₂, Equiv.toFun, CategoryTheory.Limits.Cofan.ext, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- 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₂
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))
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:
simp [Cocone.precompose, e, Cofan.inj]

Premises used: CategoryTheory.Limits.Cocone.precompose, CategoryTheory.Limits.Cofan.inj
-- 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₂
mp : Nonempty (AttachCells.{w, t, v, u} g f) → (coproducts.{w, v, u} (ofHoms g)).pushouts f
mpr : (coproducts.{w, v, u} (ofHoms g)).pushouts f → Nonempty (AttachCells.{w, t, v, u} g f)
⊢ Nonempty (AttachCells.{w, t, v, u} g f) ↔ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
constructor
-- 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₂
c : AttachCells.{w, t, v, u} g f
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
c.pushouts_coproducts

Premises used: HomotopicalAlgebra.AttachCells.pushouts_coproducts
-- 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₂
c : AttachCells.{w, t, v, u} g f
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
exact c.pushouts_coproducts

Premises used: HomotopicalAlgebra.AttachCells.pushouts_coproducts
-- 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₂
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₂
⊢ ∃ (J : Type w), colimitsOfShape.{v, u, w, w} (ofHoms g) (Discrete J) m

Tactic:
rw [coproducts_iff] at h

Premises used: CategoryTheory.MorphismProperty.coproducts_iff
-- 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₂
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₂
h₁ : ∃ (J : Type w), colimitsOfShape.{v, u, w, w} (ofHoms g) (Discrete J) m
⊢ IsPushout g₁ m f g₂

Tactic:
rw [coproducts_iff] at h

Premises used: CategoryTheory.MorphismProperty.coproducts_iff
-- 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₂
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₂
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)
⊢ Nonempty (AttachCells.{w, t, v, u} g f)

Tactic:
obtain ⟨ι, ⟨F₁, F₂, c₁, c₂, h₁, h₂, φ, hφ⟩⟩ := h
-- 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)
⊢ ∀ (j : Discrete ι),
    c₁.ι.app j ≫ Iso.hom (Iso.refl c₁.pt) =
      NatTrans.app
        (Cocone.ι
          (Functor.obj (C := Cocone.{w, v, w, u} (J := Discrete ι) (C := C) (Discrete.functor fun (i : ι) ↦ A (π i)))
            (Cocone.precompose
              (Iso.hom
                (Discrete.natIso fun (x : Discrete ι) ↦
                  match (motive :=
                    (x : Discrete ι) → F₁.obj x ≅ Functor.obj.{w, v, w, u} (Discrete.functor fun (i : ι) ↦ A (π i)) x)
                    x with
                  | { as := i } => e₁ i)))
            (Cofan.mk c₁.pt fun (i : ι) ↦ (e₁ i).inv ≫ c₁.ι.app { as := i })))
        j

Tactic:
simp
-- 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)
⊢ ∀ (j : Discrete ι),
    c₂.ι.app j ≫ Iso.hom (Iso.refl c₂.pt) =
      NatTrans.app
        (Cocone.ι
          (Functor.obj (C := Cocone.{w, v, w, u} (J := Discrete ι) (C := C) (Discrete.functor fun (i : ι) ↦ B (π i)))
            (Cocone.precompose
              (Iso.hom
                (Discrete.natIso fun (x : Discrete ι) ↦
                  match (motive :=
                    (x : Discrete ι) → F₂.obj x ≅ Functor.obj.{w, v, w, u} (Discrete.functor fun (i : ι) ↦ B (π i)) x)
                    x with
                  | { as := i } => e₂ i)))
            (Cofan.mk c₂.pt fun (i : ι) ↦ (e₂ i).inv ≫ c₂.ι.app { as := i })))
        j

Tactic:
simp