awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
h₁ :
  ∀ (φ : RightHomotopyClass Y Z),
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦ g.precomp h.s) ∘
          fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
        φ =
      id φ
⊢ Eq.{v + 1} (α := RightHomotopyClass Y Z → RightHomotopyClass Y Z)
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦ g.precomp h.s) ∘
      fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
    id

Tactic:
ext φ
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
φ : RightHomotopyClass Y Z
h₁ :
  ∀ (φ : Y ⟶ Z),
    Eq (α := RightHomotopyClass Y Z)
      (((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦ g.precomp h.s) ∘
          fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
        (mk φ))
      (id (mk φ))
⊢ ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦ g.precomp h.s) ∘
        fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
      φ =
    id φ

Tactic:
obtain ⟨φ, rfl⟩ := φ.mk_surjective

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
φ : Y ⟶ Z
⊢ Eq (α := RightHomotopyClass Y Z)
    (((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦ g.precomp h.s) ∘
        fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
      (mk φ))
    (id (mk φ))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
⊢ Function.Bijective (β := RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z)
    fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))

Tactic:
have hj : Function.Bijective (fun (g : RightHomotopyClass Y Z) ↦ g.precomp h.p) := by
    rw [← Function.Bijective.of_comp_iff'
      (precomp_bijective_of_cofibration_of_weakEquivalence Z h.s)]
    convert! Function.bijective_id
    ext φ
    obtain ⟨φ, rfl⟩ := φ.mk_surjective
    simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
hj :
  Function.Bijective (β := RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z)
    fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ Function.Bijective.{v + 1, v + 1} (α := RightHomotopyClass Y Z) (β := RightHomotopyClass X Z)
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
        g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
      fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))

Tactic:
(precomp_bijective_of_cofibration_of_weakEquivalence Z h.i).comp hj

Premises used: HomotopicalAlgebra.CofibrantBrownFactorization.toMapFactorizationData, HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence, Function.Bijective.comp, CategoryTheory.MorphismProperty.MapFactorizationData.i
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
hj :
  Function.Bijective (β := RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z)
    fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₁ :
  Eq.{v + 1} (α := RightHomotopyClass Y Z → RightHomotopyClass X Z) (fun (g : RightHomotopyClass Y Z) ↦ g.precomp f)
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
        g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
      fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
⊢ Function.Bijective (β := RightHomotopyClass X Z) fun (g : RightHomotopyClass Y Z) ↦ g.precomp f

Tactic:
convert! (precomp_bijective_of_cofibration_of_weakEquivalence Z h.i).comp hj using 1

Premises used: HomotopicalAlgebra.CofibrantBrownFactorization.toMapFactorizationData, HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence, Function.Bijective.comp, CategoryTheory.MorphismProperty.MapFactorizationData.i
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
hj :
  Function.Bijective (β := RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z)
    fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₁ :
  ∀ (φ : RightHomotopyClass Y Z),
    φ.precomp f =
      ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
            g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
          fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
        φ
⊢ Eq.{v + 1} (α := RightHomotopyClass Y Z → RightHomotopyClass X Z) (fun (g : RightHomotopyClass Y Z) ↦ g.precomp f)
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
        g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
      fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))

Tactic:
ext φ
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
hj :
  Function.Bijective (β := RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z)
    fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
φ : RightHomotopyClass Y Z
h₁ :
  ∀ (φ : Y ⟶ Z),
    Eq (α := RightHomotopyClass X Z) (precomp (mk φ) f)
      (((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
            g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
          fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
        (mk φ))
⊢ φ.precomp f =
    ((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
          g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
        fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
      φ

Tactic:
obtain ⟨φ, rfl⟩ := φ.mk_surjective

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsFibrant.{v, u} Z
f : X ⟶ Y
inst_3 : IsCofibrant.{v, u} X
inst_4 : IsCofibrant.{v, u} Y
inst_5 : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
hj :
  Function.Bijective (β := RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z)
    fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
φ : Y ⟶ Z
⊢ Eq (α := RightHomotopyClass X Z) (precomp (mk φ) f)
    (((fun (g : RightHomotopyClass (h.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C)) Z) ↦
          g.precomp (h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))) ∘
        fun (g : RightHomotopyClass Y Z) ↦ g.precomp (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
      (mk φ))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
obtain :
  ∀ (g : RightHomotopyClass Y X)
    (hg : Eq.{v + 1} (α := RightHomotopyClass X X) ((fun (g : RightHomotopyClass Y X) ↦ g.precomp f) g) (mk (𝟙 X))),
    ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)
⊢ ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)

Tactic:
obtain ⟨g, hg⟩ := (precomp_bijective_of_weakEquivalence X f).2 (.mk (𝟙 X))

Premises used: CategoryTheory.CategoryStruct.id, HomotopicalAlgebra.RightHomotopyClass.mk, And.right, HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_weakEquivalence
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : RightHomotopyClass Y X
hg : Eq.{v + 1} (α := RightHomotopyClass X X) ((fun (g : RightHomotopyClass Y X) ↦ g.precomp f) g) (mk (𝟙 X))
obtain :
  ∀ (g : Y ⟶ X)
    (hg :
      Eq.{v + 1} (α := RightHomotopyClass X X) ((fun (g : RightHomotopyClass Y X) ↦ g.precomp f) (mk g)) (mk (𝟙 X))),
    ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)
⊢ ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)

Tactic:
obtain ⟨g, rfl⟩ := g.mk_surjective

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg rwa rwa₁ rwa₂ rwa₃ : Eq (α := RightHomotopyClass X X) (mk (f ≫ g)) (mk (𝟙 X))
⊢ RightHomotopyRel (f ≫ g) (𝟙 X)

Tactic:
rwa [← mk_eq_mk_iff]

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg : Eq (α := RightHomotopyClass X X) (mk (f ≫ g)) (mk (𝟙 X))
refine : RightHomotopyRel (g ≫ f) (𝟙 Y)
⊢ ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)

Tactic:
refine ⟨g, by rwa [← mk_eq_mk_iff], ?_⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg : Eq (α := RightHomotopyClass X X) (mk (f ≫ g)) (mk (𝟙 X))
rw : Eq (α := RightHomotopyClass Y Y) (mk (g ≫ f)) (mk (𝟙 Y))
⊢ RightHomotopyRel (g ≫ f) (𝟙 Y)

Tactic:
rw [← mk_eq_mk_iff]

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg : Eq (α := RightHomotopyClass X X) (mk (f ≫ g)) (mk (𝟙 X))
a :
  Eq.{v + 1} (α := RightHomotopyClass X Y) ((fun (g : RightHomotopyClass Y Y) ↦ g.precomp f) (mk (g ≫ f)))
    ((fun (g : RightHomotopyClass Y Y) ↦ g.precomp f) (mk (𝟙 Y)))
⊢ Eq (α := RightHomotopyClass Y Y) (mk (g ≫ f)) (mk (𝟙 Y))

Tactic:
apply (precomp_bijective_of_weakEquivalence Y f).1

Premises used: And.left, HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_weakEquivalence
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg : Eq (α := RightHomotopyClass X X) (mk (f ≫ g)) (mk (𝟙 X))
a : Eq (α := RightHomotopyClass X Y) (mk (f ≫ g ≫ f)) (mk f)
⊢ Eq.{v + 1} (α := RightHomotopyClass X Y) ((fun (g : RightHomotopyClass Y Y) ↦ g.precomp f) (mk (g ≫ f)))
    ((fun (g : RightHomotopyClass Y Y) ↦ g.precomp f) (mk (𝟙 Y)))

Tactic:
simp only [precomp_mk, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, HomotopicalAlgebra.RightHomotopyClass.precomp_mk
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg : Eq (α := RightHomotopyClass X X) (mk (f ≫ g)) (mk (𝟙 X))
a : ∀ (hg : LeftHomotopyRel (f ≫ g) (𝟙 X)), LeftHomotopyRel (f ≫ g ≫ f) f
⊢ Eq (α := RightHomotopyClass X Y) (mk (f ≫ g ≫ f)) (mk f)

Tactic:
rw [mk_eq_mk_iff, ← leftHomotopyRel_iff_rightHomotopyRel] at hg ⊢

Premises used: HomotopicalAlgebra.leftHomotopyRel_iff_rightHomotopyRel, HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
g : Y ⟶ X
hg : LeftHomotopyRel (f ≫ g) (𝟙 X)
⊢ LeftHomotopyRel (f ≫ g ≫ f) f

Tactic:
simpa using hg.postcomp f

Premises used: HomotopicalAlgebra.LeftHomotopyRel.postcomp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
simp : ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)
⊢ ∃ (g : Y ⟶ X), LeftHomotopyRel (f ≫ g) (𝟙 X) ∧ LeftHomotopyRel (g ≫ f) (𝟙 Y)

Tactic:
simp only [leftHomotopyRel_iff_rightHomotopyRel]

Premises used: HomotopicalAlgebra.leftHomotopyRel_iff_rightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsCofibrant.{v, u} Y
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
inst_6 : WeakEquivalence f
⊢ ∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y)

Tactic:
apply RightHomotopyClass.whitehead

Premises used: HomotopicalAlgebra.RightHomotopyClass.whitehead
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
x x_1 : X ⟶ Y
h : LeftHomotopyRel x x_1
rw : RightHomotopyRel x x_1
⊢ Eq (α := RightHomotopyClass X Y) (RightHomotopyClass.mk x) (RightHomotopyClass.mk x_1)

Tactic:
rw [RightHomotopyClass.mk_eq_mk_iff]

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
x x_1 : X ⟶ Y
h : LeftHomotopyRel x x_1
⊢ RightHomotopyRel x x_1

Tactic:
h.rightHomotopyRel

Premises used: HomotopicalAlgebra.LeftHomotopyRel.rightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
x x_1 : X ⟶ Y
h : LeftHomotopyRel x x_1
⊢ RightHomotopyRel x x_1

Tactic:
exact h.rightHomotopyRel

Premises used: HomotopicalAlgebra.LeftHomotopyRel.rightHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
x x_1 : X ⟶ Y
h : RightHomotopyRel x x_1
rw : LeftHomotopyRel x x_1
⊢ Eq (α := LeftHomotopyClass X Y) (LeftHomotopyClass.mk x) (LeftHomotopyClass.mk x_1)

Tactic:
rw [LeftHomotopyClass.mk_eq_mk_iff]

Premises used: HomotopicalAlgebra.LeftHomotopyClass.mk_eq_mk_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
x x_1 : X ⟶ Y
h : RightHomotopyRel x x_1
⊢ LeftHomotopyRel x x_1

Tactic:
h.leftHomotopyRel

Premises used: HomotopicalAlgebra.RightHomotopyRel.leftHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
x x_1 : X ⟶ Y
h : RightHomotopyRel x x_1
⊢ LeftHomotopyRel x x_1

Tactic:
exact h.leftHomotopyRel

Premises used: HomotopicalAlgebra.RightHomotopyRel.leftHomotopyRel
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
x : LeftHomotopyClass X Y
f : X ⟶ Y
⊢ Eq (α := LeftHomotopyClass X Y)
    (Quot.lift (r := RightHomotopyRel) (fun (f : X ⟶ Y) ↦ LeftHomotopyClass.mk f) ⋯
      (Quot.lift (r := LeftHomotopyRel) (fun (f : X ⟶ Y) ↦ RightHomotopyClass.mk f) ⋯ (Quot.mk LeftHomotopyRel f)))
    (Quot.mk LeftHomotopyRel f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y Z : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
x : RightHomotopyClass X Y
f : X ⟶ Y
⊢ Eq (α := RightHomotopyClass X Y)
    (Quot.lift (r := LeftHomotopyRel) (fun (f : X ⟶ Y) ↦ RightHomotopyClass.mk f) ⋯
      (Quot.lift (r := RightHomotopyRel) (fun (f : X ⟶ Y) ↦ LeftHomotopyClass.mk f) ⋯ (Quot.mk RightHomotopyRel f)))
    (Quot.mk RightHomotopyRel f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
f : X ⟶ Y
⊢ Eq (α := RightHomotopyClass X Y)
    ((leftHomotopyClassEquivRightHomotopyClass : (a : LeftHomotopyClass X Y) → RightHomotopyClass X Y)
        (LeftHomotopyClass.mk f) :
      RightHomotopyClass X Y)
    (RightHomotopyClass.mk f : RightHomotopyClass X Y)

Tactic:
rfl

Premises used: HomotopicalAlgebra.RightHomotopyClass.mk, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : C
inst_2 : IsCofibrant.{v, u} X
inst_3 : IsFibrant.{v, u} Y
f : X ⟶ Y
⊢ Eq (α := LeftHomotopyClass X Y)
    ((Equiv.symm leftHomotopyClassEquivRightHomotopyClass : (a : RightHomotopyClass X Y) → LeftHomotopyClass X Y)
        (RightHomotopyClass.mk f) :
      LeftHomotopyClass X Y)
    (LeftHomotopyClass.mk f : LeftHomotopyClass X Y)

Tactic:
rfl

Premises used: HomotopicalAlgebra.LeftHomotopyClass.mk, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : IsStableUnderRetracts.{v, u} (cofibrations C)
inst_4 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
⊢ IsStableUnderRetracts.{v, u} (cofibrations C ⊓ weakEquivalences C)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithFibrations.{v, u} C
inst_3 : IsStableUnderRetracts.{v, u} (fibrations C)
inst_4 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
⊢ IsStableUnderRetracts.{v, u} (fibrations C ⊓ weakEquivalences C)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : IsStableUnderComposition.{v, u} (cofibrations C)
hf : Cofibration f
hg : Cofibration g
⊢ Cofibration (f ≫ g)

Tactic:
(cofibration_iff _).2 ((cofibrations C).comp_mem _ _ hf.mem hg.mem)

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.comp_mem, HomotopicalAlgebra.cofibrations, HomotopicalAlgebra.Cofibration.mem, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : IsStableUnderComposition.{v, u} (fibrations C)
hf : Fibration f
hg : Fibration g
⊢ Fibration (f ≫ g)

Tactic:
(fibration_iff _).2 ((fibrations C).comp_mem _ _ hf.mem hg.mem)

Premises used: Iff.mpr, HomotopicalAlgebra.fibrations, HomotopicalAlgebra.fibration_iff, HomotopicalAlgebra.Fibration.mem, CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Instances
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : IsStableUnderComposition.{v, u} (weakEquivalences C)
hf : WeakEquivalence f
hg : WeakEquivalence g
⊢ WeakEquivalence (f ≫ g)

Tactic:
(weakEquivalence_iff _).2 ((weakEquivalences C).comp_mem _ _ hf.mem hg.mem)

Premises used: Iff.mpr, HomotopicalAlgebra.weakEquivalence_iff, CategoryTheory.MorphismProperty.comp_mem, HomotopicalAlgebra.WeakEquivalence.mem, HomotopicalAlgebra.weakEquivalences