awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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 (Y := Limits.prod.{v, u} A A) (ψ ≫ prod.map P.p₀ (𝟙 A))
have this : Fibration ψ
Tactic: have : Fibration ψ := by
      rw [fibration_iff]
      exact (fibrations C).of_isPullback
        (IsPullback.of_right sq fac (IsPullback.of_prod_fst_with_id P.p₁ A)).flip
          (by rw [← fibration_iff]; infer_instance)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : Q.RightHomotopy f g
⊢ h.h.hom ≫ (Q.map P.ι).p₀ = f.hom
have dsimp : h.h.hom ≫ Q.p₀.hom = f.hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : Q.RightHomotopy f g
⊢ h.h.hom ≫ (Q.map P.ι).p₁ = g.hom
have dsimp : h.h.hom ≫ Q.p₁.hom = g.hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ ObjectProperty.homMk (P := P) h.h ≫ Q.p₀ = f
have h₁ : (ObjectProperty.homMk (P := P) h.h ≫ Q.p₀).hom = f.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Y_1 : C
P_1 : PrepathObject.{v, u} Y_1
X_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : PrepathObject.{v, u} Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ ObjectProperty.homMk (P := P) h.h ≫ Q.p₁ = g
have h₁ : (ObjectProperty.homMk (P := P) h.h ≫ Q.p₁).hom = g.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : PathObject.{v, u} Y
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_3 : MorphismProperty.ContainsIdentities.{v, u} (weakEquivalences C)
f₀ f₁ : X ⟶ Y
h : P.RightHomotopy f₀ f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁
have mk : ∀ (h : X ⟶ P.P), h ≫ P.p₀ = f₀ → h ≫ P.p₁ = f₁ → (WeakEquivalence f₀ ↔ WeakEquivalence f₁)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : PathObject.{v, u} Y
f g : X ⟶ Y
h : P.RightHomotopy f g
d : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} Y Y) P.p :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.p
⊢ Fibration (Y := Limits.prod.{v, u} Y Y)
    (toPrepathObject
        { P := d.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
          p₀ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst,
          p₁ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.snd,
          ι := P.ι ≫ d.i (W₁ := trivialCofibrations C) (W₂ := fibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯,
          weakEquivalence_ι := ⋯ }).p
have rw : fibrations C (Y := Limits.prod.{v, u} Y Y)
  (toPrepathObject
      { P := d.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
        p₀ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst,
        p₁ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.snd,
        ι := P.ι ≫ d.i (W₁ := trivialCofibrations C) (W₂ := fibrations C), ι_p₀ := sorry, ι_p₁ := sorry,
        weakEquivalence_ι := sorry }).p
Tactic: rw [fibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
P : PathObject.{v, u} Y
f g : X ⟶ Y
h : P.RightHomotopy f g
d : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := Limits.prod.{v, u} Y Y) P.p :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.p
⊢ fibrations C (Y := Limits.prod.{v, u} Y Y)
    (toPrepathObject
        { P := d.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
          p₀ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst,
          p₁ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.snd,
          ι := P.ι ≫ d.i (W₁ := trivialCofibrations C) (W₂ := fibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯,
          weakEquivalence_ι := ⋯ }).p
have h₁ : (toPrepathObject
      { P := d.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
        p₀ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.fst,
        p₁ := d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ prod.snd,
        ι := P.ι ≫ d.i (W₁ := trivialCofibrations C) (W₂ := fibrations C), ι_p₀ := sorry, ι_p₁ := sorry,
        weakEquivalence_ι := sorry }).p =
  d.p (W₁ := trivialCofibrations C) (W₂ := fibrations C)
Tactic: convert! d.hp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
⊢ AreEqualizedByLocalization (weakEquivalences C) f g
have rw : L.map f = L.map g
Tactic: rw [areEqualizedByLocalization_iff L]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
⊢ L.map f = L.map g
have suffices : L.map P.p₀ = L.map P.p₁
Tactic: suffices L.map P.p₀ = L.map P.p₁ by
    simp only [← h.h₀, ← h.h₁, L.map_comp, this]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
⊢ weakEquivalences C P.ι
have rw : WeakEquivalence P.ι
Tactic: rw [← weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : PathObject.{v, u} Y
h : P.RightHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
⊢ L.map P.p₀ = L.map P.p₁
have this : IsIso (L.map P.ι)
Tactic: have := Localization.inverts L (weakEquivalences C) P.ι (by
    rw [← weakEquivalence_iff]
    infer_instance)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
h : RightHomotopyRel f g
Z : C
i : Z ⟶ X
⊢ RightHomotopyRel (i ≫ f) (i ≫ g)
have obtain : ∀ (P : PathObject.{v, u} Y) (h : P.RightHomotopy f g), RightHomotopyRel (i ≫ f) (i ≫ g)
Tactic: obtain ⟨P, ⟨h⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
f g : X ⟶ Y
h : RightHomotopyRel f g
⊢ ∃ (P : PathObject.{v, u} Y), P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)
have obtain : ∀ (P : PathObject.{v, u} Y) (h : P.RightHomotopy f g),
  ∃ (P : PathObject.{v, u} Y), P.IsGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)
Tactic: obtain ⟨P, ⟨h⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (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 : IsCofibrant.{v, u} X
h : RightHomotopyRel f g
⊢ ∃ (P : PathObject.{v, u} Y), P.IsVeryGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)
have obtain : ∀ (P : PathObject.{v, u} Y),
  P.IsGood →
    ∀ (h : P.RightHomotopy f g), ∃ (P : PathObject.{v, u} Y), P.IsVeryGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)
Tactic: obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_pathObject
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (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 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
P : PathObject.{v, u} Y
left : P.IsGood
h : P.RightHomotopy f g
fac : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) P.ι :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.ι
P' : PathObject.{v, u} Y :=
  { P := fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
    p₀ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₀,
    p₁ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₁,
    ι := fac.i (W₁ := cofibrations C) (W₂ := trivialFibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
⊢ Fibration (Y := Limits.prod.{v, u} Y Y) P'.p
have rw : Fibration (Y := Limits.prod.{v, u} Y Y) (fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p)
Tactic: rw [show P'.p = fac.p ≫ P.p by cat_disch]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (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 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
P : PathObject.{v, u} Y
left : P.IsGood
h : P.RightHomotopy f g
fac : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) P.ι :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.ι
P' : PathObject.{v, u} Y :=
  { P := fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
    p₀ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₀,
    p₁ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₁,
    ι := fac.i (W₁ := cofibrations C) (W₂ := trivialFibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
⊢ ∃ (P : PathObject.{v, u} Y), P.IsVeryGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)
have this : Fibration (Y := Limits.prod.{v, u} Y Y) P'.p
Tactic: have : Fibration P'.p := by
    rw [show P'.p = fac.p ≫ P.p by cat_disch]
    infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (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 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
P : PathObject.{v, u} Y
left : P.IsGood
h : P.RightHomotopy f g
fac : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) P.ι :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.ι
P' : PathObject.{v, u} Y :=
  { P := fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
    p₀ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₀,
    p₁ := fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.p₁,
    ι := fac.i (W₁ := cofibrations C) (W₂ := trivialFibrations C), ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
this : Fibration (Y := Limits.prod.{v, u} Y Y) P'.p
⊢ ∃ (P : PathObject.{v, u} Y), P.IsVeryGood ∧ Nonempty.{v + 1} (P.RightHomotopy f g)
have sq : CommSq (W := initial.{v, u} C) (initial.to (fac.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C))) (initial.to X)
  (fac.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)) h.h
Tactic: have sq : CommSq (initial.to _) (initial.to _) fac.p h.h := { }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
f g : X ⟶ Y
h : RightHomotopyRel f g
⊢ RightHomotopyRel g f
have obtain : ∀ (P : PathObject.{v, u} Y) (h : P.RightHomotopy f g), RightHomotopyRel g f
Tactic: obtain ⟨P, ⟨h⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
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 : IsFibrant.{v, u} Y
h : RightHomotopyRel f₀ f₁
h' : RightHomotopyRel f₁ f₂
⊢ RightHomotopyRel f₀ f₂
have obtain : ∀ (P : PathObject.{v, u} Y) (h : P.RightHomotopy f₀ f₁), RightHomotopyRel f₀ f₂
Tactic: obtain ⟨P, ⟨h⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
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 : IsFibrant.{v, u} Y
h' : RightHomotopyRel f₁ f₂
P : PathObject.{v, u} Y
h : P.RightHomotopy f₀ f₁
⊢ RightHomotopyRel f₀ f₂
have obtain : ∀ (P' : PathObject.{v, u} Y), P'.IsGood → ∀ (h' : P'.RightHomotopy f₁ f₂), RightHomotopyRel f₀ f₂
Tactic: obtain ⟨P', _, ⟨h'⟩⟩ := h'.exists_good_pathObject
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (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 : IsCofibrant.{v, u} X
h : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
⊢ RightHomotopyRel (f ≫ p) (g ≫ p)
have obtain : ∀ (P : PathObject.{v, u} Y), P.IsVeryGood → ∀ (h : P.RightHomotopy f g), RightHomotopyRel (f ≫ p) (g ≫ p)
Tactic: obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (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 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
⊢ RightHomotopyRel (f ≫ p) (g ≫ p)
have obtain : ∀ (Q : PathObject.{v, u} Z), Q.IsVeryGood → RightHomotopyRel (f ≫ p) (g ≫ p)
Tactic: obtain ⟨Q, _⟩ := PathObject.exists_very_good Z
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (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 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
⊢ RightHomotopyRel (f ≫ p) (g ≫ p)
have sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
Tactic: have sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) := { }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (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 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
⊢ (h.h ≫ sq.lift) ≫ Q.p₀ = f ≫ p
have this : CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ Q.p) prod.fst =
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) prod.fst
Tactic: have := sq.fac_right =≫ prod.fst
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (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 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
this :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ Q.p) prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) prod.fst
⊢ (h.h ≫ sq.lift) ≫ Q.p₀ = f ≫ p
have this₁ : sq.lift ≫ Q.p₀ = P.p₀ ≫ p
Tactic: simp only [Category.assoc, prod.lift_fst, Q.p_fst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (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 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
⊢ (h.h ≫ sq.lift) ≫ Q.p₁ = g ≫ p
have this : CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ Q.p) prod.snd =
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) prod.snd
Tactic: have := sq.fac_right =≫ prod.snd
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (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 : IsCofibrant.{v, u} X
h_1 : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject.{v, u} Y
left : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject.{v, u} Z
h_2 : Q.IsVeryGood
sq : CommSq (Z := Limits.prod.{v, u} Z Z) (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
this :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (sq.lift ≫ Q.p) prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Z Z) (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) prod.snd
⊢ (h.h ≫ sq.lift) ≫ Q.p₁ = g ≫ p
have this₁ : sq.lift ≫ Q.p₁ = P.p₁ ≫ p
Tactic: simp only [Category.assoc, prod.lift_snd, Q.p_snd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : ModelCategory.{v, u} C
inst_2 : IsFibrant.{v, u} Y
f g : X ⟶ Y
⊢ Eq (α := RightHomotopyClass X Y) (mk f) (mk g) ↔ RightHomotopyRel f g
have rw : Eq (α := RightHomotopyClass X Y) (mk f) (mk g) ↔ Relation.EqvGen RightHomotopyRel f g
Tactic: rw [← (RightHomotopyRel.equivalence X Y).eqvGen_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (hypothesis)
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
⊢ ModelCategory.{v_1, u_1} C
have h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
Tactic: have h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor := by
    simp [trivialCofibrations, h₁, h₃]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (hypothesis)
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
⊢ ModelCategory.{v_1, u_1} C
have h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
Tactic: have h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor := by
    simp [trivialFibrations, h₂, h₃]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (hypothesis)
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
⊢ ModelCategory.{v_1, u_1} C
have this : ∀ {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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (hypothesis)
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)
⊢ ModelCategory.{v_1, u_1} C
have this₁ : ∀ {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