awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z X Y : C
P : Precylinder.{v, u} X
f g : X ⟶ Y
h : P.LeftHomotopy f g
⊢ Quiver.Hom.unop (h.h.op ≫ P.op.p₁) = g.op.unop

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z : C
X Y : Cᵒᵖ
P : Precylinder.{v, u} X
f g : X ⟶ Y
h : P.LeftHomotopy f g
⊢ (h.h.unop ≫ P.unop.p₀).op = f.unop.op

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 Z : C
X Y : Cᵒᵖ
P : Precylinder.{v, u} X
f g : X ⟶ Y
h : P.LeftHomotopy f g
⊢ (h.h.unop ≫ P.unop.p₁).op = g.unop.op

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
⊢ trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor

Tactic:
simp [trivialCofibrations, h₁, h₃]

Premises used: HomotopicalAlgebra.trivialCofibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
⊢ trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor

Tactic:
have h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor := by
    simp [trivialCofibrations, h₁, h₃]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
⊢ trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor

Tactic:
simp [trivialFibrations, h₂, h₃]

Premises used: HomotopicalAlgebra.trivialFibrations
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
⊢ trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor

Tactic:
have h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor := by
    simp [trivialFibrations, h₂, h₃]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
X Y : C
f : X ⟶ Y
hf : Cofibration f
⊢ Cofibration (e.functor.map f)

Tactic:
simpa [cofibration_iff, h₁] using hf

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
⊢ ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)

Tactic:
have {X Y : C} (f : X ⟶ Y) [hf : Cofibration f] : Cofibration (e.functor.map f) := by
    simpa [cofibration_iff, h₁] using hf
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
X Y : C
f : X ⟶ Y
hf : Fibration f
⊢ Fibration (e.functor.map f)

Tactic:
simpa [fibration_iff, h₂] using hf

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
⊢ ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)

Tactic:
have {X Y : C} (f : X ⟶ Y) [hf : Fibration f] : Fibration (e.functor.map f) := by
    simpa [fibration_iff, h₂] using hf
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
X Y : C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ WeakEquivalence (e.functor.map f)

Tactic:
simpa [weakEquivalence_iff, h₃] using hf

Premises used: HomotopicalAlgebra.weakEquivalence_iff
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
⊢ ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)

Tactic:
have {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f] : WeakEquivalence (e.functor.map f) := by
    simpa [weakEquivalence_iff, h₃] using hf
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
rw : (MorphismProperty.inverseImage (weakEquivalences D) e.functor).HasTwoOutOfThreeProperty
⊢ MorphismProperty.HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)

Tactic:
rw [h₃]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ (MorphismProperty.inverseImage (weakEquivalences D) e.functor).HasTwoOutOfThreeProperty

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
rw : (MorphismProperty.inverseImage (weakEquivalences D) e.functor).IsStableUnderRetracts
⊢ MorphismProperty.IsStableUnderRetracts.{v_1, u_1} (weakEquivalences C)

Tactic:
rw [h₃]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ (MorphismProperty.inverseImage (weakEquivalences D) e.functor).IsStableUnderRetracts

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
rw : (MorphismProperty.inverseImage (fibrations D) e.functor).IsStableUnderRetracts
⊢ MorphismProperty.IsStableUnderRetracts.{v_1, u_1} (fibrations C)

Tactic:
rw [h₂]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ (MorphismProperty.inverseImage (fibrations D) e.functor).IsStableUnderRetracts

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
rw : (MorphismProperty.inverseImage (cofibrations D) e.functor).IsStableUnderRetracts
⊢ MorphismProperty.IsStableUnderRetracts.{v_1, u_1} (cofibrations C)

Tactic:
rw [h₁]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ (MorphismProperty.inverseImage (cofibrations D) e.functor).IsStableUnderRetracts

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
A B X Y : C
x : A ⟶ B
x_1 : X ⟶ Y
h : Cofibration x
h_1 : WeakEquivalence x
h_2 : Fibration x_1
rw : HasLiftingProperty (e.functor.map x) (e.functor.map x_1)
⊢ HasLiftingProperty x x_1

Tactic:
rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.hasLiftingProperty_iff_of_isEquivalence
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
A B X Y : C
x : A ⟶ B
x_1 : X ⟶ Y
h : Cofibration x
h_1 : WeakEquivalence x
h_2 : Fibration x_1
⊢ HasLiftingProperty (e.functor.map x) (e.functor.map x_1)

Tactic:
infer_instance