mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyFiber

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : DecidableRel c.Rel
inst✝ : HasHomotopyFiber φ
i j : α
hij : c.symm.Rel i j
this : HasBinaryBiproduct (G.X j) (F.X i)
⊢ HasBinaryBiproduct (op (G.X j)) (op (F.X i))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : DecidableRel c.Rel
inst✝ : ∀ (i : α), HasBinaryBiproduct (K.X i) (K.X i)
i : α
⊢ HasBinaryBiproduct (op (K.X i)) (op (K.X i))

Tactic:
infer_instance

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 (𝟙 X) p

Tactic:
infer_instance

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
this✝ : HasLiftingProperty i p
this : HasLiftingProperty j p
⊢ HasLiftingProperty (i ≫ j) p

Tactic:
infer_instance

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:
infer_instance

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
this✝ : HasLiftingProperty p i
this : HasLiftingProperty p j
⊢ HasLiftingProperty p (i ≫ j)

Tactic:
infer_instance

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
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
p : X ⟶ Y
hp : T p
this : ∀ (j : J), HasLiftingProperty (f j) p
⊢ HasLiftingProperty (Limits.Sigma.map f) p

Tactic:
infer_instance

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
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
p : X ⟶ Y
hp : T p
this : ∀ (j : J), HasLiftingProperty p (f j)
⊢ HasLiftingProperty p (Limits.Pi.map f)

Tactic:
infer_instance

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
⊢ K.IsGE n

Tactic:
infer_instance

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
⊢ K.IsLE n

Tactic:
infer_instance

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:
infer_instance

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
⊢ (cofibrations C ⊓ weakEquivalences C).IsStableUnderRetracts

Tactic:
infer_instance

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
⊢ (fibrations C ⊓ weakEquivalences C).IsStableUnderRetracts

Tactic:
infer_instance

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).llp.IsStableUnderCobaseChange

Tactic:
infer_instance

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 : Cofibration (initial.to X)
⊢ Cofibration (initial.to X ≫ i)

Tactic:
infer_instance

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).rlp.IsStableUnderBaseChange

Tactic:
infer_instance

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).llp.IsMultiplicative

Tactic:
infer_instance

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).rlp.IsMultiplicative

Tactic:
infer_instance

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)
⊢ (trivialFibrations C).llp.IsStableUnderCobaseChange

Tactic:
infer_instance

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).rlp.IsStableUnderBaseChange

Tactic:
infer_instance

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).IsStableUnderComposition
X Y : C
p : X ⟶ Y
inst✝ : Fibration p
hY : Fibration (terminal.from Y)
⊢ Fibration (p ≫ terminal.from Y)

Tactic:
infer_instance

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)
⊢ (trivialFibrations C).llp.IsMultiplicative

Tactic:
infer_instance

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).rlp.IsMultiplicative

Tactic:
infer_instance

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
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst✝¹ : HasBinaryCoproduct X₁ X₂
inst✝ : HasBinaryCoproduct Y₁ Y₂
⊢ (cofibrations C).functorCategory (Discrete WalkingPair) (mapPair f₁ f₂)

Tactic:
rintro (_ | _) <;> assumption

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
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : HasBinaryProduct Y₁ Y₂
⊢ (fibrations C).functorCategory (Discrete WalkingPair) (mapPair f₁ f₂)

Tactic:
rintro (_ | _) <;> assumption

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)
inst✝¹ : (weakEquivalences C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderComposition
x✝ : C
⊢ WeakEquivalence (𝟙 x✝)

Tactic:
infer_instance

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)
inst✝¹ : (weakEquivalences C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderComposition
x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
x✝ : IsIso x✝¹
⊢ WeakEquivalence x✝¹

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : C
inst✝ : CategoryWithWeakEquivalences C
P : Cylinder A
⊢ WeakEquivalence P.π

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : trivialCofibrations C i
hp : Fibration p
left✝ : Cofibration i
right✝ : WeakEquivalence i
⊢ HasLiftingProperty i p

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝⁶ : HasBinaryCoproduct A A
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : HasInitial C
inst✝³ : (cofibrations C).IsStableUnderComposition
inst✝² : (cofibrations C).IsStableUnderCobaseChange
inst✝¹ : IsCofibrant A
inst✝ : P.IsGood
⊢ Cofibration (coprod.inl ≫ P.i)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝⁶ : HasBinaryCoproduct A A
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : HasInitial C
inst✝³ : (cofibrations C).IsStableUnderComposition
inst✝² : (cofibrations C).IsStableUnderCobaseChange
inst✝¹ : IsCofibrant A
inst✝ : P.IsGood
⊢ Cofibration (coprod.inr ≫ P.i)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : C
inst✝⁴ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝³ : HasBinaryCoproducts C
inst✝² : CategoryWithCofibrations C
inst✝¹ : P.IsGood
inst✝ : (cofibrations C).RespectsIso
⊢ Cofibration P.i

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : Cofibration i
hp : Fibration p ∧ WeakEquivalence p
this✝ : Fibration p
this : WeakEquivalence p
⊢ HasLiftingProperty i p

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
A : C
inst✝⁶ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
inst✝³ : (fibrations C).IsStableUnderComposition
inst✝² : (cofibrations C).RespectsIso
inst✝¹ : HasBinaryCoproducts C
inst✝ : P.IsVeryGood
⊢ Fibration P.π

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝³ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst✝¹ : Fibration f
inst✝ : WeakEquivalence w
h : RetractArrow f w
hw : (trivialCofibrations C).MapFactorizationData (fibrations C) w
⊢ (cofibrations C).rlp.IsStableUnderRetracts

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A : C
P : Cylinder A
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (codiag A)
⊢ Fibration h.p

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
A : C
P✝ : Cylinder A
inst✝¹ : IsCofibrant A
P P' : Cylinder A
inst✝ : P'.IsGood
⊢ WeakEquivalence (𝟙 A)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : C
inst✝ : CategoryWithWeakEquivalences C
P : PathObject A
⊢ WeakEquivalence P.ι

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝⁶ : HasBinaryProduct A A
inst✝⁵ : CategoryWithFibrations C
inst✝⁴ : HasTerminal C
inst✝³ : (fibrations C).IsStableUnderComposition
inst✝² : (fibrations C).IsStableUnderBaseChange
inst✝¹ : IsFibrant A
inst✝ : P.IsGood
⊢ Fibration (P.p ≫ prod.fst)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝⁶ : HasBinaryProduct A A
inst✝⁵ : CategoryWithFibrations C
inst✝⁴ : HasTerminal C
inst✝³ : (fibrations C).IsStableUnderComposition
inst✝² : (fibrations C).IsStableUnderBaseChange
inst✝¹ : IsFibrant A
inst✝ : P.IsGood
⊢ Fibration (P.p ≫ prod.snd)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : C
inst✝⁴ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝³ : HasBinaryProducts C
inst✝² : CategoryWithFibrations C
inst✝¹ : P.IsGood
inst✝ : (fibrations C).RespectsIso
⊢ Fibration P.p

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
A : C
inst✝⁶ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝⁵ : CategoryWithFibrations C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : (cofibrations C).IsStableUnderComposition
inst✝² : (fibrations C).RespectsIso
inst✝¹ : HasBinaryProducts C
inst✝ : P.IsVeryGood
⊢ Cofibration P.ι

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A : C
P : PathObject A
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (diag A)
⊢ Cofibration h.i

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
A : C
P✝ : PathObject A
inst✝¹ : IsFibrant A
P P' : PathObject A
inst✝ : P'.IsGood
⊢ WeakEquivalence (𝟙 A)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr P.i₁ P'.i₀
sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr P.i₁ P'.i₀)
⊢ Cofibration P'.i

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr P.i₁ P'.i₀
sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr P.i₁ P'.i₀)
this : Cofibration ψ
⊢ Cofibration (coprod.map P.i₀ (𝟙 A) ≫ ψ)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : (P.trans P').P ⟶ P.P ⨯ A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : ψ ≫ prod.map P.p₁ (𝟙 A) = pullback.snd P.p₁ P'.p₀ ≫ P'.p
sq : IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁ (P'.p ≫ prod.fst)
⊢ Fibration P'.p

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : (P.trans P').P ⟶ P.P ⨯ A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
fac : ψ ≫ prod.map P.p₁ (𝟙 A) = pullback.snd P.p₁ P'.p₀ ≫ P'.p
sq : IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁ (P'.p ≫ prod.fst)
this : Fibration ψ
⊢ Fibration (ψ ≫ prod.map P.p₀ (𝟙 A))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : HasFiniteLimits C
inst✝³ : HasFiniteColimits C
inst✝² : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : (trivialCofibrations C).MapFactorizationData (fibrations C) f
this✝⁴ : Cofibration hf.i
this✝³ : WeakEquivalence hf.i
φ : pushout hf.i (Arrow.Hom.left h.i) ⟶ Y := pushout.desc (hf.p ≫ Arrow.Hom.right h.i) w ⋯
this✝² : Fibration hf.p
this✝¹ : WeakEquivalence (pushout.inr hf.i (Arrow.Hom.left h.i) ≫ φ)
this✝ : WeakEquivalence φ
hp : RetractArrow hf.p φ
this : WeakEquivalence hf.p
⊢ WeakEquivalence (hf.i ≫ hf.p)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : HasFiniteLimits C
inst✝³ : HasFiniteColimits C
inst✝² : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialCofibrations C).rlp.IsStableUnderRetracts

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : HasFiniteLimits C
inst✝³ : HasFiniteColimits C
inst✝² : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialFibrations C).llp.IsStableUnderRetracts

Tactic:
infer_instance

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.LeftHomotopy f g
⊢ (Q.map P.ι).i₀ ≫ h.h.hom = f.hom

Tactic:
dsimp
        simp only [← h.h₀, ObjectProperty.FullSubcategory.comp_hom]

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
⊢ WeakEquivalence P.π

Tactic:
infer_instance

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 ≫ fac.i)

Tactic:
infer_instance

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:
dsimp
        simp only [← h.h₀, ObjectProperty.FullSubcategory.comp_hom]

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
⊢ WeakEquivalence P.ι

Tactic:
infer_instance

Goal state after: