awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : Q.LeftHomotopy f g
dsimp : Q.i₁.hom ≫ h.h.hom = g.hom
⊢ (Q.map P.ι).i₁ ≫ h.h.hom = g.hom

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : Q.LeftHomotopy f g
⊢ Q.i₁.hom ≫ h.h.hom = g.hom

Tactic:
simp only [← h.h₁, ObjectProperty.FullSubcategory.comp_hom]

Premises used: HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁, CategoryTheory.ObjectProperty.FullSubcategory.comp_hom
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
h₁ : (Q.i₀ ≫ ObjectProperty.homMk (P := P) h.h).hom = f.hom
⊢ Q.i₀ ≫ ObjectProperty.homMk (P := P) h.h = f

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ (Q.i₀ ≫ ObjectProperty.homMk (P := P) h.h).hom = f.hom

Tactic:
h.h₀

Premises used: HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ (Q.i₀ ≫ ObjectProperty.homMk (P := P) h.h).hom = f.hom

Tactic:
exact h.h₀

Premises used: HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
h₁ : (Q.i₁ ≫ ObjectProperty.homMk (P := P) h.h).hom = g.hom
⊢ Q.i₁ ≫ ObjectProperty.homMk (P := P) h.h = g

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ (Q.i₁ ≫ ObjectProperty.homMk (P := P) h.h).hom = g.hom

Tactic:
h.h₁

Premises used: HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ (Q.i₁ ≫ ObjectProperty.homMk (P := P) h.h).hom = g.hom

Tactic:
exact h.h₁

Premises used: HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} X
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_3 : MorphismProperty.ContainsIdentities.{v, u} (weakEquivalences C)
f₀ f₁ : X ⟶ Y
h : P.LeftHomotopy f₀ f₁
mk : ∀ (h : P.I ⟶ Y), P.i₀ ≫ h = f₀ → P.i₁ ≫ h = f₁ → (WeakEquivalence f₀ ↔ WeakEquivalence f₁)
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁

Tactic:
induction h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} X
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_3 : MorphismProperty.ContainsIdentities.{v, u} (weakEquivalences C)
f₀ f₁ : X ⟶ Y
h : P.I ⟶ Y
h₀ : P.i₀ ≫ h = f₀
h₁ : P.i₁ ≫ h = f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁

Tactic:
grind [weakEquivalence_precomp_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_precomp_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : Cylinder.{v, u} X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} X X) P.i :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.i
rw :
  cofibrations C (X := coprod.{v, u} X X)
    (toPrecylinder
        { I := d.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₀ := coprod.inl ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₁ := coprod.inr ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          π := d.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
          weakEquivalence_π := ⋯ }).i
⊢ Cofibration (X := coprod.{v, u} X X)
    (toPrecylinder
        { I := d.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₀ := coprod.inl ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₁ := coprod.inr ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          π := d.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
          weakEquivalence_π := ⋯ }).i

Tactic:
rw [cofibration_iff]

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : Cylinder.{v, u} X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} X X) P.i :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.i
⊢ cofibrations C (d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
d.hi

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.hi
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : Cylinder.{v, u} X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} X X) P.i :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.i
h₁ :
  (toPrecylinder
        { I := d.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₀ := coprod.inl ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₁ := coprod.inr ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          π := d.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
          weakEquivalence_π := ⋯ }).i =
    d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)
⊢ cofibrations C (X := coprod.{v, u} X X)
    (toPrecylinder
        { I := d.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₀ := coprod.inl ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₁ := coprod.inr ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          π := d.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
          weakEquivalence_π := ⋯ }).i

Tactic:
convert! d.hi

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.hi
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : Cylinder.{v, u} X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} X X) P.i :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.i
⊢ (toPrecylinder
        { I := d.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₀ := coprod.inl ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₁ := coprod.inr ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          π := d.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
          weakEquivalence_π := ⋯ }).i =
    d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : Cylinder.{v, u} X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} X X) P.i :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.i
⊢ ∃ (P' : Cylinder.{v, u} X), P'.IsGood ∧ Nonempty.{v + 1} (P'.LeftHomotopy f g)

Tactic:
exact
   ⟨{ I := d.Z
      i₀ := coprod.inl ≫ d.i
      i₁ := coprod.inr ≫ d.i
      π := d.p ≫ P.π }, ⟨by
        rw [cofibration_iff]
        convert! d.hi
        aesop⟩, ⟨{ h := d.p ≫ h.h }⟩⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A E B : C
P : Cylinder.{v, u} A
f₀ f₁ : A ⟶ B
inst_2 : IsCofibrant.{v, u} A
inst_3 : P.IsGood
h : P.LeftHomotopy f₀ f₁
p : E ⟶ B
inst_4 : Fibration p
l₀ : A ⟶ E
hl₀ : l₀ ≫ p = f₀
sq : CommSq l₀ P.i₀ p h.h
⊢ Precylinder.LeftHomotopy.h (f := l₀) { h := sq.lift, h₀ := ⋯, h₁ := ⋯ : P.LeftHomotopy l₀ (P.i₁ ≫ sq.lift) } ≫ p = h.h

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
⊢ LeftHomotopyRel f g

Tactic:
⟨_, ⟨h⟩⟩

Premises used: HomotopicalAlgebra.LeftHomotopyRel, Nonempty.intro, Exists.intro
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
rw : L.map f = L.map g
⊢ AreEqualizedByLocalization (weakEquivalences C) f g

Tactic:
rw [areEqualizedByLocalization_iff L]

Premises used: CategoryTheory.areEqualizedByLocalization_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
this : L.map P.i₀ = L.map P.i₁
⊢ L.map f = L.map g

Tactic:
simp only [← h.h₀, ← h.h₁, L.map_comp, this]

Premises used: HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀, HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
suffices : L.map P.i₀ = L.map P.i₁
⊢ L.map f = L.map g

Tactic:
suffices L.map P.i₀ = L.map P.i₁ by
    simp only [← h.h₀, ← h.h₁, L.map_comp, this]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
rw : WeakEquivalence P.π
⊢ weakEquivalences C P.π

Tactic:
rw [← weakEquivalence_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
⊢ WeakEquivalence P.π

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
⊢ IsIso (L.map P.π)

Tactic:
have := Localization.inverts L (weakEquivalences C) P.π (by
    rw [← weakEquivalence_iff]
    infer_instance)
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
this : IsIso (L.map P.π)
⊢ L.map P.i₀ = L.map P.i₁

Tactic:
simp [← cancel_mono (L.map P.π), ← L.map_comp, P.i₀_π, P.i₁_π]

Premises used: HomotopicalAlgebra.Precylinder.π, HomotopicalAlgebra.Precylinder.i₀_π, CategoryTheory.cancel_mono, HomotopicalAlgebra.Cylinder.toPrecylinder, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, HomotopicalAlgebra.Precylinder.i₁_π
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f : X ⟶ Y
⊢ LeftHomotopyRel f f

Tactic:
⟨Classical.arbitrary _, ⟨Cylinder.LeftHomotopy.refl _ _⟩⟩

Premises used: HomotopicalAlgebra.LeftHomotopyRel, Nonempty.intro, Exists.intro, Classical.arbitrary, HomotopicalAlgebra.Cylinder.LeftHomotopy.refl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
h : LeftHomotopyRel f g
Z : C
p : Y ⟶ Z
obtain : ∀ (P : Cylinder.{v, u} X) (h : P.LeftHomotopy f g), LeftHomotopyRel (f ≫ p) (g ≫ p)
⊢ LeftHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
obtain ⟨P, ⟨h⟩⟩ := h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
Z : C
p : Y ⟶ Z
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
⊢ LeftHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
(h.postcomp p).leftHomotopyRel

Premises used: HomotopicalAlgebra.Cylinder.LeftHomotopy.leftHomotopyRel, HomotopicalAlgebra.Cylinder.LeftHomotopy.postcomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
Z : C
p : Y ⟶ Z
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
⊢ LeftHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
exact (h.postcomp p).leftHomotopyRel

Premises used: HomotopicalAlgebra.Cylinder.LeftHomotopy.leftHomotopyRel, HomotopicalAlgebra.Cylinder.LeftHomotopy.postcomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
h : LeftHomotopyRel f g
obtain :
  ∀ (P : Cylinder.{v, u} X) (h : P.LeftHomotopy f g),
    ∃ (P : Cylinder.{v, u} X), P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)
⊢ ∃ (P : Cylinder.{v, u} X), P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)

Tactic:
obtain ⟨P, ⟨h⟩⟩ := h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
⊢ ∃ (P : Cylinder.{v, u} X), P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)

Tactic:
h.exists_good_cylinder

Premises used: HomotopicalAlgebra.Cylinder.LeftHomotopy.exists_good_cylinder
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
⊢ ∃ (P : Cylinder.{v, u} X), P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)

Tactic:
exact h.exists_good_cylinder

Premises used: HomotopicalAlgebra.Cylinder.LeftHomotopy.exists_good_cylinder
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h : LeftHomotopyRel f g
obtain :
  ∀ (P : Cylinder.{v, u} X),
    P.IsGood →
      ∀ (h : P.LeftHomotopy f g), ∃ (P : Cylinder.{v, u} X), P.IsVeryGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)
⊢ ∃ (P : Cylinder.{v, u} X), P.IsVeryGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)

Tactic:
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_cylinder

Premises used: HomotopicalAlgebra.LeftHomotopyRel.exists_good_cylinder
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : LeftHomotopyRel f g
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy f g
fac : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) P.π :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.π
P' : Cylinder.{v, u} X :=
  { I := fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₀ := P.i₀ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₁ := P.i₁ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    π := fac.p (W₁ := trivialCofibrations C) (W₂ := fibrations C), i₀_π := ⋯, i₁_π := ⋯, weakEquivalence_π := ⋯ }
rw : Cofibration (X := coprod.{v, u} X X) (P.i ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ Cofibration (X := coprod.{v, u} X X) P'.i

Tactic:
rw [show P'.i = P.i ≫ fac.i by cat_disch]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : LeftHomotopyRel f g
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy f g
fac : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) P.π :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.π
P' : Cylinder.{v, u} X :=
  { I := fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₀ := P.i₀ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₁ := P.i₁ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    π := fac.p (W₁ := trivialCofibrations C) (W₂ := fibrations C), i₀_π := ⋯, i₁_π := ⋯, weakEquivalence_π := ⋯ }
⊢ Cofibration (X := coprod.{v, u} X X) (P.i ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : LeftHomotopyRel f g
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy f g
fac : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) P.π :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.π
P' : Cylinder.{v, u} X :=
  { I := fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₀ := P.i₀ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₁ := P.i₁ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    π := fac.p (W₁ := trivialCofibrations C) (W₂ := fibrations C), i₀_π := ⋯, i₁_π := ⋯, weakEquivalence_π := ⋯ }
⊢ Cofibration (X := coprod.{v, u} X X) P'.i

Tactic:
have : Cofibration P'.i := by
    rw [show P'.i = P.i ≫ fac.i by cat_disch]
    infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : LeftHomotopyRel f g
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy f g
fac : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) P.π :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.π
P' : Cylinder.{v, u} X :=
  { I := fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₀ := P.i₀ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₁ := P.i₁ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    π := fac.p (W₁ := trivialCofibrations C) (W₂ := fibrations C), i₀_π := ⋯, i₁_π := ⋯, weakEquivalence_π := ⋯ }
this : Cofibration (X := coprod.{v, u} X X) P'.i
⊢ CommSq (Z := terminal.{v, u} C) h.h (fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (terminal.from Y)
    (terminal.from (fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C)))

Tactic:
have sq : CommSq h.h fac.i (terminal.from _) (terminal.from _) := { }
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : LeftHomotopyRel f g
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy f g
fac : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) P.π :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.π
P' : Cylinder.{v, u} X :=
  { I := fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₀ := P.i₀ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₁ := P.i₁ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    π := fac.p (W₁ := trivialCofibrations C) (W₂ := fibrations C), i₀_π := ⋯, i₁_π := ⋯, weakEquivalence_π := ⋯ }
this : Cofibration (X := coprod.{v, u} X X) P'.i
sq :
  CommSq (Z := terminal.{v, u} C) h.h (fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (terminal.from Y)
    (terminal.from (fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
⊢ ∃ (P : Cylinder.{v, u} X), P.IsVeryGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)

Tactic:
⟨P', { }, ⟨{ h := sq.lift }⟩ ⟩

Premises used: HomotopicalAlgebra.Cylinder.IsVeryGood.mk, CategoryTheory.CommSq.lift, Nonempty.intro, And.intro, Exists.intro, HomotopicalAlgebra.Precylinder.LeftHomotopy.mk
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
inst_2 : IsFibrant.{v, u} Y
h_1 : LeftHomotopyRel f g
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy f g
fac : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) P.π :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.π
P' : Cylinder.{v, u} X :=
  { I := fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₀ := P.i₀ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₁ := P.i₁ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    π := fac.p (W₁ := trivialCofibrations C) (W₂ := fibrations C), i₀_π := ⋯, i₁_π := ⋯, weakEquivalence_π := ⋯ }
this : Cofibration (X := coprod.{v, u} X X) P'.i
sq :
  CommSq (Z := terminal.{v, u} C) h.h (fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (terminal.from Y)
    (terminal.from (fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
⊢ ∃ (P : Cylinder.{v, u} X), P.IsVeryGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)

Tactic:
exact ⟨P', { }, ⟨{ h := sq.lift }⟩ ⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
h : LeftHomotopyRel f g
obtain : ∀ (P : Cylinder.{v, u} X) (h : P.LeftHomotopy f g), LeftHomotopyRel g f
⊢ LeftHomotopyRel g f

Tactic:
obtain ⟨P, ⟨h⟩⟩ := h
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
⊢ LeftHomotopyRel g f

Tactic:
h.symm.leftHomotopyRel

Premises used: HomotopicalAlgebra.Cylinder.LeftHomotopy.leftHomotopyRel, HomotopicalAlgebra.Cylinder.LeftHomotopy.symm