mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
X x✝¹ x✝ : C
p : x✝¹ ⟶ x✝
hp : T p
⊢ HasLiftingProperty (𝟙 X) p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
X✝ Y✝ Z✝ : C
i : X✝ ⟶ Y✝
j : Y✝ ⟶ Z✝
hi : T.llp i
hj : T.llp j
x✝¹ x✝ : C
p : x✝¹ ⟶ x✝
hp : T p
⊢ HasLiftingProperty (i ≫ j) p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
X x✝¹ x✝ : C
p : x✝¹ ⟶ x✝
hp : T p
⊢ HasLiftingProperty p (𝟙 X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
X✝ Y✝ Z✝ : C
i : X✝ ⟶ Y✝
j : Y✝ ⟶ Z✝
hi : T.rlp i
hj : T.rlp j
x✝¹ x✝ : C
p : x✝¹ ⟶ x✝
hp : T p
⊢ HasLiftingProperty p (i ≫ j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
⊢ T.llp.IsStableUnderCoproductsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
⊢ X.IsLE n ↔ ∀ (i : ℤ), n < i → IsZero ((homologyFunctor C i).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
⊢ T.rlp.IsStableUnderProductsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T ≤ T.rlp.llp

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts ≤ T.rlp.llp

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n i : ℤ
hi : i < n
hX : X.IsGE n
⊢ IsZero ((homologyFunctor C i).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts.rlp = T.rlp

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n i : ℤ
hi : n < i
hX : X.IsLE n
⊢ IsZero ((homologyFunctor C i).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type w
⊢ T.colimitsOfShape (Discrete J) ≤ T.rlp.llp

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
n : ℤ
⊢ (Q.obj K).IsGE n ↔ K.IsGE n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
n : ℤ
⊢ (Q.obj K).IsLE n ↔ K.IsLE n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ coproducts.{w, v, u} T ≤ T.rlp.llp

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
K : CochainComplex C ℤ
n : ℤ
inst✝ : K.IsGE n
⊢ (Q.obj K).IsGE n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
⊢ ∃ α, δ m n α = ↑z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
⊢ -1 + 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ (coproducts.{w, v, u} T).rlp = T.rlp

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
K : CochainComplex C ℤ
n : ℤ
inst✝ : K.IsLE n
⊢ (Q.obj K).IsLE n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
β : Cochain L L (-1)
hβ : δ (-1) 0 β = ↑(Cocycle.ofHom (𝟙 L))
⊢ n + -1 = m

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.retracts.rlp = T.rlp

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
β : Cochain L L (-1)
hβ : δ (-1) 0 β = ↑(Cocycle.ofHom (𝟙 L))
⊢ -1 + 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
⊢ ((singleFunctor C n).obj X).IsGE n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
inst✝ : Nonempty ι
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p → (ofHoms fun x ↦ i).rlp p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
β : Cochain L L (-1)
hβ : δ (-1) 0 β = ↑(Cocycle.ofHom (𝟙 L))
⊢ δ m n ((↑z).comp β ⋯) = ↑z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
⊢ ((singleFunctor C n).obj X).IsLE n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
inst✝ : Nonempty ι
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p → (ofHoms fun x ↦ p).llp i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
⊢ ∃ α, δ m n α = ↑z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
hX : X.IsLE n
⊢ ∃ K, ∃ (_ : K.IsStrictlyLE n), Nonempty (X ≅ Q.obj K)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
hX : X.IsGE n
⊢ ∃ K, ∃ (_ : K.IsStrictlyGE n), Nonempty (X ≅ Q.obj K)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
G : C ⥤ D
inst✝ : G.IsEquivalence
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) (G.map p) ↔ HasLiftingProperty i p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X : DerivedCategory C
a b : ℤ
inst✝¹ : X.IsGE a
inst✝ : X.IsLE b
K : CochainComplex C ℤ
hK : K.IsStrictlyLE b
e : X ≅ Q.obj K
⊢ K.IsGE a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X : DerivedCategory C
a b : ℤ
inst✝¹ : X.IsGE a
inst✝ : X.IsLE b
⊢ ∃ K, ∃ (_ : K.IsStrictlyGE a) (_ : K.IsStrictlyLE b), Nonempty (X ≅ Q.obj K)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
inst✝¹ : X.IsGE n
inst✝ : X.IsLE n
⊢ ∃ Y, Nonempty (X ≅ (singleFunctor C n).obj Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
i : X ⟶ Y
p : Y ⟶ Z
h : i ≫ p = f
inst✝ : HasLiftingProperty f p
⊢ i ≫ p = f ≫ 𝟙 Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
i : X ⟶ Y
p : Y ⟶ Z
h : i ≫ p = f
inst✝ : HasLiftingProperty i f
⊢ 𝟙 X ≫ f = i ≫ p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
⊢ W₁ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₂.IsStableUnderRetracts
h₂ : W₂ ≤ W₁.rlp
X Y : C
p : X ⟶ Y
hp : W₁.rlp p
⊢ W₂ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²³ : Category.{v_1, u_1} C₁
inst✝²² : Category.{v_2, u_2} C₂
inst✝²¹ : Category.{v_3, u_5} C₃
inst✝²⁰ : Category.{v_4, u_6} C₄
inst✝¹⁹ : Category.{v_6, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
h₂ : c₁.π c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
h₃ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.r c₂ c₃ c₁₂ c₄ (i₁, c₂.next i₂, i₃) = j'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialFibrations C f ↔ Fibration f ∧ WeakEquivalence f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithCofibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialCofibrations C f ↔ Cofibration f ∧ WeakEquivalence f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : CategoryWithCofibrations C
⊢ Fibration f.op ↔ Cofibration f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithCofibrations C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Cofibration f.unop ↔ Fibration f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithCofibrations C
inst✝ : Cofibration f
⊢ Fibration f.op

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithCofibrations C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : Fibration f
⊢ Cofibration f.unop

Tactic:
rwa [cofibration_unop_iff]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithCofibrations C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : Fibration f
⊢ Cofibration f.unop

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : CategoryWithFibrations C
⊢ Cofibration f.op ↔ Fibration f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithFibrations C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Fibration f.unop ↔ Cofibration f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithFibrations C
inst✝ : Fibration f
⊢ Cofibration f.op

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithFibrations C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : Cofibration f
⊢ Fibration f.unop

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : CategoryWithWeakEquivalences C
⊢ WeakEquivalence f.op ↔ WeakEquivalence f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : WeakEquivalence f
⊢ WeakEquivalence f.op

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithWeakEquivalences C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ WeakEquivalence f.unop

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
P : ObjectProperty C
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ WeakEquivalence f ↔ WeakEquivalence f.hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithWeakEquivalences C
P : ObjectProperty C
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ WeakEquivalence f.hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithWeakEquivalences C
P : ObjectProperty C
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ WeakEquivalence (P.ι.map f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : (cofibrations C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (trivialCofibrations C).IsStableUnderRetracts

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithFibrations C
inst✝¹ : (fibrations C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (trivialFibrations C).IsStableUnderRetracts

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : WeakEquivalence g
hfg : WeakEquivalence (f ≫ g)
⊢ WeakEquivalence f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : WeakEquivalence f
hfg : WeakEquivalence (f ≫ g)
⊢ WeakEquivalence g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CategoryWithWeakEquivalences C
inst✝¹ : (weakEquivalences C).HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
fg : X ⟶ Z
fac : f ≫ g = fg
inst✝ : WeakEquivalence g
hfg : WeakEquivalence fg
⊢ WeakEquivalence f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : CategoryWithCofibrations C
inst✝¹ : HasInitial C
inst✝ : (cofibrations C).RespectsIso
A X : C
i : A ⟶ X
hA : IsInitial A
⊢ IsCofibrant X ↔ Cofibration i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : (weakEquivalences C).HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
fg : X ⟶ Z
fac : f ≫ g = fg
inst✝¹ : WeakEquivalence f
inst✝ : WeakEquivalence fg
⊢ WeakEquivalence g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialCofibrations C).IsStableUnderCobaseChange

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
inst✝¹ : (cofibrations C).IsStableUnderComposition
X Y : C
i : X ⟶ Y
inst✝ : Cofibration i
hX : IsCofibrant X
⊢ IsCofibrant Y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (fibrations C).IsStableUnderBaseChange

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialCofibrations C).IsMultiplicative

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hY : IsCofibrant Y
⊢ Cofibration coprod.inl

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (fibrations C).IsMultiplicative

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
J : Type w
⊢ (trivialCofibrations C).IsStableUnderCoproductsOfShape J

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hX : IsCofibrant X
⊢ Cofibration coprod.inr

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
J : Type w
⊢ (fibrations C).IsStableUnderProductsOfShape J

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : CategoryWithFibrations C
inst✝¹ : HasTerminal C
inst✝ : (fibrations C).RespectsIso
X Y : C
p : X ⟶ Y
hY : IsTerminal Y
⊢ IsFibrant X ↔ Fibration p

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
⊢ (cofibrations C).IsStableUnderCobaseChange

Tactic:
by

Goal state after: