-- Mathlib/AlgebraicTopology/RelativeCellComplex/AttachCells.lean
lemma pushouts_coproducts : (coproducts.{w} (ofHoms g)).pushouts f

Proof state:
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 g f
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
refine ⟨_, _, _, _, _, ?_, c.isPushout⟩

Result:
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 g f
⊢ coproducts.{w, v, u} (ofHoms g) c.m

Proof state:
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 g f
x✝ : Discrete c.ι
i : c.ι
⊢ c.cofan₁.ι.app { as := i } ≫ c.m =
    { pt := c.cofan₂.pt,
            ι :=
              (Discrete.natTrans fun x =>
                  match x with
                  | { as := i } => g (c.π i)) ≫
                c.cofan₂.ι }.ι.app
      { as := i }

Tactic:
exact c.hm i

Result:
no goals

Proof state:
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 g f
this :
  c.m =
    c.isColimit₁.desc
      { pt := c.cofan₂.pt,
        ι :=
          (Discrete.natTrans fun x =>
              match x with
              | { as := i } => g (c.π i)) ≫
            c.cofan₂.ι }
⊢ coproducts.{w, v, u} (ofHoms g) c.m

Tactic:
rw [this, coproducts_iff]

Result:
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 g f
this :
  c.m =
    c.isColimit₁.desc
      { pt := c.cofan₂.pt,
        ι :=
          (Discrete.natTrans fun x =>
              match x with
              | { as := i } => g (c.π i)) ≫
            c.cofan₂.ι }
⊢ ∃ J,
    (ofHoms g).colimitsOfShape (Discrete J)
      (c.isColimit₁.desc
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun x =>
                match x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι })

Proof state:
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 g f
x✝ : Discrete c.ι
i : c.ι
⊢ (Discrete.functor fun i => A (c.π i)).obj { as := i } ⟶ (Discrete.functor fun i => B (c.π i)).obj { as := i }

Tactic:
exact g (c.π i)

Result:
no goals

Proof state:
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 g f
⊢ coproducts.{w, v, u} (ofHoms g) c.m

Tactic:
have : c.m = c.isColimit₁.desc
    (Cocone.mk _ (Discrete.natTrans (fun ⟨i⟩ ↦ by exact g (c.π i)) ≫ c.cofan₂.ι)) :=
  c.isColimit₁.hom_ext (fun ⟨i⟩ ↦ by rw [IsColimit.fac]; exact c.hm i)

Result:
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 g f
this :
  c.m =
    c.isColimit₁.desc
      { pt := c.cofan₂.pt,
        ι :=
          (Discrete.natTrans fun x =>
              match x with
              | { as := i } => g (c.π i)) ≫
            c.cofan₂.ι }
⊢ coproducts.{w, v, u} (ofHoms g) c.m

Proof state:
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 g f
this :
  c.m =
    c.isColimit₁.desc
      { pt := c.cofan₂.pt,
        ι :=
          (Discrete.natTrans fun x =>
              match x with
              | { as := i } => g (c.π i)) ≫
            c.cofan₂.ι }
⊢ ∃ J,
    (ofHoms g).colimitsOfShape (Discrete J)
      (c.isColimit₁.desc
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun x =>
                match x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι })

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

Result:
no goals

Proof state:
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 g f
x✝ : Discrete c.ι
i : c.ι
⊢ c.cofan₁.ι.app { as := i } ≫ c.m =
    c.cofan₁.ι.app { as := i } ≫
      c.isColimit₁.desc
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun x =>
                match x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι }

Tactic:
rw [IsColimit.fac]

Result:
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 g f
x✝ : Discrete c.ι
i : c.ι
⊢ c.cofan₁.ι.app { as := i } ≫ c.m =
    { pt := c.cofan₂.pt,
            ι :=
              (Discrete.natTrans fun x =>
                  match x with
                  | { as := i } => g (c.π i)) ≫
                c.cofan₂.ι }.ι.app
      { as := i }