awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P'.IsGood
this :
  WeakEquivalence
    (CategoryStruct.comp (Y := pushout P.i₁ P'.i₀) (P.i₀ ≫ pushout.inl P.i₁ P'.i₀) (pushout.desc P.π P'.π ⋯))
⊢ WeakEquivalence (P.trans P'.toPrecylinder).π
have dsimp : WeakEquivalence (X := pushout P.i₁ P'.i₀) (pushout.desc P.π P'.π sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
⊢ Cofibration (X := coprod.{v, u} A A) (P.trans P').i
have rw : Cofibration (X := coprod.{v, u} A A) (coprod.map P.i₀ (𝟙 A) ≫ ψ)
Tactic: rw [show (P.trans P').i = coprod.map P.i₀ (𝟙 A) ≫ ψ by simp [Precylinder.i, ψ]]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
⊢ Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
have h₁ : CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl (coprod.map P.i₁ (𝟙 A) ≫ ψ) =
  CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl (P'.i ≫ pushout.inr P.i₁ P'.i₀)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
h₁ :
  CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl (coprod.map P.i₁ (𝟙 A) ≫ ψ) =
    CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl (P'.i ≫ pushout.inr P.i₁ P'.i₀)
⊢ Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
have h₂ : CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inr (coprod.map P.i₁ (𝟙 A) ≫ ψ) =
  CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inr (P'.i ≫ pushout.inr P.i₁ P'.i₀)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
⊢ Cofibration (X := coprod.{v, u} A A) (coprod.map P.i₀ (𝟙 A) ≫ ψ)
have fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
Tactic: have fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr _ _ := by
      ext
      · simp [ψ, pushout.condition]
      · simp [ψ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
⊢ Cofibration (X := coprod.{v, u} A A) (coprod.map P.i₀ (𝟙 A) ≫ ψ)
have sq : IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ) (pushout.inr P.i₁ P'.i₀)
Tactic: have sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr _ _) := by
      simpa [ψ] using IsPushout.of_hasPushout P.i₁ P'.i₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
sq :
  IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ)
    (pushout.inr P.i₁ P'.i₀)
⊢ Cofibration ψ
have rw : cofibrations C ψ
Tactic: rw [cofibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
sq :
  IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ)
    (pushout.inr P.i₁ P'.i₀)
⊢ cofibrations C (X := coprod.{v, u} A A) P'.i
have rw : Cofibration (X := coprod.{v, u} A A) P'.i
Tactic: rw [← cofibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Cylinder (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : Cylinder.{v, u} A
inst_2 : IsCofibrant.{v, u} A
P P' : Cylinder.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : coprod.{v, u} P.I A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : Eq (α := coprod.{v, u} A A ⟶ (P.trans P').I) (coprod.map P.i₁ (𝟙 A) ≫ ψ) (P'.i ≫ pushout.inr P.i₁ P'.i₀)
sq :
  IsPushout P.i₁ (CategoryStruct.comp (Y := coprod.{v, u} A A) coprod.inl P'.i) (coprod.inl ≫ ψ)
    (pushout.inr P.i₁ P'.i₀)
⊢ Cofibration (X := coprod.{v, u} A A) (coprod.map P.i₀ (𝟙 A) ≫ ψ)
have this : Cofibration ψ
Tactic: have : Cofibration ψ := by
      rw [cofibration_iff]
      exact (cofibrations C).of_isPushout
        (IsPushout.of_top sq fac (IsPushout.of_coprod_inl_with_id P.i₁ A).flip)
        (by rw [← cofibration_iff]; infer_instance)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : ModelCategory.{u_2, u_1} C
X : C
R₀ : LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
  (localizerMorphism C) X :=
  LocalizerMorphism.LeftResolution.mk (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (X₁ := mk (HoCat.resolutionObj.{u_2, u_1} X)) (HoCat.pResolutionObj X) ⋯
R :
  LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) X
⊢ Nonempty (Zigzag R R₀)
have sq : CommSq (W := initial.{u_2, u_1} C)
  (initial.to
    (Functor.obj
      (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
        (localizerMorphism C))
      (R₀.X₁ (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))))
  (initial.to
    (Functor.obj
      (LocalizerMorphism.functor (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
        (localizerMorphism C))
      (R.X₁ (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))))
  (R₀.w (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))
  (R.w (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C))
Tactic: have sq : CommSq (initial.to _) (initial.to _) R₀.w R.w := ⟨by simp⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : ModelCategory.{u_2, u_1} C
X : C
R₀ : LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
  (localizerMorphism C) X :=
  LocalizerMorphism.LeftResolution.mk (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (X₁ := mk (HoCat.resolutionObj.{u_2, u_1} X)) (HoCat.pResolutionObj X) ⋯
⊢ IsConnected
    (LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)
have hR₀ : ∀
  (R :
    LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X),
  Nonempty (Zigzag R R₀)
Tactic: have hR₀ (R) : Nonempty (Zigzag R R₀) := by
    have sq : CommSq (initial.to _) (initial.to _) R₀.w R.w := ⟨by simp⟩
    exact ⟨Zigzag.of_hom { f := homMk (sq.lift) }⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant (hypothesis)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : ModelCategory.{u_2, u_1} C
X : C
R₀ : LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
  (localizerMorphism C) X :=
  LocalizerMorphism.LeftResolution.mk (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (X₁ := mk (HoCat.resolutionObj.{u_2, u_1} X)) (HoCat.pResolutionObj X) ⋯
hR₀ :
  ∀
    (R :
      LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ :=
        weakEquivalences C) (localizerMorphism C) X),
    Nonempty (Zigzag R R₀)
⊢ IsConnected
    (LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)
have this : Nonempty
  (LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) X)
Tactic: have : Nonempty ((localizerMorphism C).LeftResolution X) := ⟨R₀⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
R₀ : LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
  (localizerMorphism C) X :=
  LocalizerMorphism.RightResolution.mk (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (X₁ := mk (HoCat.resolutionObj.{v_1, u_1} X)) (HoCat.iResolutionObj X) ⋯
R :
  LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) X
⊢ Nonempty (Zigzag R R₀)
have sq : CommSq (Z := terminal.{v_1, u_1} C)
  (R.w (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C))
  (R₀.w (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C))
  (terminal.from
    (Functor.obj
      (LocalizerMorphism.functor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
        (localizerMorphism C))
      (R.X₁ (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C))))
  (terminal.from
    (Functor.obj
      (LocalizerMorphism.functor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
        (localizerMorphism C))
      (R₀.X₁ (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C))))
Tactic: have sq : CommSq R.w R₀.w (terminal.from _) (terminal.from _) := ⟨by simp⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
R₀ : LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
  (localizerMorphism C) X :=
  LocalizerMorphism.RightResolution.mk (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (X₁ := mk (HoCat.resolutionObj.{v_1, u_1} X)) (HoCat.iResolutionObj X) ⋯
⊢ IsConnected
    (LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)
have hR₀ : ∀
  (R :
    LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X),
  Nonempty (Zigzag R R₀)
Tactic: have hR₀ (R) : Nonempty (Zigzag R R₀) := by
    have sq : CommSq R.w R₀.w (terminal.from _) (terminal.from _) := ⟨by simp⟩
    exact ⟨Zigzag.of_inv { f := homMk sq.lift }⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
R₀ : LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
  (localizerMorphism C) X :=
  LocalizerMorphism.RightResolution.mk (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (X₁ := mk (HoCat.resolutionObj.{v_1, u_1} X)) (HoCat.iResolutionObj X) ⋯
hR₀ :
  ∀
    (R :
      LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
        (localizerMorphism C) X),
    Nonempty (Zigzag R R₀)
⊢ IsConnected
    (LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)
have this : Nonempty
  (LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
    (localizerMorphism C) X)
Tactic: have : Nonempty ((localizerMorphism C).RightResolution X) := ⟨R₀⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
inst_2 : IsCofibrant.{v_1, u_1} (X.obj (P := fibrantObjects C))
f g : X ⟶ Y
⊢ Eq (α :=
      Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj (Quotient.functor (homRel C)) X)
        (Functor.obj (Quotient.functor (homRel C)) Y))
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) f)
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) g) ↔
    homRel C f g
have rw : Functor.homRel (D := HoCat.{v_1, u_1} C) (Quotient.functor (homRel C)) f g ↔ homRel C f g
Tactic: rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isCofibrant_src.eqvGen_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
inst_2 : IsCofibrant.{v_1, u_1} (X.obj (P := fibrantObjects C))
f g : X ⟶ Y
rw : Functor.homRel (D := HoCat.{v_1, u_1} C) (Quotient.functor (homRel C)) f g ↔ homRel C f g
⊢ Eq (α :=
      Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj (Quotient.functor (homRel C)) X)
        (Functor.obj (Quotient.functor (homRel C)) Y))
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) f)
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) g) ↔
    homRel C f g
have rw₁ : Relation.EqvGen (HomRel.CompClosure (homRel C)) f g ↔ homRel C f g
Tactic: rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isCofibrant_src.eqvGen_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
inst_2 : IsCofibrant.{v_1, u_1} (X.obj (P := fibrantObjects C))
f g : X ⟶ Y
rw : Functor.homRel (D := HoCat.{v_1, u_1} C) (Quotient.functor (homRel C)) f g ↔ homRel C f g
rw₁ : Relation.EqvGen (HomRel.CompClosure (homRel C)) f g ↔ homRel C f g
⊢ Eq (α :=
      Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj (Quotient.functor (homRel C)) X)
        (Functor.obj (Quotient.functor (homRel C)) Y))
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) f)
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) g) ↔
    homRel C f g
have rw₂ : Relation.EqvGen (homRel C) f g ↔ homRel C f g
Tactic: rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isCofibrant_src.eqvGen_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
inst_2 : IsCofibrant.{v_1, u_1} (X.obj (P := fibrantObjects C))
f g : X ⟶ Y
rw : Functor.homRel (D := HoCat.{v_1, u_1} C) (Quotient.functor (homRel C)) f g ↔ homRel C f g
rw₁ : Relation.EqvGen (HomRel.CompClosure (homRel C)) f g ↔ homRel C f g
rw₂ : Relation.EqvGen (homRel C) f g ↔ homRel C f g
⊢ Eq (α :=
      Quiver.Hom (V := HoCat.{v_1, u_1} C) (Functor.obj (Quotient.functor (homRel C)) X)
        (Functor.obj (Quotient.functor (homRel C)) Y))
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) f)
      (CategoryTheory.Functor.map (Quotient.functor (homRel C)) g) ↔
    homRel C f g
have rw₃ : (fun (x1 x2 : X ⟶ Y) ↦ homRel C x1 x2) f g ↔ homRel C f g
Tactic: rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isCofibrant_src.eqvGen_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
⊢ weakEquivalences (FibrantObject.{v_1, u_1} C) f ↔ weakEquivalences (FibrantObject.{v_1, u_1} C) g
have simp : WeakEquivalence f.hom ↔ WeakEquivalence g.hom
Tactic: simp only [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
⊢ WeakEquivalence f.hom ↔ WeakEquivalence g.hom
have obtain : ∀ (P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))) (h : P.LeftHomotopy f.hom g.hom),
  WeakEquivalence f.hom ↔ WeakEquivalence g.hom
Tactic: obtain ⟨P, ⟨h⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f : X ⟶ Y
⊢ WeakEquivalence (X := Functor.obj toHoCat X) (CategoryTheory.Functor.map toHoCat f) ↔ WeakEquivalence f
have simp : weakEquivalences (HoCat.{v_1, u_1} C) (X := Functor.obj toHoCat X) (CategoryTheory.Functor.map toHoCat f) ↔
  weakEquivalences (FibrantObject.{v_1, u_1} C) f
Tactic: simp only [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
x x_1 : FibrantObject.{v_1, u_1} C
x_2 : x ⟶ x_1
h : weakEquivalences (FibrantObject.{v_1, u_1} C) x_2
⊢ MorphismProperty.inverseImage (weakEquivalences (HoCat.{v_1, u_1} C)) toHoCat x_2
have h₁ : WeakEquivalence x_2
Tactic: simp only [← weakEquivalence_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h : homRel C f g
⊢ AreEqualizedByLocalization (weakEquivalences (FibrantObject.{v_1, u_1} C)) f g
have obtain : ∀ (P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))),
  P.IsVeryGood →
    ∀ (h : P.LeftHomotopy f.hom g.hom), AreEqualizedByLocalization (weakEquivalences (FibrantObject.{v_1, u_1} C)) f g
Tactic: obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_cylinder
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))
left : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := FibrantObject.{v_1, u_1} C)
    (weakEquivalences (FibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (FibrantObject.{v_1, u_1} C))
⊢ AreEqualizedByLocalization (weakEquivalences (FibrantObject.{v_1, u_1} C)) f g
have rw : L.map f = L.map g
Tactic: rw [areEqualizedByLocalization_iff L]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))
left : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := FibrantObject.{v_1, u_1} C)
    (weakEquivalences (FibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (FibrantObject.{v_1, u_1} C))
⊢ L.map f = L.map g
have suffices : Eq (α := L.obj (mk (X.obj (P := fibrantObjects C))) ⟶ L.obj (mk P.I)) (L.map (homMk P.i₀)) (L.map (homMk P.i₁))
Tactic: suffices L.map (homMk P.i₀) = L.map (homMk P.i₁) by
    simp only [show f = homMk P.i₀ ≫ homMk h.h by cat_disch,
      show g = homMk P.i₁ ≫ homMk h.h by cat_disch, Functor.map_comp, this]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))
left : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := FibrantObject.{v_1, u_1} C)
    (weakEquivalences (FibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (FibrantObject.{v_1, u_1} C))
⊢ weakEquivalences (FibrantObject.{v_1, u_1} C) (X := mk P.I) (Y := mk (X.obj (P := fibrantObjects C))) (homMk P.π)
have simp : WeakEquivalence P.π
Tactic: simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X Y : FibrantObject.{v_1, u_1} C
f g : X ⟶ Y
h_1 : homRel C f g
P : Cylinder.{v_1, u_1} (X.obj (P := fibrantObjects C))
left : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject.{v_1, u_1} C ⥤
  MorphismProperty.Localization.{v_1, u_1} (C := FibrantObject.{v_1, u_1} C)
    (weakEquivalences (FibrantObject.{v_1, u_1} C)) :=
  MorphismProperty.Q (weakEquivalences (FibrantObject.{v_1, u_1} C))
⊢ Eq (α := L.obj (mk (X.obj (P := fibrantObjects C))) ⟶ L.obj (mk P.I)) (L.map (homMk P.i₀)) (L.map (homMk P.i₁))
have this : IsIso (X := L.obj (mk P.I)) (Y := L.obj (mk (X.obj (P := fibrantObjects C)))) (L.map (homMk P.π))
Tactic: have := Localization.inverts L (weakEquivalences _) (homMk P.π) (by
    simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
    infer_instance)