awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this_3 : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_4 :
  WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)
this : WeakEquivalence φ
⊢ weakEquivalences C f
have have : ∀ (hp : RetractArrow (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C)) φ), weakEquivalences C f
Tactic: have hp : RetractArrow hf.p φ :=
      { i := Arrow.homMk (pushout.inl _ _) h.i.right
        r := Arrow.homMk (pushout.desc (𝟙 _) (h.r.left ≫ hf.i) (by simp)) h.r.right }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this_3 : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_4 :
  WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)
this : WeakEquivalence φ
hp : RetractArrow (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C)) φ
⊢ weakEquivalences C f
have this₁ : WeakEquivalence (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: have := mk'.cm3a_aux hp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : MapFactorizationData (trivialCofibrations C) (fibrations C) f
this_1 : Cofibration (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_2 : WeakEquivalence (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C))
φ : pushout (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ⟶ Y :=
  pushout.desc (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ Arrow.Hom.right h.i) w ⋯
this_3 : Fibration (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
this_4 :
  WeakEquivalence (pushout.inr (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C)) (Arrow.Hom.left h.i) ≫ φ)
this_5 : WeakEquivalence φ
hp : RetractArrow (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C)) φ
this : WeakEquivalence (hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
⊢ weakEquivalences C f
have rw : WeakEquivalence
  (hf.i (W₁ := trivialCofibrations C) (W₂ := fibrations C) ≫ hf.p (W₁ := trivialCofibrations C) (W₂ := fibrations C))
Tactic: rw [← weakEquivalence_iff, ← hf.fac]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsStableUnderRetracts.{v, u} (fibrations C)
have rw : IsStableUnderRetracts.{v, u} (rlp (trivialCofibrations C))
Tactic: rw [← rlp_eq_of_wfs (trivialCofibrations C) (fibrations C)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : CategoryWithCofibrations.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
inst_4 : HasFiniteLimits.{v, u} C
inst_5 : HasFiniteColimits.{v, u} C
inst_6 : HasTwoOutOfThreeProperty.{v, u} (weakEquivalences C)
inst_7 : IsWeakFactorizationSystem.{v, u} (cofibrations C) (trivialFibrations C)
inst_8 : IsWeakFactorizationSystem.{v, u} (trivialCofibrations C) (fibrations C)
⊢ IsStableUnderRetracts.{v, u} (cofibrations C)
have rw : IsStableUnderRetracts.{v, u} (llp (trivialFibrations C))
Tactic: rw [← llp_eq_of_wfs (cofibrations C) (trivialFibrations C)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Bifibrant (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
inst_4 : IsCofibrant.{v, u} X
inst_5 : IsCofibrant.{v, u} Y
f : X ⟶ Y
⊢ WeakEquivalence (C := CofibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ WeakEquivalence f
have simp : weakEquivalences (CofibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ weakEquivalences C f
Tactic: simp only [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Bifibrant (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithFibrations.{v, u} C
inst_2 : HasTerminal.{v, u} C
inst_3 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
inst_4 : IsFibrant.{v, u} X
inst_5 : IsFibrant.{v, u} Y
f : X ⟶ Y
⊢ WeakEquivalence (C := FibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ WeakEquivalence f
have simp : weakEquivalences (FibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ weakEquivalences C f
Tactic: simp only [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Bifibrant (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CategoryWithCofibrations.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CategoryWithFibrations.{v, u} C
inst_4 : HasTerminal.{v, u} C
inst_5 : CategoryWithWeakEquivalences.{v, u} C
X Y : C
inst_6 : IsCofibrant.{v, u} X
inst_7 : IsFibrant.{v, u} X
inst_8 : IsCofibrant.{v, u} Y
inst_9 : IsFibrant.{v, u} Y
f : X ⟶ Y
⊢ WeakEquivalence (C := BifibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ WeakEquivalence f
have simp : weakEquivalences (BifibrantObject.{v, u} C) (X := mk X) (Y := mk Y) (homMk f) ↔ weakEquivalences C f
Tactic: simp only [weakEquivalence_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : BifibrantObject.{v, u} C
f g : X ⟶ Y
⊢ homRel C f g ↔ LeftHomotopyRel f.hom g.hom
have rw : RightHomotopyRel f.hom g.hom ↔ LeftHomotopyRel f.hom g.hom
Tactic: rw [homRel_iff_rightHomotopyRel, leftHomotopyRel_iff_rightHomotopyRel]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : BifibrantObject.{v, u} C
f g : X ⟶ Y
rw : RightHomotopyRel f.hom g.hom ↔ LeftHomotopyRel f.hom g.hom
⊢ homRel C f g ↔ LeftHomotopyRel f.hom g.hom
have rw₁ : RightHomotopyRel f.hom g.hom ↔ RightHomotopyRel f.hom g.hom
Tactic: rw [homRel_iff_rightHomotopyRel, leftHomotopyRel_iff_rightHomotopyRel]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
⊢ MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F ↔
    ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
have refine_1 : ∀ (H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F) (K L : BifibrantObject.{v, u} C)
  (f g : K ⟶ L) (h : homRel C f g), F.map f = F.map g
Tactic: refine ⟨fun H K L f g h ↦ ?_, fun h X Y f hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
refine_1 :
  ∀ (H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F) (K L : BifibrantObject.{v, u} C)
    (f g : K ⟶ L) (h : homRel C f g), F.map f = F.map g
⊢ MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F ↔
    ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
have refine_2 : ∀ (h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g)
  (X Y : BifibrantObject.{v, u} C) (f : X ⟶ Y) (hf : weakEquivalences (BifibrantObject.{v, u} C) f), IsIso (F.map f)
Tactic: refine ⟨fun H K L f g h ↦ ?_, fun h X Y f hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h : homRel C f g
⊢ F.map f = F.map g
have refine_1 : ∀ (P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))),
  P.IsVeryGood → ∀ (h : P.RightHomotopy f.hom g.hom), F.map f = F.map g
Tactic: obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
⊢ F.map f = F.map g
have this : IsCofibrant.{v, u} P.P
Tactic: have := isCofibrant_of_cofibration P.ι
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this : IsCofibrant.{v, u} P.P
⊢ weakEquivalences (BifibrantObject.{v, u} C) (X := mk (L.obj (P := bifibrantObjects C))) (Y := mk P.P) (homMk P.ι)
have rw : WeakEquivalence (X :=
  ObjectProperty.FullSubcategory.obj (P := bifibrantObjects C) (mk (L.obj (P := bifibrantObjects C)))) (Y :=
  ObjectProperty.FullSubcategory.obj (P := bifibrantObjects C) (mk P.P)) (InducedCategory.Hom.hom (homMk P.ι))
Tactic: rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this : IsCofibrant.{v, u} P.P
⊢ F.map f = F.map g
have this₁ : IsIso (X := F.obj (mk (L.obj (P := bifibrantObjects C)))) (Y := F.obj (mk P.P)) (F.map (homMk P.ι))
Tactic: have : IsIso (F.map (homMk P.ι)) := H _ (by
      rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
      exact inferInstanceAs (WeakEquivalence P.ι))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this_1 : IsCofibrant.{v, u} P.P
this : IsIso (X := F.obj (mk (L.obj (P := bifibrantObjects C)))) (Y := F.obj (mk P.P)) (F.map (homMk P.ι))
⊢ F.map f = F.map g
have refine_1 : Eq (α := F.obj K ⟶ F.obj L)
  (CategoryStruct.comp (Y := F.obj (mk P.P)) (F.map (homMk h.h)) (F.map (homMk P.p₀)) : F.obj K ⟶ F.obj L)
  (CategoryStruct.comp (Y := F.obj (mk P.P)) (F.map (homMk h.h)) (F.map (homMk P.p₁)) : F.obj K ⟶ F.obj L)
Tactic: simp only [show f = homMk h.h ≫ homMk P.p₀ by cat_disch,
      show g = homMk h.h ≫ homMk P.p₁ by cat_disch, Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
H : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
K L : BifibrantObject.{v, u} C
f g : K ⟶ L
h_1 : homRel C f g
P : PathObject.{v, u} (L.obj (P := bifibrantObjects C))
left : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this_1 : IsCofibrant.{v, u} P.P
this : IsIso (X := F.obj (mk (L.obj (P := bifibrantObjects C)))) (Y := F.obj (mk P.P)) (F.map (homMk P.ι))
⊢ Eq (α := F.obj K ⟶ F.obj L)
    (CategoryStruct.comp (Y := F.obj (mk P.P)) (F.map (homMk h.h)) (F.map (homMk P.p₀)) : F.obj K ⟶ F.obj L)
    (CategoryStruct.comp (Y := F.obj (mk P.P)) (F.map (homMk h.h)) (F.map (homMk P.p₁)) : F.obj K ⟶ F.obj L)
have refine_1 : Eq (α := F.obj (mk P.P) ⟶ F.obj L) (F.map (homMk P.p₀) : F.obj (mk P.P) ⟶ F.obj L)
  (F.map (homMk P.p₁) : F.obj (mk P.P) ⟶ F.obj L)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : weakEquivalences (BifibrantObject.{v, u} C) f
⊢ IsIso (F.map f)
have hf₁ : WeakEquivalence f.hom
Tactic: rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
⊢ IsIso (F.map f)
have refine_2 : ∀ (g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C))
  (h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C))))
  (h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))), IsIso (F.map f)
Tactic: obtain ⟨g', h₁, h₂⟩ := RightHomotopyClass.whitehead f.hom
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
⊢ IsIso (F.map f)
have refine_2 : Eq (α := F.obj X ⟶ F.obj X) (F.map f ≫ F.map (homMk g') : F.obj X ⟶ F.obj X) (𝟙 (F.obj X) : F.obj X ⟶ F.obj X)
Tactic: refine ⟨F.map (homMk g'), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
refine_2 :
  Eq (α := F.obj X ⟶ F.obj X) (F.map f ≫ F.map (homMk g') : F.obj X ⟶ F.obj X) (𝟙 (F.obj X) : F.obj X ⟶ F.obj X)
⊢ IsIso (F.map f)
have refine_2₁ : Eq (α := F.obj Y ⟶ F.obj Y) (F.map (homMk g') ≫ F.map f : F.obj Y ⟶ F.obj Y) (𝟙 (F.obj Y) : F.obj Y ⟶ F.obj Y)
Tactic: refine ⟨F.map (homMk g'), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
⊢ Eq (α := F.obj X ⟶ F.obj X) (F.map f ≫ F.map (homMk g') : F.obj X ⟶ F.obj X) (𝟙 (F.obj X) : F.obj X ⟶ F.obj X)
have refine_2 : F.map (f ≫ homMk g') = F.map (𝟙 X)
Tactic: rw [← F.map_comp, ← F.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
⊢ F.map (f ≫ homMk g') = F.map (𝟙 X)
have refine_2 : homRel C (Y := X) (f ≫ homMk g' : X ⟶ X) (𝟙 X : X ⟶ X)
Tactic: apply h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
⊢ Eq (α := F.obj Y ⟶ F.obj Y) (F.map (homMk g') ≫ F.map f : F.obj Y ⟶ F.obj Y) (𝟙 (F.obj Y) : F.obj Y ⟶ F.obj Y)
have refine_2 : F.map (homMk g' ≫ f) = F.map (𝟙 Y)
Tactic: rw [← F.map_comp, ← F.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
h : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj (P := bifibrantObjects C) ⟶ X.obj (P := bifibrantObjects C)
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 (X.obj (P := bifibrantObjects C)))
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 (Y.obj (P := bifibrantObjects C)))
⊢ F.map (homMk g' ≫ f) = F.map (𝟙 Y)
have refine_2 : homRel C (X := Y) (homMk g' ≫ f : Y ⟶ Y) (𝟙 Y : Y ⟶ Y)
Tactic: apply h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
⊢ MorphismProperty.IsInvertedBy.{v, v, u, u} (C := BifibrantObject.{v, u} C)
    (weakEquivalences (BifibrantObject.{v, u} C)) toHoCat
have rw : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L),
  homRel C f g →
    Eq (α := Functor.obj toHoCat K ⟶ Functor.obj toHoCat L) (CategoryTheory.Functor.map toHoCat f)
      (CategoryTheory.Functor.map toHoCat g)
Tactic: rw [inverts_iff_factors]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
F : CategoryTheory.Functor.{v, v_1, u, u_1} (BifibrantObject.{v, u} C) D
hF : MorphismProperty.IsInvertedBy (weakEquivalences (BifibrantObject.{v, u} C)) F
⊢ ∀ (x y : BifibrantObject.{v, u} C) (f₁ f₂ : x ⟶ y), homRel C f₁ f₂ → F.map f₁ = F.map f₂
have rwa : ∀ (hF : ∀ ⦃K L : BifibrantObject.{v, u} C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g)
  (x y : BifibrantObject.{v, u} C) (f₁ f₂ : x ⟶ y), homRel C f₁ f₂ → F.map f₁ = F.map f₂
Tactic: rwa [inverts_iff_factors] at hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ModelCategory.{v, u} C
X Y : BifibrantObject.{v, u} C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ weakEquivalences (BifibrantObject.{v, u} C) f
have rwa : ∀ (hf : weakEquivalences (BifibrantObject.{v, u} C) f), weakEquivalences (BifibrantObject.{v, u} C) f
Tactic: rwa [weakEquivalence_iff] at hf
Cleared hypotheses: hf