awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
fg : X ⟶ Z
fac : f ≫ g = fg
inst_3 : WeakEquivalence g
hfg : WeakEquivalence fg
⊢ WeakEquivalence f
have hfg₁ : WeakEquivalence (f ≫ g)
Tactic: subst fac
Cleared hypotheses: fg, fac, hfg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
fg : X ⟶ Z
fac : f ≫ g = fg
inst_3 : WeakEquivalence f
inst_4 : WeakEquivalence fg
⊢ WeakEquivalence g
have inst : WeakEquivalence (f ≫ g)
Tactic: subst fac
Cleared hypotheses: fg, fac, inst_4
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsStableUnderCobaseChange.{v, u} (trivialCofibrations C)
have rw : IsStableUnderCobaseChange.{v, u} (llp (fibrations C))
Tactic: rw [← fibrations_llp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsStableUnderBaseChange.{v, u} (fibrations C)
have rw : IsStableUnderBaseChange.{v, u} (rlp (trivialCofibrations C))
Tactic: rw [← trivialCofibrations_rlp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsMultiplicative.{v, u} (trivialCofibrations C)
have rw : IsMultiplicative.{v, u} (llp (fibrations C))
Tactic: rw [← fibrations_llp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsMultiplicative.{v, u} (fibrations C)
have rw : IsMultiplicative.{v, u} (rlp (trivialCofibrations C))
Tactic: rw [← trivialCofibrations_rlp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
J : Type w
⊢ IsStableUnderCoproductsOfShape.{v, u, w} (trivialCofibrations C) J
have rw : IsStableUnderCoproductsOfShape.{v, u, w} (llp (fibrations C)) J
Tactic: rw [← fibrations_llp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
J : Type w
⊢ IsStableUnderProductsOfShape.{v, u, w} (fibrations C) J
have rw : IsStableUnderProductsOfShape.{v, u, w} (rlp (trivialCofibrations C)) J
Tactic: rw [← trivialCofibrations_rlp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
⊢ IsStableUnderCobaseChange.{v, u} (cofibrations C)
have rw : IsStableUnderCobaseChange.{v, u} (llp (trivialFibrations C))
Tactic: rw [← trivialFibrations_llp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
⊢ IsStableUnderBaseChange.{v, u} (trivialFibrations C)
have rw : IsStableUnderBaseChange.{v, u} (rlp (cofibrations C))
Tactic: rw [← cofibrations_rlp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
⊢ IsMultiplicative.{v, u} (cofibrations C)
have rw : IsMultiplicative.{v, u} (llp (trivialFibrations C))
Tactic: rw [← trivialFibrations_llp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
⊢ IsMultiplicative.{v, u} (trivialFibrations C)
have rw : IsMultiplicative.{v, u} (rlp (cofibrations C))
Tactic: rw [← cofibrations_rlp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
J : Type w
⊢ IsStableUnderCoproductsOfShape.{v, u, w} (cofibrations C) J
have rw : IsStableUnderCoproductsOfShape.{v, u, w} (llp (trivialFibrations C)) J
Tactic: rw [← trivialFibrations_llp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
J : Type w
⊢ IsStableUnderProductsOfShape.{v, u, w} (trivialFibrations C) J
have rw : IsStableUnderProductsOfShape.{v, u, w} (rlp (cofibrations C)) J
Tactic: rw [← cofibrations_rlp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (cofibrations C)
hg : Cofibration g
⊢ Cofibration (Y := pushout f g) (pushout.inl f g)
have rw : ∀ (hg : cofibrations C g), cofibrations C (Y := pushout f g) (pushout.inl f g)
Tactic: rw [cofibration_iff] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (cofibrations C)
hf : Cofibration f
⊢ Cofibration (Y := pushout f g) (pushout.inr f g)
have rw : ∀ (hf : cofibrations C f), cofibrations C (Y := pushout f g) (pushout.inr f g)
Tactic: rw [cofibration_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (trivialCofibrations C)
inst_6 : Cofibration g
inst_7 : WeakEquivalence g
⊢ WeakEquivalence (Y := pushout f g) (pushout.inl f g)
have rw : weakEquivalences C (Y := pushout f g) (pushout.inl f g)
Tactic: rw [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_4 : HasPushout f g
inst_5 : IsStableUnderCobaseChange.{v, u} (trivialCofibrations C)
inst_6 : Cofibration f
inst_7 : WeakEquivalence f
⊢ WeakEquivalence (Y := pushout f g) (pushout.inr f g)
have rw : weakEquivalences C (Y := pushout f g) (pushout.inr f g)
Tactic: rw [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (fibrations C)
hf : Fibration f
⊢ Fibration (X := pullback f g) (pullback.snd f g)
have rw : ∀ (hf : fibrations C f), fibrations C (X := pullback f g) (pullback.snd f g)
Tactic: rw [fibration_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (fibrations C)
hg : Fibration g
⊢ Fibration (X := pullback f g) (pullback.fst f g)
have rw : ∀ (hg : fibrations C g), fibrations C (X := pullback f g) (pullback.fst f g)
Tactic: rw [fibration_iff] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (trivialFibrations C)
inst_6 : Fibration f
inst_7 : WeakEquivalence f
⊢ WeakEquivalence (X := pullback f g) (pullback.snd f g)
have rw : weakEquivalences C (X := pullback f g) (pullback.snd f g)
Tactic: rw [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_4 : HasPullback f g
inst_5 : IsStableUnderBaseChange.{v, u} (trivialFibrations C)
inst_6 : Fibration g
inst_7 : WeakEquivalence g
⊢ WeakEquivalence (X := pullback f g) (pullback.fst f g)
have rw : weakEquivalences C (X := pullback f g) (pullback.fst f g)
Tactic: rw [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasCoproduct.{u_1, v, u} X
inst_5 : HasCoproduct.{u_1, v, u} Y
h : ∀ (i : J), Cofibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
⊢ Cofibration (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map f)
have simp : ∀ (h : ∀ (i : J), cofibrations C (f i)),
  cofibrations C (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map f)
Tactic: simp only [cofibration_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasCoproduct.{u_1, v, u} X
inst_5 : HasCoproduct.{u_1, v, u} Y
h : ∀ (i : J), Cofibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_7 : ∀ (i : J), WeakEquivalence (f i)
⊢ WeakEquivalence (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map f)
have rw : weakEquivalences C (X := sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_1, v, u} Y) (Limits.Sigma.map f)
Tactic: rw [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasProduct.{u_1, v, u} X
inst_5 : HasProduct.{u_1, v, u} Y
h : ∀ (i : J), Fibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ Fibration (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map f)
have simp : ∀ (h : ∀ (i : J), fibrations C (f i)),
  fibrations C (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map f)
Tactic: simp only [fibration_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
J_1 : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst_4 : HasProduct.{u_1, v, u} X
inst_5 : HasProduct.{u_1, v, u} Y
h : ∀ (i : J), Fibration (f i)
inst_6 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_7 : ∀ (i : J), WeakEquivalence (f i)
⊢ WeakEquivalence (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map f)
have rw : weakEquivalences C (X := piObj.{u_1, v, u} X) (Y := piObj.{u_1, v, u} Y) (Limits.Pi.map f)
Tactic: rw [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
h₁ : Cofibration f₁
h₂ : Cofibration f₂
inst_5 : HasBinaryCoproduct.{v, u} X₁ X₂
inst_6 : HasBinaryCoproduct.{v, u} Y₁ Y₂
⊢ Cofibration (X := coprod.{v, u} X₁ X₂) (Y := coprod.{v, u} Y₁ Y₂) (coprod.map f₁ f₂)
have rw : ∀ (h₁ : cofibrations C f₁) (h₂ : cofibrations C f₂) [inst_7 : HasBinaryCoproduct.{v, u} X₁ X₂]
  [inst_8 : HasBinaryCoproduct.{v, u} Y₁ Y₂],
  cofibrations C (X := coprod.{v, u} X₁ X₂) (Y := coprod.{v, u} Y₁ Y₂) (coprod.map f₁ f₂)
Tactic: rw [cofibration_iff] at h₁ h₂ ⊢
Cleared hypotheses: h₁, h₂, inst_5, inst_6
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst_5 : HasBinaryCoproduct.{v, u} X₁ X₂
inst_6 : HasBinaryCoproduct.{v, u} Y₁ Y₂
⊢ cofibrations C (X := coprod.{v, u} X₁ X₂) (Y := coprod.{v, u} Y₁ Y₂) (coprod.map f₁ f₂)
have hf : functorCategory.{v, 0, 0, u} (cofibrations C) (Discrete WalkingPair) (X := pair X₁ X₂) (Y := pair Y₁ Y₂) (mapPair f₁ f₂)
Tactic: apply MorphismProperty.colimMap
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
h₁ : Fibration f₁
h₂ : Fibration f₂
inst_5 : HasBinaryProduct.{v, u} X₁ X₂
inst_6 : HasBinaryProduct.{v, u} Y₁ Y₂
⊢ Fibration (X := Limits.prod.{v, u} X₁ X₂) (Y := Limits.prod.{v, u} Y₁ Y₂) (prod.map f₁ f₂)
have rw : ∀ (h₁ : fibrations C f₁) (h₂ : fibrations C f₂) [inst_7 : HasBinaryProduct.{v, u} X₁ X₂]
  [inst_8 : HasBinaryProduct.{v, u} Y₁ Y₂],
  fibrations C (X := Limits.prod.{v, u} X₁ X₂) (Y := Limits.prod.{v, u} Y₁ Y₂) (prod.map f₁ f₂)
Tactic: rw [fibration_iff] at h₁ h₂ ⊢
Cleared hypotheses: h₁, h₂, inst_5, inst_6
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst_5 : HasBinaryProduct.{v, u} X₁ X₂
inst_6 : HasBinaryProduct.{v, u} Y₁ Y₂
⊢ fibrations C (X := Limits.prod.{v, u} X₁ X₂) (Y := Limits.prod.{v, u} Y₁ Y₂) (prod.map f₁ f₂)
have hf : functorCategory.{v, 0, 0, u} (fibrations C) (Discrete WalkingPair) (X := pair X₁ X₂) (Y := pair Y₁ Y₂) (mapPair f₁ f₂)
Tactic: apply MorphismProperty.limMap
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsIso f
⊢ Cofibration f
have this : llp (fibrations C) f
Tactic: have := (fibrations C).llp_of_isIso f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsIso f
this : llp (fibrations C) f
⊢ Cofibration f
have this₁ : trivialCofibrations C f
Tactic: rw [fibrations_llp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_5 : IsIso f
⊢ Fibration f
have this : rlp (cofibrations C) f
Tactic: have := (cofibrations C).rlp_of_isIso f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_5 : IsIso f
this : rlp (cofibrations C) f
⊢ Fibration f
have this₁ : trivialFibrations C f
Tactic: rw [cofibrations_rlp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsIso f
⊢ WeakEquivalence f
have have : ∀ (h : MapFactorizationData (trivialCofibrations C) (fibrations C) f), WeakEquivalence f
Tactic: have h := MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsIso f
h : MapFactorizationData (trivialCofibrations C) (fibrations C) f
⊢ WeakEquivalence f
have rw : weakEquivalences C f
Tactic: rw [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsStableUnderComposition.{v, u} (weakEquivalences C)
x : C
⊢ weakEquivalences.{v, u} C (𝟙 x)
have rw : WeakEquivalence.{v, u} (𝟙 x)
Tactic: rw [← weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
inst_5 : IsStableUnderRetracts.{v, u} (weakEquivalences C)
inst_6 : IsStableUnderComposition.{v, u} (weakEquivalences C)
x x_1 : C
x_2 : x ⟶ x_1
h : IsIso x_2
⊢ weakEquivalences C x_2
have rw : WeakEquivalence x_2
Tactic: rw [← weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Instances (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithWeakEquivalences.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : ContainsIdentities.{v, u} (weakEquivalences C)
X : C
⊢ WeakEquivalence.{v, u} (𝟙 X)
have rw : weakEquivalences.{v, u} C (𝟙 X)
Tactic: rw [weakEquivalence_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 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (cofibrations C)
A X : C
i : A ⟶ X
hA : IsInitial.{v_1, u_1} A
⊢ IsCofibrant.{v_1, u_1} X ↔ Cofibration i
have simp : cofibrations.{v_1, u_1} C (X := initial.{v_1, u_1} C) (initial.to X) ↔ cofibrations C i
Tactic: simp only [cofibration_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 : CategoryWithCofibrations.{v_1, u_1} C
inst_2 : HasInitial.{v_1, u_1} C
inst_3 : MorphismProperty.RespectsIso.{v_1, u_1} (cofibrations C)
A X : C
i : A ⟶ X
hA : IsInitial.{v_1, u_1} A
⊢ cofibrations.{v_1, u_1} C (X := initial.{v_1, u_1} C) (initial.to X) ↔ cofibrations C i
have apply : Arrow.mk (X := initial.{v_1, u_1} C) (initial.to X) ≅ Arrow.mk i
Tactic: apply (cofibrations 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 : 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 : IsCofibrant.{v_1, u_1} X
⊢ IsCofibrant.{v_1, u_1} Y
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