awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact h.symm.leftHomotopyRel

Premises used: HomotopicalAlgebra.Cylinder.LeftHomotopy.leftHomotopyRel, HomotopicalAlgebra.Cylinder.LeftHomotopy.symm
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f₀ f₁ f₂ : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h : LeftHomotopyRel f₀ f₁
h' : LeftHomotopyRel f₁ f₂
obtain : ∀ (P : Cylinder.{v, u} X) (h : P.LeftHomotopy f₀ f₁), LeftHomotopyRel f₀ f₂
⊢ LeftHomotopyRel f₀ 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 : ModelCategory.{v, u} C
f₀ f₁ f₂ : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h' : LeftHomotopyRel f₁ f₂
P : Cylinder.{v, u} X
h : P.LeftHomotopy f₀ f₁
obtain : ∀ (P' : Cylinder.{v, u} X), P'.IsGood → ∀ (h' : P'.LeftHomotopy f₁ f₂), LeftHomotopyRel f₀ f₂
⊢ LeftHomotopyRel f₀ f₂

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₀ f₁ f₂ : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h'_1 : LeftHomotopyRel f₁ f₂
P : Cylinder.{v, u} X
h : P.LeftHomotopy f₀ f₁
P' : Cylinder.{v, u} X
left : P'.IsGood
h' : P'.LeftHomotopy f₁ f₂
⊢ LeftHomotopyRel f₀ f₂

Tactic:
(h.trans h').leftHomotopyRel

Premises used: HomotopicalAlgebra.Cylinder.LeftHomotopy.leftHomotopyRel, HomotopicalAlgebra.Cylinder.LeftHomotopy.trans
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f₀ f₁ f₂ : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h'_1 : LeftHomotopyRel f₁ f₂
P : Cylinder.{v, u} X
h : P.LeftHomotopy f₀ f₁
P' : Cylinder.{v, u} X
left : P'.IsGood
h' : P'.LeftHomotopy f₁ f₂
⊢ LeftHomotopyRel f₀ f₂

Tactic:
exact (h.trans h').leftHomotopyRel

Premises used: HomotopicalAlgebra.Cylinder.LeftHomotopy.leftHomotopyRel, HomotopicalAlgebra.Cylinder.LeftHomotopy.trans
-- 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
Z : C
i : Z ⟶ X
obtain : ∀ (P : Cylinder.{v, u} X), P.IsVeryGood → ∀ (h : P.LeftHomotopy f g), LeftHomotopyRel (i ≫ f) (i ≫ g)
⊢ LeftHomotopyRel (i ≫ f) (i ≫ g)

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

Premises used: HomotopicalAlgebra.LeftHomotopyRel.exists_very_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
Z : C
i : Z ⟶ X
P : Cylinder.{v, u} X
left : P.IsVeryGood
h : P.LeftHomotopy f g
obtain : ∀ (Q : Cylinder.{v, u} Z), Q.IsVeryGood → LeftHomotopyRel (i ≫ f) (i ≫ g)
⊢ LeftHomotopyRel (i ≫ f) (i ≫ g)

Tactic:
obtain ⟨Q, _⟩ := Cylinder.exists_very_good Z

Premises used: HomotopicalAlgebra.Cylinder.exists_very_good
-- 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
Z : C
i : Z ⟶ X
P : Cylinder.{v, u} X
left : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder.{v, u} Z
h_2 : Q.IsVeryGood
⊢ CommSq (W := coprod.{v, u} Z Z) (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)

Tactic:
have sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i) := ⟨by aesop_cat⟩
-- 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
Z : C
i : Z ⟶ X
P : Cylinder.{v, u} X
left : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (W := coprod.{v, u} Z Z) (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
⊢ CategoryStruct.comp (Y := coprod.{v, u} Z Z) coprod.inl (Q.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} Z Z) coprod.inl (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁))

Tactic:
have := coprod.inl ≫= sq.fac_left
-- 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
Z : C
i : Z ⟶ X
P : Cylinder.{v, u} X
left : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (W := coprod.{v, u} Z Z) (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
this :
  CategoryStruct.comp (Y := coprod.{v, u} Z Z) coprod.inl (Q.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} Z Z) coprod.inl (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁))
⊢ Q.i₀ ≫ sq.lift = i ≫ P.i₀

Tactic:
simp only [Q.inl_i_assoc, coprod.inl_desc] at this

Premises used: HomotopicalAlgebra.Cylinder.toPrecylinder, CategoryTheory.Limits.coprod.inl_desc, HomotopicalAlgebra.Precylinder.inl_i_assoc
-- 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
Z : C
i : Z ⟶ X
P : Cylinder.{v, u} X
left : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (W := coprod.{v, u} Z Z) (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
this : Q.i₀ ≫ sq.lift = i ≫ P.i₀
⊢ Q.i₀ ≫ sq.lift ≫ h.h = i ≫ f

Tactic:
simp [reassoc_of% this]
-- 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
Z : C
i : Z ⟶ X
P : Cylinder.{v, u} X
left : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (W := coprod.{v, u} Z Z) (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
⊢ CategoryStruct.comp (Y := coprod.{v, u} Z Z) coprod.inr (Q.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} Z Z) coprod.inr (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁))

Tactic:
have := coprod.inr ≫= sq.fac_left
-- 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
Z : C
i : Z ⟶ X
P : Cylinder.{v, u} X
left : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (W := coprod.{v, u} Z Z) (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
this :
  CategoryStruct.comp (Y := coprod.{v, u} Z Z) coprod.inr (Q.i ≫ sq.lift) =
    CategoryStruct.comp (Y := coprod.{v, u} Z Z) coprod.inr (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁))
⊢ Q.i₁ ≫ sq.lift = i ≫ P.i₁

Tactic:
simp only [Q.inr_i_assoc, coprod.inr_desc] at this

Premises used: HomotopicalAlgebra.Precylinder.inr_i_assoc, HomotopicalAlgebra.Cylinder.toPrecylinder, CategoryTheory.Limits.coprod.inr_desc
-- 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
Z : C
i : Z ⟶ X
P : Cylinder.{v, u} X
left : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (W := coprod.{v, u} Z Z) (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
this : Q.i₁ ≫ sq.lift = i ≫ P.i₁
⊢ Q.i₁ ≫ sq.lift ≫ h.h = i ≫ g

Tactic:
simp [reassoc_of% this]
-- 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
Z : C
i : Z ⟶ X
P : Cylinder.{v, u} X
left : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (W := coprod.{v, u} Z Z) (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
⊢ LeftHomotopyRel (i ≫ f) (i ≫ g)

Tactic:
exact ⟨Q,
   ⟨{ h := sq.lift ≫ h.h
      h₀ := by
        have := coprod.inl ≫= sq.fac_left
        simp only [Q.inl_i_assoc, coprod.inl_desc] at this
        simp [reassoc_of% this]
      h₁ := by
        have := coprod.inr ≫= sq.fac_left
        simp only [Q.inr_i_assoc, coprod.inr_desc] at this
        simp [reassoc_of% this] }⟩⟩
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
⊢ Function.Surjective.{v + 1, v + 1} (α := X ⟶ Y) (β := LeftHomotopyClass X Y) mk

Tactic:
Quot.mk_surjective

Premises used: HomotopicalAlgebra.LeftHomotopyClass.mk, HomotopicalAlgebra.LeftHomotopyClass, Quot.mk_surjective
-- 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
⊢ Eq (α := LeftHomotopyClass X Y) (mk f) (mk g)

Tactic:
Quot.sound h

Premises used: HomotopicalAlgebra.LeftHomotopyClass.mk, Quot.sound, HomotopicalAlgebra.LeftHomotopyClass
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := LeftHomotopyClass X Z) (postcomp (mk f) g) (mk (f ≫ g))

Tactic:
rfl

Premises used: HomotopicalAlgebra.LeftHomotopyClass.postcomp, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
inst_2 : IsCofibrant.{v, u} X
f g : X ⟶ Y
rw : Eq (α := LeftHomotopyClass X Y) (mk f) (mk g) ↔ Relation.EqvGen LeftHomotopyRel f g
⊢ Eq (α := LeftHomotopyClass X Y) (mk f) (mk g) ↔ LeftHomotopyRel f g

Tactic:
rw [← (LeftHomotopyRel.equivalence X Y).eqvGen_iff]

Premises used: HomotopicalAlgebra.LeftHomotopyRel.equivalence, Equivalence.eqvGen_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
inst_2 : IsCofibrant.{v, u} X
f g : X ⟶ Y
⊢ Eq (α := LeftHomotopyClass X Y) (mk f) (mk g) ↔ Relation.EqvGen LeftHomotopyRel f g

Tactic:
Quot.eq

Premises used: HomotopicalAlgebra.LeftHomotopyClass.mk, HomotopicalAlgebra.LeftHomotopyClass, Quot.eq
-- Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
inst_2 : IsCofibrant.{v, u} X
f g : X ⟶ Y
⊢ Eq (α := LeftHomotopyClass X Y) (mk f) (mk g) ↔ Relation.EqvGen LeftHomotopyRel f g

Tactic:
exact Quot.eq

Premises used: Quot.eq
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
rw : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (weakEquivalences C))
⊢ MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (C := Cᵒᵖ) (weakEquivalences Cᵒᵖ)

Tactic:
rw [weakEquivalences_op]

Premises used: HomotopicalAlgebra.weakEquivalences_op
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
⊢ MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (weakEquivalences C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (weakEquivalences C)
rw : MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (weakEquivalences C))
⊢ MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (weakEquivalences Cᵒᵖ)

Tactic:
rw [weakEquivalences_op]

Premises used: HomotopicalAlgebra.weakEquivalences_op
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (weakEquivalences C)
⊢ MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (weakEquivalences C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (cofibrations C)
rw : MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (cofibrations C))
⊢ MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (fibrations Cᵒᵖ)

Tactic:
rw [fibrations_op]

Premises used: HomotopicalAlgebra.fibrations_op
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (cofibrations C)
⊢ MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (cofibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (fibrations C)
rw : MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (fibrations C))
⊢ MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (cofibrations Cᵒᵖ)

Tactic:
rw [cofibrations_op]

Premises used: HomotopicalAlgebra.cofibrations_op
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (fibrations C)
⊢ MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (fibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.HasFactorization.{v, u} (trivialCofibrations C) (fibrations C)
rw :
  MorphismProperty.HasFactorization.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (fibrations C))
    (MorphismProperty.op (trivialCofibrations C))
⊢ MorphismProperty.HasFactorization.{v, u} (C := Cᵒᵖ) (cofibrations Cᵒᵖ) (trivialFibrations Cᵒᵖ)

Tactic:
rw [cofibrations_op, trivialFibrations_op]

Premises used: HomotopicalAlgebra.cofibrations_op, HomotopicalAlgebra.trivialFibrations_op
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.HasFactorization.{v, u} (trivialCofibrations C) (fibrations C)
⊢ MorphismProperty.HasFactorization.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (fibrations C))
    (MorphismProperty.op (trivialCofibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.HasFactorization.{v, u} (cofibrations C) (trivialFibrations C)
rw :
  MorphismProperty.HasFactorization.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (trivialFibrations C))
    (MorphismProperty.op (cofibrations C))
⊢ MorphismProperty.HasFactorization.{v, u} (C := Cᵒᵖ) (trivialCofibrations Cᵒᵖ) (fibrations Cᵒᵖ)

Tactic:
rw [trivialCofibrations_op, fibrations_op, ]

Premises used: HomotopicalAlgebra.trivialCofibrations_op, HomotopicalAlgebra.fibrations_op
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
inst_2 : MorphismProperty.HasFactorization.{v, u} (cofibrations C) (trivialFibrations C)
⊢ MorphismProperty.HasFactorization.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (trivialFibrations C))
    (MorphismProperty.op (cofibrations C))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithCofibrations.{v, u} C
⊢ Eq (α := MorphismProperty (Over.{v, u} S)) (cofibrations (Over.{v, u} S)) (MorphismProperty.over (cofibrations C))

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, HomotopicalAlgebra.cofibrations, CategoryTheory.MorphismProperty.over, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithCofibrations.{v, u} C
X Y : Over.{v, u} S
f : X ⟶ Y
⊢ Cofibration f ↔ Cofibration (Over.Hom.left f)

Tactic:
simp only [cofibration_iff, cofibrations_over_def, MorphismProperty.over_iff]

Premises used: HomotopicalAlgebra.cofibrations_over_def, CategoryTheory.MorphismProperty.over_iff, HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithCofibrations.{v, u} C
X Y : Over.{v, u} S
f : X ⟶ Y
inst_2 rwa rwa₁ rwa₂ rwa₃ : Cofibration f
⊢ Cofibration (Over.Hom.left f)

Tactic:
rwa [← cofibrations_over_iff]

Premises used: HomotopicalAlgebra.cofibrations_over_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (cofibrations C)
rw :
  MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S)
    (MorphismProperty.inverseImage (cofibrations C) (Over.forget S))
⊢ MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S) (cofibrations (Over.{v, u} S))

Tactic:
rw [cofibrations_over_def, MorphismProperty.over_eq_inverseImage]

Premises used: CategoryTheory.MorphismProperty.over_eq_inverseImage, HomotopicalAlgebra.cofibrations_over_def
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (cofibrations C)
⊢ MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S)
    (MorphismProperty.inverseImage (cofibrations C) (Over.forget S))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithFibrations.{v, u} C
⊢ Eq (α := MorphismProperty (Over.{v, u} S)) (fibrations (Over.{v, u} S)) (MorphismProperty.over (fibrations C))

Tactic:
rfl

Premises used: CategoryTheory.Over, HomotopicalAlgebra.fibrations, CategoryTheory.CostructuredArrow, CategoryTheory.MorphismProperty.over, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithFibrations.{v, u} C
X Y : Over.{v, u} S
f : X ⟶ Y
⊢ Fibration f ↔ Fibration (Over.Hom.left f)

Tactic:
simp only [fibration_iff, fibrations_over_def, MorphismProperty.over_iff]

Premises used: HomotopicalAlgebra.fibration_iff, HomotopicalAlgebra.fibrations_over_def, CategoryTheory.MorphismProperty.over_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithFibrations.{v, u} C
X Y : Over.{v, u} S
f : X ⟶ Y
inst_2 rwa rwa₁ rwa₂ rwa₃ : Fibration f
⊢ Fibration (Over.Hom.left f)

Tactic:
rwa [← fibrations_over_iff]

Premises used: HomotopicalAlgebra.fibrations_over_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (fibrations C)
rw :
  MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S)
    (MorphismProperty.inverseImage (fibrations C) (Over.forget S))
⊢ MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S) (fibrations (Over.{v, u} S))

Tactic:
rw [fibrations_over_def, MorphismProperty.over_eq_inverseImage]

Premises used: CategoryTheory.MorphismProperty.over_eq_inverseImage, HomotopicalAlgebra.fibrations_over_def
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (fibrations C)
⊢ MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S)
    (MorphismProperty.inverseImage (fibrations C) (Over.forget S))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
⊢ Eq (α := MorphismProperty (Over.{v, u} S)) (weakEquivalences (Over.{v, u} S))
    (MorphismProperty.over (weakEquivalences C))

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, CategoryTheory.MorphismProperty.over, HomotopicalAlgebra.weakEquivalences, rfl
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : Over.{v, u} S
f : X ⟶ Y
⊢ WeakEquivalence f ↔ WeakEquivalence (Over.Hom.left f)

Tactic:
simp only [weakEquivalence_iff, weakEquivalences_over_def, MorphismProperty.over_iff]

Premises used: HomotopicalAlgebra.weakEquivalence_iff, CategoryTheory.MorphismProperty.over_iff, HomotopicalAlgebra.weakEquivalences_over_def
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : Over.{v, u} S
f : X ⟶ Y
inst_2 rwa rwa₁ rwa₂ rwa₃ : WeakEquivalence f
⊢ WeakEquivalence (Over.Hom.left f)

Tactic:
rwa [← weakEquivalences_over_iff]

Premises used: HomotopicalAlgebra.weakEquivalences_over_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (weakEquivalences C)
rw :
  MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S)
    (MorphismProperty.inverseImage (weakEquivalences C) (Over.forget S))
⊢ MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S) (weakEquivalences (Over.{v, u} S))

Tactic:
rw [weakEquivalences_over_def, MorphismProperty.over_eq_inverseImage]

Premises used: CategoryTheory.MorphismProperty.over_eq_inverseImage, HomotopicalAlgebra.weakEquivalences_over_def
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : MorphismProperty.IsStableUnderRetracts.{v, u} (weakEquivalences C)
⊢ MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S)
    (MorphismProperty.inverseImage (weakEquivalences C) (Over.forget S))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
⊢ Eq (α := MorphismProperty (Over.{v, u} S)) (trivialCofibrations (Over.{v, u} S))
    (MorphismProperty.over (trivialCofibrations C))

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, HomotopicalAlgebra.cofibrations, CategoryTheory.MorphismProperty.over, HomotopicalAlgebra.weakEquivalences, rfl, HomotopicalAlgebra.trivialCofibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Over
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithFibrations.{v, u} C
⊢ Eq (α := MorphismProperty (Over.{v, u} S)) (trivialFibrations (Over.{v, u} S))
    (MorphismProperty.over (trivialFibrations C))

Tactic:
rfl

Premises used: CategoryTheory.Over, HomotopicalAlgebra.fibrations, CategoryTheory.CostructuredArrow, CategoryTheory.MorphismProperty.over, HomotopicalAlgebra.trivialFibrations, HomotopicalAlgebra.weakEquivalences, rfl