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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ : C
P✝ : Precylinder X✝
Y✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : Precylinder X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ Q.i₀ ≫ ObjectProperty.homMk h.h = f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ : C
P✝ : Precylinder X✝
Y✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : Precylinder X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ Q.i₁ ≫ ObjectProperty.homMk h.h = g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ : C
P✝ : Precylinder X✝
Y✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : Precylinder X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ Q.i₁ ≫ ObjectProperty.homMk h.h = g

Tactic:
by ext; exact h.h₁

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : CategoryWithWeakEquivalences C
P : Cylinder X
inst✝¹ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝ : (weakEquivalences C).ContainsIdentities
f₀ f₁ : X ⟶ Y
h : P.LeftHomotopy f₀ f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
P : Cylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : (cofibrations C).MapFactorizationData (trivialFibrations C) P.i :=
  (cofibrations C).factorizationData (trivialFibrations C) P.i
⊢ Cofibration
    { I := d.Z, i₀ := coprod.inl ≫ d.i, i₁ := coprod.inr ≫ d.i, π := d.p ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
        weakEquivalence_π := ⋯ }.i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
P : Cylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
⊢ ∃ P', P'.IsGood ∧ Nonempty (P'.LeftHomotopy f g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A E B : C
P : Cylinder A
f₀ f₁ : A ⟶ B
inst✝² : IsCofibrant A
inst✝¹ : P.IsGood
h : P.LeftHomotopy f₀ f₁
p : E ⟶ B
inst✝ : Fibration p
l₀ : A ⟶ E
hl₀ : l₀ ≫ p = f₀
sq : CommSq l₀ P.i₀ p h.h
⊢ { h := sq.lift, h₀ := ⋯, h₁ := ⋯ }.h ≫ p = h.h

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : Cylinder X
h : P.LeftHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
this : L.map P.i₀ = L.map P.i₁
⊢ L.map f = L.map g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : Cylinder X
h : P.LeftHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ weakEquivalences C P.π

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
⊢ LeftHomotopyRel.FactorsThroughLocalization (weakEquivalences C)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : CategoryWithWeakEquivalences C
f g : X ⟶ Y
h : LeftHomotopyRel f g
Z : C
p : Y ⟶ Z
⊢ LeftHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
f g : X ⟶ Y
h : LeftHomotopyRel f g
⊢ ∃ P, P.IsGood ∧ Nonempty (P.LeftHomotopy f g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝ : LeftHomotopyRel f g
P : Cylinder X
left✝ : P.IsGood
h : P.LeftHomotopy f g
fac : (trivialCofibrations C).MapFactorizationData (fibrations C) P.π :=
  (trivialCofibrations C).factorizationData (fibrations C) P.π
P' : Cylinder X :=
  { I := fac.Z, i₀ := P.i₀ ≫ fac.i, i₁ := P.i₁ ≫ fac.i, π := fac.p, i₀_π := ⋯, i₁_π := ⋯, weakEquivalence_π := ⋯ }
⊢ Cofibration P'.i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h : LeftHomotopyRel f g
⊢ ∃ P, P.IsVeryGood ∧ Nonempty (P.LeftHomotopy f g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : CategoryWithWeakEquivalences C
f g : X ⟶ Y
h : LeftHomotopyRel f g
⊢ LeftHomotopyRel g f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f₀ f₁ f₂ : X ⟶ Y
inst✝ : IsCofibrant X
h : LeftHomotopyRel f₀ f₁
h' : LeftHomotopyRel f₁ f₂
⊢ LeftHomotopyRel f₀ f₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
⊢ coprod.desc (i ≫ P.i₀) (i ≫ P.i₁) ≫ P.π = Q.i ≫ Q.π ≫ i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
⊢ Q.i₀ ≫ sq.lift ≫ h.h = i ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
Y : C
P : PrepathObject Y
X : C
f₀ f₁ f₂ : X ⟶ Y
h : P.RightHomotopy f₀ f₁
P' : PrepathObject Y
h' : P'.RightHomotopy f₁ f₂
inst✝ : HasPullback P.p₁ P'.p₀
⊢ h.h ≫ P.p₁ = h'.h ≫ P'.p₀

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
⊢ Q.i₁ ≫ sq.lift ≫ h.h = i ≫ g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y✝ : C
P✝ : PrepathObject Y✝
X✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : PrepathObject Y
f g : X ⟶ Y
h : Q.RightHomotopy f g
⊢ h.h.hom ≫ (Q.map P.ι).p₀ = f.hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
⊢ LeftHomotopyRel (i ≫ f) (i ≫ g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y✝ : C
P✝ : PrepathObject Y✝
X✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : PrepathObject Y
f g : X ⟶ Y
h : Q.RightHomotopy f g
⊢ h.h.hom ≫ (Q.map P.ι).p₁ = g.hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
inst✝ : IsCofibrant X
f g : X ⟶ Y
⊢ mk f = mk g ↔ LeftHomotopyRel f g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y✝ : C
P✝ : PrepathObject Y✝
X✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : PrepathObject Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ ObjectProperty.homMk h.h ≫ Q.p₀ = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
⊢ F.map f₀ = F.map f₁

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y✝ : C
P✝ : PrepathObject Y✝
X✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : PrepathObject Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ ObjectProperty.homMk h.h ≫ Q.p₁ = g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y✝ : C
P✝ : PrepathObject Y✝
X✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : PrepathObject Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ ObjectProperty.homMk h.h ≫ Q.p₁ = g

Tactic:
by ext; exact h.h₁

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : CategoryWithWeakEquivalences C
P : PathObject Y
inst✝¹ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝ : (weakEquivalences C).ContainsIdentities
f₀ f₁ : X ⟶ Y
h : P.RightHomotopy f₀ f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Quotient r ⥤ E
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ F₁ = F₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
⊢ (functor r).IsLocalization W

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.π
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
P : PathObject Y
f g : X ⟶ Y
h : P.RightHomotopy f g
d : (trivialCofibrations C).MapFactorizationData (fibrations C) P.p :=
  (trivialCofibrations C).factorizationData (fibrations C) P.p
⊢ Fibration
    { P := d.Z, p₀ := d.p ≫ prod.fst, p₁ := d.p ≫ prod.snd, ι := P.ι ≫ d.i, ι_p₀ := ⋯, ι_p₁ := ⋯,
        weakEquivalence_ι := ⋯ }.p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.π
F : Quotient L.homRel ⥤ D := Quotient.lift L.homRel L ⋯
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
hf : W f
⊢ IsIso ((Quotient.functor L.homRel).map f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
P : PathObject Y
f g : X ⟶ Y
h : P.RightHomotopy f g
⊢ ∃ P', P'.IsGood ∧ Nonempty (P'.RightHomotopy f g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A B X : C
P : PathObject B
f₀ f₁ : A ⟶ B
inst✝² : IsFibrant B
inst✝¹ : P.IsGood
h : P.RightHomotopy f₀ f₁
i : A ⟶ X
inst✝ : Cofibration i
l₀ : X ⟶ B
hl₀ : i ≫ l₀ = f₀
sq : CommSq h.h i P.p₀ l₀
⊢ i ≫ { h := sq.lift, h₀ := ⋯, h₁ := ⋯ }.h = h.h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.π
⊢ L.IsLocalization W

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
this : L.map P.p₀ = L.map P.p₁
⊢ L.map f = L.map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.ι
⊢ L.IsLocalization W

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ weakEquivalences C P.ι

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
⊢ RightHomotopyRel.FactorsThroughLocalization (weakEquivalences C)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : CategoryWithWeakEquivalences C
f g : X ⟶ Y
h : RightHomotopyRel f g
Z : C
i : Z ⟶ X
⊢ RightHomotopyRel (i ≫ f) (i ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
inst✝ : Congruence r
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.ι
X Y : C
f₀ f₁ : X ⟶ Y
hf : (functor r).map f₀ = (functor r).map f₁
⊢ ∃ P x, W P.ι

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
f g : X ⟶ Y
h : RightHomotopyRel f g
⊢ ∃ P, P.IsGood ∧ Nonempty (P.RightHomotopy f g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝ : RightHomotopyRel f g
P : PathObject Y
left✝ : P.IsGood
h : P.RightHomotopy f g
fac : (cofibrations C).MapFactorizationData (trivialFibrations C) P.ι :=
  (cofibrations C).factorizationData (trivialFibrations C) P.ι
P' : PathObject Y :=
  { P := fac.Z, p₀ := fac.p ≫ P.p₀, p₁ := fac.p ≫ P.p₁, ι := fac.i, ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
⊢ Fibration P'.p

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h : RightHomotopyRel f g
⊢ ∃ P, P.IsVeryGood ∧ Nonempty (P.RightHomotopy f g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : CategoryWithWeakEquivalences C
f g : X ⟶ Y
h : RightHomotopyRel f g
⊢ RightHomotopyRel g f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f₀ f₁ f₂ : X ⟶ Y
inst✝ : IsFibrant Y
h : RightHomotopyRel f₀ f₁
h' : RightHomotopyRel f₁ f₂
⊢ RightHomotopyRel f₀ f₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝¹ : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
⊢ (h.h ≫ sq.lift) ≫ Q.p₀ = f ≫ p

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝¹ : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
⊢ (h.h ≫ sq.lift) ≫ Q.p₁ = g ≫ p

Tactic:
have := sq.fac_right =≫ prod.snd

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝¹ : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
this : (sq.lift ≫ Q.p) ≫ prod.snd = prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p) ≫ prod.snd
⊢ (h.h ≫ sq.lift) ≫ Q.p₁ = g ≫ p
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝¹ : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
⊢ (h.h ≫ sq.lift) ≫ Q.p₁ = g ≫ p

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
⊢ RightHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
inst✝ : IsFibrant Y
f g : X ⟶ Y
⊢ mk f = mk g ↔ RightHomotopyRel f g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z X Y : C
P : PrepathObject Y
f g : X ⟶ Y
h : P.RightHomotopy f g
⊢ (P.op.i₀ ≫ h.h.op).unop = f.op.unop

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z X Y : C
P : PrepathObject Y
f g : X ⟶ Y
h : P.RightHomotopy f g
⊢ (P.op.i₁ ≫ h.h.op).unop = g.op.unop

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z : C
X Y : Cᵒᵖ
P : PrepathObject Y
f g : X ⟶ Y
h : P.RightHomotopy f g
⊢ (P.unop.i₀ ≫ h.h.unop).op = f.unop.op

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z : C
X Y : Cᵒᵖ
P : PrepathObject Y
f g : X ⟶ Y
h : P.RightHomotopy f g
⊢ (P.unop.i₁ ≫ h.h.unop).op = g.unop.op

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z X Y : C
P : Precylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
⊢ (h.h.op ≫ P.op.p₀).unop = f.op.unop

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z X Y : C
P : Precylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
⊢ (h.h.op ≫ P.op.p₁).unop = g.op.unop

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z : C
X Y : Cᵒᵖ
P : Precylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
⊢ (h.h.unop ≫ P.unop.p₀).op = f.unop.op

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z : C
X Y : Cᵒᵖ
P : Precylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
⊢ (h.h.unop ≫ P.unop.p₁).op = g.unop.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{u_7, u_1} C
inst✝⁷ : Category.{u_6, u_2} D
inst✝⁶ : Category.{u_5, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n a a' : A
h : n + a = a'
X : C
⊢ G.map ((shiftIso hΦ n a a' h).hom.app X) =
    (commShiftIso G n).hom.app ((Φ a').obj X) ≫
      (shiftFunctor E n).map ((hΦ a').hom.app X) ≫ (F.shiftIso n a a' h).hom.app X ≫ (hΦ a).inv.app X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty Cᵒᵖ
inst✝ : P.IsStableUnderShift ℤ
n : ℤ
X : C
hX : P.unop X
⊢ n = - -n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty Cᵒᵖ
inst✝ : P.IsStableUnderShift ℤ
n : ℤ
X : C
hX : P.unop X
⊢ P.unop.shift n X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
T : Triangle Cᵒᵖ
hT : T ∈ Pretriangulated.distinguishedTriangles
h₁ : P.op T.obj₁
h₃ : P.op T.obj₃
⊢ P.op.isoClosure T.obj₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty Cᵒᵖ
inst✝ : P.IsTriangulatedClosed₂
T : Triangle C
hT : T ∈ Pretriangulated.distinguishedTriangles
h₁ : P.unop T.obj₁
h₃ : P.unop T.obj₃
⊢ P.unop.isoClosure T.obj₂

Tactic:
by

Goal state after: