awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
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
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))
⊢ Nonempty (Zigzag R R₀)

Tactic:
exact ⟨Zigzag.of_hom { f := homMk (sq.lift) }⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
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₀)

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) }⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
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₀)
⊢ 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₀⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
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₀)
this :
  Nonempty
    (LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)
⊢ IsConnected
    (LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)

Tactic:
zigzag_isConnected (fun R₁ R₂ ↦ (hR₀ R₁).some.trans (hR₀ R₂).some.symm)

Premises used: Nonempty.some, CategoryTheory.zigzag_isConnected, CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.symm
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
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₀)
this :
  Nonempty
    (LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)
⊢ IsConnected
    (LocalizerMorphism.LeftResolution (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)

Tactic:
exact zigzag_isConnected (fun R₁ R₂ ↦ (hR₀ R₁).some.trans (hR₀ R₂).some.symm)

Premises used: Nonempty.some, CategoryTheory.zigzag_isConnected, CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.symm
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : ModelCategory.{u_2, u_1} C
⊢ LocalizerMorphism.HasLeftResolutions (W₁ := MorphismProperty.arrow (weakEquivalences (CofibrantObject.{u_2, u_1} C)))
    (W₂ := MorphismProperty.arrow (weakEquivalences C))
    (LocalizerMorphism.arrow (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))

Tactic:
fun f ↦ ⟨{
    X₁ := Arrow.mk (homMk (HoCat.resolutionMap f.hom))
    w := Arrow.homMk (HoCat.pResolutionObj f.left) (HoCat.pResolutionObj f.right)
      (HoCat.resolutionMap_fac f.hom).symm
    hw := ⟨mem_weakEquivalences (HoCat.pResolutionObj f.left),
      mem_weakEquivalences (HoCat.pResolutionObj f.right)⟩ }⟩

Premises used: HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj, CategoryTheory.Arrow.left, CategoryTheory.Arrow.hom, HomotopicalAlgebra.mem_weakEquivalences, Nonempty.intro, HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap_fac, And.intro, CategoryTheory.LocalizerMorphism.LeftResolution.mk, Eq.symm, CategoryTheory.Arrow.right, CategoryTheory.Arrow.homMk
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : ModelCategory.{u_2, u_1} C
⊢ LocalizerMorphism.IsLeftDerivabilityStructure (W₁ := weakEquivalences (CofibrantObject.{u_2, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)

Tactic:
.mk' _

Premises used: CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.mk'
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
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
⊢ WeakEquivalence (R.w (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C))

Tactic:
simpa only [weakEquivalence_iff] using R.hw

Premises used: HomotopicalAlgebra.weakEquivalence_iff, CategoryTheory.LocalizerMorphism.RightResolution.hw
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
X : C
⊢ weakEquivalences.{v_1, u_1} C (Y :=
    Functor.obj.{v_1, v_1, u_1, u_1} (C := FibrantObject.{v_1, u_1} C)
      (LocalizerMorphism.functor (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
        (localizerMorphism C))
      (mk (HoCat.resolutionObj.{v_1, u_1} X)))
    (HoCat.iResolutionObj X)

Tactic:
simpa using mem_weakEquivalences (HoCat.iResolutionObj X)

Premises used: HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj, HomotopicalAlgebra.mem_weakEquivalences
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
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
⊢ Eq (α := X ⟶ terminal.{v_1, u_1} 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))))
    (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))))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
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
⊢ 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⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
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
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))))
⊢ Nonempty (Zigzag R R₀)

Tactic:
⟨Zigzag.of_inv { f := homMk sq.lift }⟩

Premises used: CategoryTheory.LocalizerMorphism.RightResolution.Hom.mk, CategoryTheory.CommSq.lift, Nonempty.intro, CategoryTheory.Zigzag.of_inv, HomotopicalAlgebra.FibrantObject.homMk
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
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
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))))
⊢ Nonempty (Zigzag R R₀)

Tactic:
exact ⟨Zigzag.of_inv { f := homMk sq.lift }⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
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₀)

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 }⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
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₀)
⊢ 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₀⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
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₀)
this :
  Nonempty
    (LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)
⊢ IsConnected
    (LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)

Tactic:
zigzag_isConnected (fun R₁ R₂ ↦ (hR₀ R₁).some.trans (hR₀ R₂).some.symm)

Premises used: Nonempty.some, CategoryTheory.zigzag_isConnected, CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.symm
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
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₀)
this :
  Nonempty
    (LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)
⊢ IsConnected
    (LocalizerMorphism.RightResolution (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C) X)

Tactic:
exact zigzag_isConnected (fun R₁ R₂ ↦ (hR₀ R₁).some.trans (hR₀ R₂).some.symm)

Premises used: Nonempty.some, CategoryTheory.zigzag_isConnected, CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.symm
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
⊢ LocalizerMorphism.HasRightResolutions (W₁ := MorphismProperty.arrow (weakEquivalences (FibrantObject.{v_1, u_1} C)))
    (W₂ := MorphismProperty.arrow (weakEquivalences C))
    (LocalizerMorphism.arrow (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ := weakEquivalences C)
      (localizerMorphism C))

Tactic:
fun f ↦ ⟨{
    X₁ := Arrow.mk (homMk (HoCat.resolutionMap f.hom))
    w := Arrow.homMk (HoCat.iResolutionObj f.left) (HoCat.iResolutionObj f.right)
      (HoCat.resolutionMap_fac f.hom)
    hw := ⟨mem_weakEquivalences (HoCat.iResolutionObj f.left),
      mem_weakEquivalences (HoCat.iResolutionObj f.right)⟩ }⟩

Premises used: HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap_fac, CategoryTheory.Arrow.left, HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj, CategoryTheory.LocalizerMorphism.RightResolution.mk, CategoryTheory.Arrow.hom, HomotopicalAlgebra.mem_weakEquivalences, Nonempty.intro, And.intro, CategoryTheory.Arrow.right, CategoryTheory.Arrow.homMk
-- Module: Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
⊢ LocalizerMorphism.IsRightDerivabilityStructure (W₁ := weakEquivalences (FibrantObject.{v_1, u_1} C)) (W₂ :=
    weakEquivalences C) (localizerMorphism C)

Tactic:
.mk' _

Premises used: CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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
⊢ homRel C f g ↔ LeftHomotopyRel f.hom g.hom

Tactic:
Iff.rfl

Premises used: Iff.rfl, HomotopicalAlgebra.FibrantObject.homRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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))
⊢ _root_.Equivalence fun (x1 x2 : X ⟶ Y) ↦ homRel C x1 x2

Tactic:
(LeftHomotopyRel.equivalence _ _).comap (fun (f : X ⟶ Y) ↦ f.hom)

Premises used: HomotopicalAlgebra.FibrantObject.homRel, HomotopicalAlgebra.LeftHomotopyRel.equivalence, CategoryTheory.InducedCategory.Hom.hom, Equivalence.comap
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := FibrantObject.{v_1, u_1} C) (Functor.obj toHoCat)

Tactic:
fun ⟨_⟩ ↦ ⟨_, rfl⟩

Premises used: HomotopicalAlgebra.FibrantObject.toHoCat, Exists, _private.0.HomotopicalAlgebra.FibrantObject.toHoCat_obj_surjective.match_1, Exists.intro, Eq, Function.Surjective, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : ModelCategory.{v_1, u_1} C
⊢ Functor.Full.{v_1, v_1, u_1, u_1} (C := FibrantObject.{v_1, u_1} C) (D := HoCat.{v_1, u_1} C)
    (Quotient.functor (homRel C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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
⊢ Eq (α := Functor.obj toHoCat X ⟶ Functor.obj toHoCat Y) (CategoryTheory.Functor.map toHoCat f)
    (CategoryTheory.Functor.map toHoCat g)

Tactic:
CategoryTheory.Quotient.sound _ h

Premises used: CategoryTheory.Quotient.sound
-- Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
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
rw₃ rw₄ : (fun (x1 x2 : X ⟶ Y) ↦ homRel C x1 x2) 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

Tactic:
rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self, homRel_equivalence_of_isCofibrant_src.eqvGen_eq]

Premises used: CategoryTheory.Functor.homRel_iff, CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen, HomotopicalAlgebra.FibrantObject.homRel_equivalence_of_isCofibrant_src, CategoryTheory.HomRel.compClosure_eq_self, Equivalence.eqvGen_eq