mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
⊢ Function.Bijective (leftHomotopyClassToHom L)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
⊢ Function.Surjective L.map

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
h : L.map f = L.map g
⊢ rightHomotopyClassToHom L (RightHomotopyClass.mk f) = rightHomotopyClassToHom L (RightHomotopyClass.mk g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
⊢ RightHomotopyRel f g ↔ L.map f = L.map g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
h : L.map f = L.map g
⊢ leftHomotopyClassToHom L (LeftHomotopyClass.mk f) = leftHomotopyClassToHom L (LeftHomotopyClass.mk g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
f g : X ⟶ Y
⊢ LeftHomotopyRel f g ↔ L.map f = L.map g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
⊢ (weakEquivalences Cᵒᵖ).HasTwoOutOfThreeProperty

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (weakEquivalences Cᵒᵖ).IsStableUnderRetracts

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ (fibrations Cᵒᵖ).IsStableUnderRetracts

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (fibrations C).IsStableUnderRetracts
⊢ (cofibrations Cᵒᵖ).IsStableUnderRetracts

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (trivialCofibrations C).HasFactorization (fibrations C)
⊢ (cofibrations Cᵒᵖ).HasFactorization (trivialFibrations Cᵒᵖ)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (cofibrations C).HasFactorization (trivialFibrations C)
⊢ (trivialCofibrations Cᵒᵖ).HasFactorization (fibrations Cᵒᵖ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
X₁ X₂ X₃ X₄ : Over S
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : CommSq t l r b
inst✝ : ⋯.HasLift
sq' : CommSq (Over.Hom.left t) (Over.Hom.left l) (Over.Hom.left r) (Over.Hom.left b) := map (Over.forget S) sq
⊢ sq'.lift ≫ X₂.hom = X₃.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
X₁ X₂ X₃ X₄ : Over S
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : CommSq t l r b
inst✝ : ⋯.HasLift
sq' : CommSq (Over.Hom.left t) (Over.Hom.left l) (Over.Hom.left r) (Over.Hom.left b) := map (Over.forget S) sq
⊢ sq'.lift ≫ X₂.hom = X₃.hom

Tactic:
by rw [← Over.w b, ← sq'.fac_right_assoc, Over.w r]

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
X₁ X₂ X₃ X₄ : Over S
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : CommSq t l r b
inst✝ : ⋯.HasLift
⊢ sq.HasLift

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {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✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
⊢ WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
⊢ (weakEquivalences (BifibrantObject C)).IsInvertedBy F ↔
    ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
⊢ (weakEquivalences (BifibrantObject C)).IsInvertedBy toHoCat

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
hF : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
⊢ ∀ (x y : BifibrantObject C) (f₁ f₂ : x ⟶ y), homRel C f₁ f₂ → F.map f₁ = F.map f₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ weakEquivalences (BifibrantObject C) f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : X ⟶ Y
h : RightHomotopyRel x✝¹ x✝
⊢ toHoCat.map (homMk x✝¹) = toHoCat.map (homMk x✝)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : (toHoCat.obj (mk X)).as ⟶ (toHoCat.obj (mk Y)).as
h : HomRel.CompClosure (homRel C) x✝¹ x✝
⊢ RightHomotopyClass.mk x✝¹.hom = RightHomotopyClass.mk x✝.hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
⊢ Function.LeftInverse (Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯) (Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
⊢ Function.RightInverse (Quot.lift (fun f ↦ RightHomotopyClass.mk f.hom) ⋯)
    (Quot.lift (fun f ↦ toHoCat.map (homMk f)) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
f : X ⟶ Y
⊢ homEquivLeft (LeftHomotopyClass.mk f) = toHoCat.map (homMk f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
x✝³ x✝² : BifibrantObject C
x✝¹ x✝ : x✝³ ⟶ x✝²
h : homRel C x✝¹ x✝
⊢ (BifibrantObject.ιFibrantObject ⋙ FibrantObject.toHoCat).map x✝¹ =
    (BifibrantObject.ιFibrantObject ⋙ FibrantObject.toHoCat).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {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✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : Cofibration (pushout.inl f i ≫ h.i)
⊢ WeakEquivalence (pushout.inl f i ≫ h.i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
x✝³ x✝² : BifibrantObject C
x✝¹ x✝ : x✝³ ⟶ x✝²
h : homRel C x✝¹ x✝
⊢ (BifibrantObject.ιCofibrantObject ⋙ CofibrantObject.toHoCat).map x✝¹ =
    (BifibrantObject.ιCofibrantObject ⋙ CofibrantObject.toHoCat).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (terminal.from X.obj) :=
  (trivialCofibrations C).factorizationData (fibrations C) (terminal.from X.obj)
this : IsCofibrant h.Z
⊢ IsFibrant h.Z

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ ∃ Y i, Cofibration (ι.map i) ∧ WeakEquivalence (ι.map i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence X.iBifibrantResolutionObj

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
⊢ ι.map (f ≫ X₂.iBifibrantResolutionObj) ≫
      terminal.from (ι.obj (BifibrantObject.ιCofibrantObject.obj X₂.bifibrantResolutionObj)) =
    X₁.iBifibrantResolutionObj.hom ≫ terminal.from (BifibrantObject.ιCofibrantObject.obj X₁.bifibrantResolutionObj).obj

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {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✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : Cofibration (pushout.inl f i ≫ h.i)
this : WeakEquivalence (pushout.inl f i ≫ h.i)
⊢ i ≫ pushout.inr f i ≫ h.i ≫ sq'.lift = f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
sq :
  CommSq (ι.map (f ≫ X₂.iBifibrantResolutionObj)) X₁.iBifibrantResolutionObj.hom
    (terminal.from (ι.obj (BifibrantObject.ιCofibrantObject.obj X₂.bifibrantResolutionObj)))
    (terminal.from (BifibrantObject.ιCofibrantObject.obj X₁.bifibrantResolutionObj).obj)
⊢ X₁.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map (BifibrantObject.homMk sq.lift) =
    f ≫ X₂.iBifibrantResolutionObj

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
⊢ ∃ g, X₁.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map g = f ≫ X₂.iBifibrantResolutionObj

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h : ∀ {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✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
inst✝ : WeakEquivalence f
⊢ WeakEquivalence (bifibrantResolutionMap f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h✝ : ∀ {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✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (pullback.lift f i ⋯) :=
  (trivialCofibrations C).factorizationData (fibrations C) (pullback.lift f i ⋯)
sq' : CommSq h.i i (h.p ≫ pullback.snd p g) (𝟙 B)
⊢ WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
Y : BifibrantObject.HoCat C
f g : BifibrantObject.toHoCat.obj X.bifibrantResolutionObj ⟶ Y
h :
  toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map f =
    toHoCat.map X.iBifibrantResolutionObj ≫ BifibrantObject.HoCat.ιCofibrantObject.map g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ toHoCat.map X.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (BifibrantObject.toHoCat.map (bifibrantResolutionMap (𝟙 X))) =
    toHoCat.map X.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (𝟙 (BifibrantObject.toHoCat.obj X.bifibrantResolutionObj))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ X₃ : CofibrantObject C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ toHoCat.map X₁.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (BifibrantObject.toHoCat.map (bifibrantResolutionMap (f ≫ g))) =
    toHoCat.map X₁.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map
        (BifibrantObject.toHoCat.map (bifibrantResolutionMap f) ≫
          BifibrantObject.toHoCat.map (bifibrantResolutionMap g))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h✝ : ∀ {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✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (pullback.lift f i ⋯) :=
  (trivialCofibrations C).factorizationData (fibrations C) (pullback.lift f i ⋯)
sq' : CommSq h.i i (h.p ≫ pullback.snd p g) (𝟙 B)
h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g)
h₂ : Fibration (h.p ≫ pullback.snd p g)
⊢ WeakEquivalence (h.p ≫ pullback.snd p g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ ∀ (x y : CofibrantObject C) (f₁ f₂ : x ⟶ y),
    homRel C f₁ f₂ → bifibrantResolution'.map f₁ = bifibrantResolution'.map f₂

Tactic:
intro X Y f g h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h : homRel C f g
⊢ bifibrantResolution'.map f = bifibrantResolution'.map g
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ ∀ (x y : CofibrantObject C) (f₁ f₂ : x ⟶ y),
    homRel C f₁ f₂ → bifibrantResolution'.map f₁ = bifibrantResolution'.map f₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : HoCat C
⊢ WeakEquivalence (HoCat.adjUnit.app X)

Tactic:
obtain ⟨X, rfl⟩ := toHoCat_obj_surjective X
  rw [HoCat.adjUnit_app, weakEquivalence_toHoCat_map_iff,
    weakEquivalence_iff_of_objectProperty]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : HoCat C
⊢ WeakEquivalence (HoCat.adjUnit.app X)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
inst✝ : CategoryWithCofibrations C
X Y : Over S
f : X ⟶ Y
⊢ Cofibration f ↔ Cofibration (Over.Hom.left f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithCofibrations C
X Y : Over S
f : X ⟶ Y
inst✝ : Cofibration f
⊢ Cofibration (Over.Hom.left f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithCofibrations C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ (cofibrations (Over S)).IsStableUnderRetracts

Tactic:
rw [cofibrations_over_def, MorphismProperty.over_eq_inverseImage]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithCofibrations C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ ((cofibrations C).inverseImage (Over.forget S)).IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithCofibrations C
inst✝ : (cofibrations C).IsStableUnderRetracts
⊢ (cofibrations (Over S)).IsStableUnderRetracts

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
inst✝ : CategoryWithFibrations C
X Y : Over S
f : X ⟶ Y
⊢ Fibration f ↔ Fibration (Over.Hom.left f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ : BifibrantObject C
f : X₁ ⟶ X₂
⊢ f ≫ BifibrantObject.homMk (mk X₂.obj).iBifibrantResolutionObj.hom =
    BifibrantObject.homMk (mk X₁.obj).iBifibrantResolutionObj.hom ≫
      bifibrantResolutionMap (BifibrantObject.ιCofibrantObject.map f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithFibrations C
X Y : Over S
f : X ⟶ Y
inst✝ : Fibration f
⊢ Fibration (Over.Hom.left f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithFibrations C
inst✝ : (fibrations C).IsStableUnderRetracts
⊢ (fibrations (Over S)).IsStableUnderRetracts

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
inst✝ : CategoryWithWeakEquivalences C
X Y : Over S
f : X ⟶ Y
⊢ WeakEquivalence f ↔ WeakEquivalence (Over.Hom.left f)

Tactic:
by

Goal state after: