-- Mathlib/AlgebraicTopology/RelativeCellComplex/AttachCells.lean
lemma nonempty_attachCells_iff :
    Nonempty (AttachCells.{w} g f) ↔ (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₂
⊢ Nonempty (AttachCells g f) ↔ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
constructor

Result:
case mp
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 g f) → (coproducts.{w, v, u} (ofHoms g)).pushouts f

case mpr
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₂
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f → Nonempty (AttachCells g f)

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro.mk
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₂ : 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₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
π : ι → α := fun i => ⋯.choose
e : (i : ι) → Arrow.mk (φ.app { as := i }) ≅ Arrow.mk (g (π i)) := fun i => eqToIso ⋯
e₁ : (i : ι) → F₁.obj { as := i } ≅ A (π i) := fun i => Arrow.leftFunc.mapIso (e i)
e₂ : (i : ι) → F₂.obj { as := i } ≅ B (π i) := fun i => Arrow.rightFunc.mapIso (e i)
⊢ Nonempty (AttachCells 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₁ (Cocones.ext (Iso.refl _) (by simp)))
  isColimit₂ :=
    (IsColimit.precomposeHomEquiv (Discrete.natIso (fun ⟨i⟩ ↦ e₂ i)) _).1
      (IsColimit.ofIsoColimit h₂ (Cocones.ext (Iso.refl _) (by simp)))
  hm i := by simp [e₁, e₂]
  isPushout := sq }⟩

Result:
no goals

Proof state:
case mp.intro
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:
exact c.pushouts_coproducts

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro.intro
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 g f)

Tactic:
rw [coproducts_iff] at h

Result:
case mpr.intro.intro.intro.intro.intro.intro
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, (ofHoms g).colimitsOfShape (Discrete J) m
sq : IsPushout g₁ m f g₂
⊢ Nonempty (AttachCells g 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₂
ι : Type w
X Y : C
F₁ F₂ : 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₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
π : ι → α := fun i => ⋯.choose
e : (i : ι) → Arrow.mk (φ.app { as := i }) ≅ Arrow.mk (g (π i)) := fun i => eqToIso ⋯
e₁ : (i : ι) → F₁.obj { as := i } ≅ A (π i) := fun i => Arrow.leftFunc.mapIso (e i)
e₂ : (i : ι) → F₂.obj { as := i } ≅ B (π i) := fun i => Arrow.rightFunc.mapIso (e i)
⊢ ∀ (j : Discrete ι),
    c₁.ι.app j ≫ (Iso.refl c₁.pt).hom =
      ((Cocones.precompose
                  (Discrete.natIso fun x =>
                      match x with
                      | { as := i } => e₁ i).hom).obj
              (Cofan.mk c₁.pt fun i => (e₁ i).inv ≫ c₁.ι.app { as := i })).ι.app
        j

Tactic:
simp

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₂
ι : Type w
X Y : C
F₁ F₂ : 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₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
π : ι → α := fun i => ⋯.choose
e : (i : ι) → Arrow.mk (φ.app { as := i }) ≅ Arrow.mk (g (π i)) := fun i => eqToIso ⋯
e₁ : (i : ι) → F₁.obj { as := i } ≅ A (π i) := fun i => Arrow.leftFunc.mapIso (e i)
e₂ : (i : ι) → F₂.obj { as := i } ≅ B (π i) := fun i => Arrow.rightFunc.mapIso (e i)
i : ι
⊢ (Cofan.mk c₁.pt fun i => (e₁ i).inv ≫ c₁.ι.app { as := i }).inj i ≫ h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι } =
    g (π i) ≫ (Cofan.mk c₂.pt fun i => (e₂ i).inv ≫ c₂.ι.app { as := i }).inj i

Tactic:
simp [e₁, e₂]

Result:
no goals

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

Tactic:
rintro ⟨Y₁, Y₂, m, g₁, g₂, h, sq⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro
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 g 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₂
ι : Type w
X Y : C
F₁ F₂ : 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₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
π : ι → α := fun i => ⋯.choose
e : (i : ι) → Arrow.mk (φ.app { as := i }) ≅ Arrow.mk (g (π i)) := fun i => eqToIso ⋯
e₁ : (i : ι) → F₁.obj { as := i } ≅ A (π i) := fun i => Arrow.leftFunc.mapIso (e i)
e₂ : (i : ι) → F₂.obj { as := i } ≅ B (π i) := fun i => Arrow.rightFunc.mapIso (e i)
⊢ ∀ (j : Discrete ι),
    c₂.ι.app j ≫ (Iso.refl c₂.pt).hom =
      ((Cocones.precompose
                  (Discrete.natIso fun x =>
                      match x with
                      | { as := i } => e₂ i).hom).obj
              (Cofan.mk c₂.pt fun i => (e₂ i).inv ≫ c₂.ι.app { as := i })).ι.app
        j

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro.mk
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₂ : 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₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
π : ι → α := fun i => ⋯.choose
⊢ Nonempty (AttachCells g f)

Tactic:
let e (i : ι) : Arrow.mk (φ.app ⟨i⟩) ≅ Arrow.mk (g (π i)) :=
  eqToIso (((ofHoms_iff _ _).1 (hφ ⟨i⟩)).choose_spec)

Result:
case mpr.intro.intro.intro.intro.intro.intro.intro.mk
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₂ : 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₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
π : ι → α := fun i => ⋯.choose
e : (i : ι) → Arrow.mk (φ.app { as := i }) ≅ Arrow.mk (g (π i)) := fun i => eqToIso ⋯
⊢ Nonempty (AttachCells g f)