awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
inst_3 : MorphismProperty.IsStableUnderComposition.{v_1, u_1} (cofibrations C)
X Y : C
i : X ⟶ Y
inst_4 : Cofibration i
hX : Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to X)
⊢ Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to Y)
have rw : Cofibration (X := initial.{v_1, u_1} C) (initial.to X ≫ i)
Tactic: rw [Subsingleton.elim (initial.to Y) (initial.to X ≫ i)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
inst_4 : HasBinaryCoproduct.{v_1, u_1} X Y
hY : IsCofibrant.{v_1, u_1} Y
⊢ Cofibration.{v_1, u_1} (C := C) (X := X) (Y := coprod.{v_1, u_1} X Y) coprod.inl
have hY₁ : Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to Y)
Tactic: rw [isCofibrant_iff] at hY
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
inst_4 : HasBinaryCoproduct.{v_1, u_1} X Y
hY : Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to Y)
⊢ Cofibration.{v_1, u_1} (C := C) (X := X) (Y := coprod.{v_1, u_1} X Y) coprod.inl
have rw : ∀ (hY : cofibrations.{v_1, u_1} C (X := initial.{v_1, u_1} C) (initial.to Y)),
  cofibrations.{v_1, u_1} C (X := X) (Y := coprod.{v_1, u_1} X Y) coprod.inl
Tactic: rw [cofibration_iff] at hY ⊢
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
inst_4 : HasBinaryCoproduct.{v_1, u_1} X Y
hX : IsCofibrant.{v_1, u_1} X
⊢ Cofibration.{v_1, u_1} (C := C) (X := Y) (Y := coprod.{v_1, u_1} X Y) coprod.inr
have hX₁ : Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to X)
Tactic: rw [isCofibrant_iff] at hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
inst_4 : HasBinaryCoproduct.{v_1, u_1} X Y
hX : Cofibration.{v_1, u_1} (X := initial.{v_1, u_1} C) (initial.to X)
⊢ Cofibration.{v_1, u_1} (C := C) (X := Y) (Y := coprod.{v_1, u_1} X Y) coprod.inr
have rw : ∀ (hX : cofibrations.{v_1, u_1} C (X := initial.{v_1, u_1} C) (initial.to X)),
  cofibrations.{v_1, u_1} C (X := Y) (Y := coprod.{v_1, u_1} X Y) coprod.inr
Tactic: rw [cofibration_iff] at hX ⊢
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
hY : IsTerminal.{v_1, u_1} Y
⊢ IsFibrant.{v_1, u_1} X ↔ Fibration p
have simp : fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X) ↔ fibrations C p
Tactic: simp only [fibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
hY : IsTerminal.{v_1, u_1} Y
⊢ fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X) ↔ fibrations C p
have symm : fibrations C p ↔ fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X)
Tactic: symm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
hY : IsTerminal.{v_1, u_1} Y
⊢ fibrations C p ↔ fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X)
have apply : Arrow.mk p ≅ Arrow.mk (Y := terminal.{v_1, u_1} C) (terminal.from X)
Tactic: apply (fibrations C).arrow_mk_iso_iff
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.IsStableUnderComposition.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
inst_4 : Fibration p
hY : IsFibrant.{v_1, u_1} Y
⊢ IsFibrant.{v_1, u_1} X
have hY₁ : Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from Y)
Tactic: rw [isFibrant_iff] at hY ⊢
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
inst_3 : MorphismProperty.IsStableUnderComposition.{v_1, u_1} (fibrations C)
X Y : C
p : X ⟶ Y
inst_4 : Fibration p
hY : Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from Y)
⊢ Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from X)
have rw : Fibration (Y := terminal.{v_1, u_1} C) (p ≫ terminal.from Y)
Tactic: rw [Subsingleton.elim (terminal.from X) (p ≫ terminal.from Y)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hY : IsFibrant.{v_1, u_1} Y
⊢ Fibration.{v_1, u_1} (C := C) (X := Limits.prod.{v_1, u_1} X Y) prod.fst
have hY₁ : Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from Y)
Tactic: rw [isFibrant_iff] at hY
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hY : Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from Y)
⊢ Fibration.{v_1, u_1} (C := C) (X := Limits.prod.{v_1, u_1} X Y) prod.fst
have rw : ∀ (hY : fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from Y)),
  fibrations.{v_1, u_1} C (X := Limits.prod.{v_1, u_1} X Y) prod.fst
Tactic: rw [fibration_iff] at hY ⊢
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hX : IsFibrant.{v_1, u_1} X
⊢ Fibration.{v_1, u_1} (C := C) (X := Limits.prod.{v_1, u_1} X Y) prod.snd
have hX₁ : Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from X)
Tactic: rw [isFibrant_iff] at hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CategoryWithFibrations.{v_1, u_1} C
inst_2 : HasTerminal.{v_1, u_1} C
X Y : C
inst_3 : MorphismProperty.IsStableUnderBaseChange.{v_1, u_1} (fibrations C)
inst_4 : HasBinaryProduct.{v_1, u_1} X Y
hX : Fibration.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (terminal.from X)
⊢ Fibration.{v_1, u_1} (C := C) (X := Limits.prod.{v_1, u_1} X Y) prod.snd
have rw : ∀ (hX : fibrations.{v_1, u_1} C (Y := terminal.{v_1, u_1} C) (terminal.from X)),
  fibrations.{v_1, u_1} C (X := Limits.prod.{v_1, u_1} X Y) prod.snd
Tactic: rw [fibration_iff] at hX ⊢
Cleared hypotheses: hX
-- 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} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [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 p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
⊢ sq.HasLift
have sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
  (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: have sq' : CommSq (𝟙 X) (pushout.inl _ _ ≫ h.i) p h.p := .mk
-- 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} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [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 p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ sq.HasLift
have h₁ : WeakEquivalence
  ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
    h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: have h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p) := by simpa
-- 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} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [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 p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₁ :
  WeakEquivalence
    ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
      h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ sq.HasLift
have h₂ : cofibrations C (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: have h₂ := comp_mem _ _ _ ((cofibrations C).of_isPushout
      (IsPushout.of_hasPushout f i) (mem_cofibrations i)) h.hi
-- 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} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [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 p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₁ :
  WeakEquivalence
    ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
      h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₂ : cofibrations C (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ sq.HasLift
have h₃ : Cofibration (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: rw [← cofibration_iff] at h₂
Cleared hypotheses: 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} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [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 p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₁ :
  WeakEquivalence
    ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
      h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₂ : Cofibration (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ WeakEquivalence (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
have rw : ∀
  (h₁ :
    weakEquivalences C
      ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
        h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C)))
  (h₂ : Cofibration (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))),
  weakEquivalences C (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
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} (cofibrations C) (trivialFibrations C)
inst_6 : HasPushouts.{v_1, u_1} C
inst_7 : IsStableUnderComposition.{v_1, u_1} (cofibrations C)
inst_8 : IsStableUnderCobaseChange.{v_1, u_1} (cofibrations C)
h_1 : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [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 p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : MapFactorizationData (cofibrations C) (trivialFibrations C) (X := pushout f i) (pushout.desc p g ⋯) :=
  factorizationData (cofibrations C) (trivialFibrations C) (pushout.desc p g ⋯)
sq' :
  CommSq (𝟙 X) (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) p
    (h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₁ :
  WeakEquivalence
    ((pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C)) ≫
      h.p (W₁ := cofibrations C) (W₂ := trivialFibrations C))
h₂ : Cofibration (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
⊢ sq.HasLift
have this : WeakEquivalence (pushout.inl f i ≫ h.i (W₁ := cofibrations C) (W₂ := trivialFibrations C))
Tactic: have : WeakEquivalence (pushout.inl f i ≫ h.i) := by
      rw [weakEquivalence_iff] at h₁ ⊢
      exact of_postcomp _ _ _ h.hp.2 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.HasLift
have sq' : CommSq (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) i
  (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g) (𝟙 B)
Tactic: have sq' : CommSq h.i i (h.p ≫ pullback.snd _ _) (𝟙 B) := .mk
-- 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)
⊢ sq.HasLift
have h₁ : WeakEquivalence
  (h.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫
    h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
Tactic: have h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g) := by simpa
-- 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)
⊢ sq.HasLift
have h₂ : fibrations C (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
Tactic: have h₂ := comp_mem _ _ _ h.hp ((fibrations C).of_isPullback
      (IsPullback.of_hasPullback p g) (mem_fibrations p))
-- 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₂ : fibrations C (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
⊢ sq.HasLift
have h₃ : Fibration (h.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ pullback.snd p g)
Tactic: rw [← fibration_iff] at h₂
Cleared hypotheses: h₂