awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
⊢ WeakEquivalence (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
have rw : ∀
  (h₁ :
    weakEquivalences C
      (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
        h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g))
  (h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)),
  weakEquivalences C (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
Tactic: rw [weakEquivalence_iff] at h₁ ⊢
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
⊢ sq.HasLift
have this : WeakEquivalence (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
Tactic: have : WeakEquivalence (h.p ≫ pullback.snd p g) := by
      rw [weakEquivalence_iff] at h₁ ⊢
      exact of_precomp _ _ _ h.hi.2 h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
this : WeakEquivalence (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
⊢ (sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g) ≫ p = g
have rw : sq'.lift ≫ (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g) ≫ p = g
Tactic: rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
this : WeakEquivalence (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
rw : sq'.lift ≫ (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g) ≫ p = g
⊢ (sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g) ≫ p = g
have rw₁ : sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g ≫ p = g
Tactic: rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
this : WeakEquivalence (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
rw : sq'.lift ≫ (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g) ≫ p = g
rw₁ : sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g ≫ p = g
⊢ (sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g) ≫ p = g
have rw₂ : sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g ≫ g = g
Tactic: rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : CategoryWithFibrations.{v_1, u_1} C
inst_3 : CategoryWithWeakEquivalences.{v_1, u_1} C
inst_4 : HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
inst_5 : HasFactorization.{v_1, u_1} (trivialCofibrations C) (fibrations C)
inst_6 : HasPullbacks.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (fibrations C)
inst_8 : IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst_9 : Cofibration i
inst_10 : Fibration p
inst_11 : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (trivialCofibrations C) (fibrations C) (Y := pullback p g) (pullback.lift f i ⋯) :=
  factorizationData (trivialCofibrations C) (fibrations C) (pullback.lift f i ⋯)
sq' :
  CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
    (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
h₁ :
  WeakEquivalence
    (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
      h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
h₂ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
this : WeakEquivalence (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
rw : sq'.lift ≫ (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g) ≫ p = g
rw₁ : sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g ≫ p = g
rw₂ : sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g ≫ g = g
⊢ (sq'.lift ≫ h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.fst p g) ≫ p = g
have rw₃ : g = g
Tactic: rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : Q.LeftHomotopy f g
⊢ (Q.map P.ι).i₀ ≫ h.h.hom = f.hom
have dsimp : Q.i₀.hom ≫ h.h.hom = f.hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : Q.LeftHomotopy f g
⊢ (Q.map P.ι).i₁ ≫ h.h.hom = g.hom
have dsimp : Q.i₁.hom ≫ h.h.hom = g.hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ Q.i₀ ≫ ObjectProperty.homMk (P := P) h.h = f
have h₁ : (Q.i₀ ≫ ObjectProperty.homMk (P := P) h.h).hom = f.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 : C
P_1 : Precylinder.{v, u} X_1
Y_1 : C
P : ObjectProperty.{v, u} C
X Y : P.FullSubcategory
Q : Precylinder.{v, u} X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ Q.i₁ ≫ ObjectProperty.homMk (P := P) h.h = g
have h₁ : (Q.i₁ ≫ ObjectProperty.homMk (P := P) h.h).hom = g.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
P : Cylinder.{v, u} X
inst_2 : MorphismProperty.HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_3 : MorphismProperty.ContainsIdentities.{v, u} (weakEquivalences C)
f₀ f₁ : X ⟶ Y
h : P.LeftHomotopy f₀ f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁
have mk : ∀ (h : P.I ⟶ Y), P.i₀ ≫ h = f₀ → P.i₁ ≫ h = f₁ → (WeakEquivalence f₀ ↔ WeakEquivalence f₁)
Tactic: induction h
Cleared hypotheses: h
-- 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
P : Cylinder.{v, u} X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} X X) P.i :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.i
⊢ Cofibration (X := coprod.{v, u} X X)
    (toPrecylinder
        { I := d.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₀ := coprod.inl ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₁ := coprod.inr ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          π := d.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
          weakEquivalence_π := ⋯ }).i
have rw : cofibrations C (X := coprod.{v, u} X X)
  (toPrecylinder
      { I := d.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
        i₀ := coprod.inl ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
        i₁ := coprod.inr ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
        π := d.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.π, i₀_π := sorry, i₁_π := sorry,
        weakEquivalence_π := sorry }).i
Tactic: rw [cofibration_iff]
-- 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
P : Cylinder.{v, u} X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : MorphismProperty.MapFactorizationData (cofibrations C) (trivialFibrations C) (X := coprod.{v, u} X X) P.i :=
  MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.i
⊢ cofibrations C (X := coprod.{v, u} X X)
    (toPrecylinder
        { I := d.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₀ := coprod.inl ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          i₁ := coprod.inr ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
          π := d.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
          weakEquivalence_π := ⋯ }).i
have h₁ : (toPrecylinder
      { I := d.Z (W₁ := cofibrations C) (W₂ := trivialFibrations C),
        i₀ := coprod.inl ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
        i₁ := coprod.inr ≫ d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C),
        π := d.p (W₁ := cofibrations C) (W₂ := trivialFibrations C) ≫ P.π, i₀_π := sorry, i₁_π := sorry,
        weakEquivalence_π := sorry }).i =
  d.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)
Tactic: convert! d.hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy 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.LeftHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy 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.i₀ = L.map P.i₁
Tactic: suffices L.map P.i₀ = L.map P.i₁ by
    simp only [← h.h₀, ← h.h₁, L.map_comp, this]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy 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.LeftHomotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
f g : X ⟶ Y
P : Cylinder.{v, u} X
h : P.LeftHomotopy f g
L : C ⥤ MorphismProperty.Localization.{v, u} (weakEquivalences C) := MorphismProperty.Q (weakEquivalences C)
⊢ L.map P.i₀ = L.map P.i₁
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.LeftHomotopy (goal)
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
Z : C
p : Y ⟶ Z
⊢ LeftHomotopyRel (f ≫ p) (g ≫ p)
have obtain : ∀ (P : Cylinder.{v, u} X) (h : P.LeftHomotopy f g), LeftHomotopyRel (f ≫ p) (g ≫ p)
Tactic: obtain ⟨P, ⟨h⟩⟩ := h
Cleared hypotheses: h
-- 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
h : LeftHomotopyRel f g
⊢ ∃ (P : Cylinder.{v, u} X), P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)
have obtain : ∀ (P : Cylinder.{v, u} X) (h : P.LeftHomotopy f g),
  ∃ (P : Cylinder.{v, u} X), P.IsGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)
Tactic: obtain ⟨P, ⟨h⟩⟩ := h
Cleared hypotheses: h
-- 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
⊢ ∃ (P : Cylinder.{v, u} X), P.IsVeryGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)
have obtain : ∀ (P : Cylinder.{v, u} X),
  P.IsGood → ∀ (h : P.LeftHomotopy f g), ∃ (P : Cylinder.{v, u} X), P.IsVeryGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)
Tactic: obtain ⟨P, _, ⟨h⟩⟩ := h.exists_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
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy f g
fac : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) P.π :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.π
P' : Cylinder.{v, u} X :=
  { I := fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₀ := P.i₀ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₁ := P.i₁ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    π := fac.p (W₁ := trivialCofibrations C) (W₂ := fibrations C), i₀_π := ⋯, i₁_π := ⋯, weakEquivalence_π := ⋯ }
⊢ Cofibration (X := coprod.{v, u} X X) P'.i
have rw : Cofibration (X := coprod.{v, u} X X) (P.i ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: rw [show P'.i = P.i ≫ fac.i by cat_disch]
-- 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
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy f g
fac : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) P.π :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.π
P' : Cylinder.{v, u} X :=
  { I := fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₀ := P.i₀ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₁ := P.i₁ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    π := fac.p (W₁ := trivialCofibrations C) (W₂ := fibrations C), i₀_π := ⋯, i₁_π := ⋯, weakEquivalence_π := ⋯ }
⊢ ∃ (P : Cylinder.{v, u} X), P.IsVeryGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)
have this : Cofibration (X := coprod.{v, u} X X) P'.i
Tactic: have : Cofibration P'.i := by
    rw [show P'.i = P.i ≫ fac.i by cat_disch]
    infer_instance
-- 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
P : Cylinder.{v, u} X
left : P.IsGood
h : P.LeftHomotopy f g
fac : MorphismProperty.MapFactorizationData (trivialCofibrations C) (fibrations C) P.π :=
  MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.π
P' : Cylinder.{v, u} X :=
  { I := fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₀ := P.i₀ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    i₁ := P.i₁ ≫ fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C),
    π := fac.p (W₁ := trivialCofibrations C) (W₂ := fibrations C), i₀_π := ⋯, i₁_π := ⋯, weakEquivalence_π := ⋯ }
this : Cofibration (X := coprod.{v, u} X X) P'.i
⊢ ∃ (P : Cylinder.{v, u} X), P.IsVeryGood ∧ Nonempty.{v + 1} (P.LeftHomotopy f g)
have sq : CommSq (Z := terminal.{v, u} C) h.h (fac.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (terminal.from Y)
  (terminal.from (fac.Z (W₁ := trivialCofibrations C) (W₂ := fibrations C)))
Tactic: have sq : CommSq h.h fac.i (terminal.from _) (terminal.from _) := { }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy (goal)
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
⊢ LeftHomotopyRel g f
have obtain : ∀ (P : Cylinder.{v, u} X) (h : P.LeftHomotopy f g), LeftHomotopyRel g f
Tactic: obtain ⟨P, ⟨h⟩⟩ := h
Cleared hypotheses: h
-- 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₀ f₁ f₂ : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h : LeftHomotopyRel f₀ f₁
h' : LeftHomotopyRel f₁ f₂
⊢ LeftHomotopyRel f₀ f₂
have obtain : ∀ (P : Cylinder.{v, u} X) (h : P.LeftHomotopy f₀ f₁), LeftHomotopyRel f₀ f₂
Tactic: obtain ⟨P, ⟨h⟩⟩ := h
Cleared hypotheses: h
-- 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₀ f₁ f₂ : X ⟶ Y
inst_2 : IsCofibrant.{v, u} X
h' : LeftHomotopyRel f₁ f₂
P : Cylinder.{v, u} X
h : P.LeftHomotopy f₀ f₁
⊢ LeftHomotopyRel f₀ f₂
have obtain : ∀ (P' : Cylinder.{v, u} X), P'.IsGood → ∀ (h' : P'.LeftHomotopy f₁ f₂), LeftHomotopyRel f₀ f₂
Tactic: obtain ⟨P', _, ⟨h'⟩⟩ := h'.exists_good_cylinder