awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (goal)
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
⊢ LeftHomotopyRel (i ≫ f) (i ≫ g)
have obtain : ∀ (P : Cylinder.{v, u} X), P.IsVeryGood → ∀ (h : P.LeftHomotopy f g), LeftHomotopyRel (i ≫ f) (i ≫ g)
Tactic: obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_cylinder
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (goal)
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
⊢ LeftHomotopyRel (i ≫ f) (i ≫ g)
have obtain : ∀ (Q : Cylinder.{v, u} Z), Q.IsVeryGood → LeftHomotopyRel (i ≫ f) (i ≫ g)
Tactic: obtain ⟨Q, _⟩ := Cylinder.exists_very_good Z
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (hypothesis)
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
⊢ LeftHomotopyRel (i ≫ f) (i ≫ g)
have sq : 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⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (hypothesis)
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)
⊢ Q.i₀ ≫ sq.lift ≫ h.h = i ≫ f
have 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₁))
Tactic: have := coprod.inl ≫= sq.fac_left
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (hypothesis)
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 ≫ h.h = i ≫ f
have this₁ : Q.i₀ ≫ sq.lift = i ≫ P.i₀
Tactic: simp only [Q.inl_i_assoc, coprod.inl_desc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (hypothesis)
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)
⊢ Q.i₁ ≫ sq.lift ≫ h.h = i ≫ g
have 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₁))
Tactic: have := coprod.inr ≫= sq.fac_left
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (hypothesis)
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 ≫ h.h = i ≫ g
have this₁ : Q.i₁ ≫ sq.lift = i ≫ P.i₁
Tactic: simp only [Q.inr_i_assoc, coprod.inr_desc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (goal)
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) ↔ LeftHomotopyRel f g
have rw : Eq (α := LeftHomotopyClass X Y) (mk f) (mk g) ↔ Relation.EqvGen LeftHomotopyRel f g
Tactic: rw [← (LeftHomotopyRel.equivalence X Y).eqvGen_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Opposite (goal)
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ᵒᵖ) (weakEquivalences Cᵒᵖ)
have rw : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (weakEquivalences C))
Tactic: rw [weakEquivalences_op]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Opposite (goal)
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ᵒᵖ) (weakEquivalences Cᵒᵖ)
have rw : MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (weakEquivalences C))
Tactic: rw [weakEquivalences_op]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Opposite (goal)
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ᵒᵖ) (fibrations Cᵒᵖ)
have rw : MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (cofibrations C))
Tactic: rw [fibrations_op]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Opposite (goal)
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ᵒᵖ) (cofibrations Cᵒᵖ)
have rw : MorphismProperty.IsStableUnderRetracts.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (fibrations C))
Tactic: rw [cofibrations_op]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Opposite (goal)
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ᵒᵖ) (cofibrations Cᵒᵖ) (trivialFibrations Cᵒᵖ)
have rw : MorphismProperty.HasFactorization.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (fibrations C))
  (MorphismProperty.op (trivialCofibrations C))
Tactic: rw [cofibrations_op, trivialFibrations_op]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Opposite (goal)
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ᵒᵖ) (trivialCofibrations Cᵒᵖ) (fibrations Cᵒᵖ)
have rw : MorphismProperty.HasFactorization.{v, u} (C := Cᵒᵖ) (MorphismProperty.op (trivialFibrations C))
  (MorphismProperty.op (cofibrations C))
Tactic: rw [trivialCofibrations_op, fibrations_op, ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Over (goal)
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) (cofibrations (Over.{v, u} S))
have rw : MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S)
  (MorphismProperty.inverseImage (cofibrations C) (Over.forget S))
Tactic: rw [cofibrations_over_def, MorphismProperty.over_eq_inverseImage]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Over (goal)
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) (fibrations (Over.{v, u} S))
have rw : MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S)
  (MorphismProperty.inverseImage (fibrations C) (Over.forget S))
Tactic: rw [fibrations_over_def, MorphismProperty.over_eq_inverseImage]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Over (goal)
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) (weakEquivalences (Over.{v, u} S))
have rw : MorphismProperty.IsStableUnderRetracts (C := Over.{v, u} S)
  (MorphismProperty.inverseImage (weakEquivalences C) (Over.forget S))
Tactic: rw [weakEquivalences_over_def, MorphismProperty.over_eq_inverseImage]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
⊢ MorphismProperty.HasTwoOutOfThreeProperty (C := Over.{v, u} S) (weakEquivalences (Over.{v, u} S))
have rw : MorphismProperty.HasTwoOutOfThreeProperty (C := Over.{v, u} S)
  (MorphismProperty.inverseImage (weakEquivalences C) (Over.forget S))
Tactic: rw [weakEquivalences_over_def, MorphismProperty.over_eq_inverseImage]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : MorphismProperty.HasFactorization.{v, u} (trivialCofibrations C) (fibrations C)
⊢ MorphismProperty.HasFactorization (C := Over.{v, u} S) (trivialCofibrations (Over.{v, u} S))
    (fibrations (Over.{v, u} S))
have rw : MorphismProperty.HasFactorization (C := Over.{v, u} S) (MorphismProperty.over (trivialCofibrations C))
  (MorphismProperty.over (fibrations C))
Tactic: rw [fibrations_over_def, trivialCofibrations_over_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : MorphismProperty.HasFactorization.{v, u} (cofibrations C) (trivialFibrations C)
⊢ MorphismProperty.HasFactorization (C := Over.{v, u} S) (cofibrations (Over.{v, u} S))
    (trivialFibrations (Over.{v, u} S))
have rw : MorphismProperty.HasFactorization (C := Over.{v, u} S) (MorphismProperty.over (cofibrations C))
  (MorphismProperty.over (trivialFibrations C))
Tactic: rw [cofibrations_over_def, trivialFibrations_over_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
⊢ WeakEquivalence P.symm.ι
have dsimp : WeakEquivalence P.ι
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProduct.{v, u} A A
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : HasTerminal.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (fibrations C)
inst_6 : MorphismProperty.IsStableUnderBaseChange.{v, u} (fibrations C)
inst_7 : IsFibrant.{v, u} A
inst_8 : P.IsGood
⊢ Fibration P.p₀
have rw : Fibration (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p prod.fst)
Tactic: rw [← P.p_fst]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProduct.{v, u} A A
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : HasTerminal.{v, u} C
inst_5 : MorphismProperty.IsStableUnderComposition.{v, u} (fibrations C)
inst_6 : MorphismProperty.IsStableUnderBaseChange.{v, u} (fibrations C)
inst_7 : IsFibrant.{v, u} A
inst_8 : P.IsGood
⊢ Fibration P.p₁
have rw : Fibration (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p prod.snd)
Tactic: rw [← P.p_snd]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
⊢ fibrations C (Y := Limits.prod.{v, u} A A) P.p
have rw : Fibration (Y := Limits.prod.{v, u} A A) P.p
Tactic: rw [← fibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
⊢ Fibration (Y := Limits.prod.{v, u} A A) P.symm.p
have hp : fibrations C (Y := Limits.prod.{v, u} A A) P.p
Tactic: have hp : fibrations C P.p := by rw [← fibration_iff]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
hp : fibrations C (Y := Limits.prod.{v, u} A A) P.p
⊢ Fibration (Y := Limits.prod.{v, u} A A) P.symm.p
have rw : fibrations C (Y := Limits.prod.{v, u} A A)
  (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p (Iso.hom (prod.braiding A A)))
Tactic: rw [P.symm_p, fibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : P.IsGood
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
hp : fibrations C (Y := Limits.prod.{v, u} A A) P.p
⊢ fibrations C (Y := Limits.prod.{v, u} A A)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p (Iso.hom (prod.braiding A A)))
have refine : Arrow.mk (Y := Limits.prod.{v, u} A A)
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P.p (Iso.hom (prod.braiding A A))) ≅
  Arrow.mk (Y := Limits.prod.{v, u} A A) P.p
Tactic: refine ((fibrations C).arrow_mk_iso_iff ?_).2 hp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} A
inst_2 : CategoryWithFibrations.{v, u} C
inst_3 : CategoryWithCofibrations.{v, u} C
inst_4 : MorphismProperty.IsStableUnderComposition.{v, u} (cofibrations C)
inst_5 : MorphismProperty.RespectsIso.{v, u} (fibrations C)
inst_6 : HasBinaryProducts.{v, u} C
inst_7 : P.IsVeryGood
⊢ Cofibration P.symm.ι
have dsimp : Cofibration P.ι
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P : PathObject.{v, u} A
h :
  MorphismProperty.MapFactorizationData.{v, u} (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} A A)
    (diag A)
⊢ Cofibration (ofFactorizationData h).ι
have dsimp : Cofibration (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P'.IsGood
⊢ WeakEquivalence
    (CategoryStruct.comp (Y := pullback P.p₁ P'.p₀) (pullback.lift P.ι P'.ι ⋯) (pullback.fst P.p₁ P'.p₀ ≫ P.p₀))
have rw : WeakEquivalence.{v, u} (𝟙 A)
Tactic: rw [pullback.lift_fst_assoc, PrepathObject.ι_p₀]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P'.IsGood
⊢ WeakEquivalence (P.trans P'.toPrepathObject).ι
have this : WeakEquivalence
  (CategoryStruct.comp (Y := pullback P.p₁ P'.p₀) (pullback.lift P.ι P'.ι sorry) (pullback.fst P.p₁ P'.p₀ ≫ P.p₀))
Tactic: have : WeakEquivalence (pullback.lift P.ι P'.ι (by simp) ≫
        pullback.fst P.p₁ P'.p₀ ≫ P.p₀) := by
      rw [pullback.lift_fst_assoc, PrepathObject.ι_p₀]
      infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P'.IsGood
this :
  WeakEquivalence
    (CategoryStruct.comp (Y := pullback P.p₁ P'.p₀) (pullback.lift P.ι P'.ι ⋯) (pullback.fst P.p₁ P'.p₀ ≫ P.p₀))
⊢ WeakEquivalence (P.trans P'.toPrepathObject).ι
have dsimp : WeakEquivalence (Y := pullback P.p₁ P'.p₀) (pullback.lift P.ι P'.ι sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
⊢ Fibration (Y := Limits.prod.{v, u} A A) (P.trans P').p
have rw : Fibration (Y := Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₀ (𝟙 A))
Tactic: rw [show (P.trans P').p = ψ ≫ prod.map P.p₀ (𝟙 A) by simp [PrepathObject.p, ψ]]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
⊢ Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
have h₁ : CategoryStruct.comp (Y := Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) prod.fst =
  CategoryStruct.comp (Y := Limits.prod.{v, u} A A) (pullback.snd P.p₁ P'.p₀ ≫ P'.p) prod.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
h₁ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v, u} A A) (pullback.snd P.p₁ P'.p₀ ≫ P'.p) prod.fst
⊢ Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
have h₂ : CategoryStruct.comp (Y := Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) prod.snd =
  CategoryStruct.comp (Y := Limits.prod.{v, u} A A) (pullback.snd P.p₁ P'.p₀ ≫ P'.p) prod.snd
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
⊢ Fibration (Y := Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₀ (𝟙 A))
have fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
Tactic: have fac : ψ ≫ prod.map P.p₁ (𝟙 A) = pullback.snd _ _ ≫ P'.p := by
      ext
      · simp [ψ, pullback.condition]
      · simp [ψ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
⊢ Fibration (Y := Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₀ (𝟙 A))
have sq : IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁
  (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P'.p prod.fst)
Tactic: have sq : IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁ (P'.p ≫ prod.fst) := by
      simpa [ψ] using IsPullback.of_hasPullback P.p₁ P'.p₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
sq :
  IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P'.p prod.fst)
⊢ Fibration ψ
have rw : fibrations C ψ
Tactic: rw [fibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.PathObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
A : C
P_1 : PathObject.{v, u} A
inst_2 : IsFibrant.{v, u} A
P P' : PathObject.{v, u} A
inst_3 : P.IsGood
inst_4 : P'.IsGood
ψ : (P.trans P').P ⟶ Limits.prod.{v, u} P.P A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : Eq (α := (P.trans P').P ⟶ Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₁ (𝟙 A)) (pullback.snd P.p₁ P'.p₀ ≫ P'.p)
sq :
  IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁
    (CategoryStruct.comp (Y := Limits.prod.{v, u} A A) P'.p prod.fst)
⊢ fibrations C (Y := Limits.prod.{v, u} A A) P'.p
have rw : Fibration (Y := Limits.prod.{v, u} A A) P'.p
Tactic: rw [← fibration_iff]