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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
x✝ : Homotopy f g
⊢ (fun h ↦ h.ofExtend) ((fun h ↦ h.extend e) x✝) = x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
x✝ : Homotopy (extendMap f e) (extendMap g e)
⊢ (fun h ↦ h.extend e) ((fun h ↦ h.ofExtend) x✝) = x✝

Tactic:
by simp

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
⊢ ∀ (n a n' : ℤ), a + n' = n → ∀ (X : DerivedCategory C), (∃ K x, K.IsStrictlyLE n) → ∃ K x, K.IsStrictlyLE n'

Tactic:
rintro n a n' h X ⟨K, e, _⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n a n' : ℤ
h : a + n' = n
X : DerivedCategory C
K : CochainComplex C ℤ
e : X ≅ Q.obj K
h✝ : K.IsStrictlyLE n
⊢ ∃ K x, K.IsStrictlyLE n'
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ ∀ (n a n' : ℤ), a + n' = n → ∀ (X : DerivedCategory C), (∃ K x, K.IsStrictlyGE n) → ∃ K x, K.IsStrictlyGE n'

Tactic:
rintro n a n' h X ⟨K, e, _⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n a n' : ℤ
h : a + n' = n
X : DerivedCategory C
K : CochainComplex C ℤ
e : X ≅ Q.obj K
h✝ : K.IsStrictlyGE n
⊢ ∃ K x, K.IsStrictlyGE n'
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 Y : DerivedCategory C
f : X ⟶ Y
K : CochainComplex C ℤ
e₁ : X ≅ Q.obj K
h✝¹ : K.IsStrictlyLE 0
L : CochainComplex C ℤ
e₂ : Y ≅ Q.obj L
h✝ : L.IsStrictlyGE 1
⊢ 0 < 1

Tactic:
by simp

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 Y : DerivedCategory C
f : X ⟶ Y
K : CochainComplex C ℤ
e₁ : X ≅ Q.obj K
h✝¹ : K.IsStrictlyLE 0
L : CochainComplex C ℤ
e₂ : Y ≅ Q.obj L
h✝ : L.IsStrictlyGE 1
⊢ (e₁.inv ≫ f) ≫ e₂.hom = 0

Tactic:
apply (subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE K L 0 1 (by simp)).elim

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)
inst✝ : K.HasPathObject
hc : ∀ (i : α), ∃ j, c.Rel i j
⊢ ι K ≫ π₀ K = 𝟙 K

Tactic:
by simp

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
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ (triangleOfSES h).mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (Iso.refl (triangleOfSES h).obj₁).hom =
    (asIso (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13))).hom ≫
      (Triangle.mk (Q.map (K.ιTruncLE 0) ≫ e₂.hom) (e₂.inv ≫ Q.map (K.πTruncGE 1))
          (inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13)) ≫
            (triangleOfSES h).mor₃)).mor₃

Tactic:
by simp

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
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ 0 + n = n

Tactic:
by simp

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 simp

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 simp

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₁ : Fibration f₁
h₂ : Fibration f₂
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : HasBinaryProduct Y₁ Y₂
⊢ Fibration (prod.map f₁ f₂)

Tactic:
rw [fibration_iff] at h₁ h₂ ⊢
  apply MorphismProperty.limMap
  rintro (_ | _) <;> assumption

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : C
P P' : Precylinder A
inst✝ : HasPushout P.i₁ P'.i₀
⊢ P.i₁ ≫ P.π = P'.i₀ ≫ P'.π

Tactic:
by simp

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
⊢ P.i₁ ≫ P.π = P'.i₀ ≫ P'.π

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : C
P P' : PrepathObject A
inst✝ : HasPullback P.p₁ P'.p₀
⊢ P.ι ≫ P.p₁ = P'.ι ≫ P'.p₀

Tactic:
by simp

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
this : (trivialFibrations C).IsStableUnderRetracts
⊢ Arrow.Hom.left h.r ≫ f = hw.i ≫ hw.p ≫ Arrow.Hom.right h.r

Tactic:
by simp

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
this : (trivialFibrations C).IsStableUnderRetracts
sq : CommSq (Arrow.Hom.left h.r) hw.i f (hw.p ≫ Arrow.Hom.right h.r)
⊢ fibrations C f

Tactic:
rwa [← fibration_iff]

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
⊢ P.ι ≫ P.p₁ = P'.ι ≫ P'.p₀

Tactic:
by simp

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
⊢ hf.i ≫ hf.p ≫ Arrow.Hom.right h.i = Arrow.Hom.left h.i ≫ w

Tactic:
by simp

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 φ
⊢ hf.i ≫ 𝟙 hf.Z = Arrow.Hom.left h.i ≫ Arrow.Hom.left h.r ≫ hf.i

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : C
P : PrepathObject A
⊢ (P.p₀.op ≫ P.ι.op).unop = (𝟙 (op A)).unop

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : C
P : PrepathObject A
⊢ (P.p₁.op ≫ P.ι.op).unop = (𝟙 (op A)).unop

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ
P : PrepathObject A
⊢ (P.p₀.unop ≫ P.ι.unop).op = (𝟙 (unop A)).op

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ
P : PrepathObject A
⊢ (P.p₁.unop ≫ P.ι.unop).op = (𝟙 (unop A)).op

Tactic:
by simp

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

Tactic:
by
    rw [← rlp_eq_of_wfs (trivialCofibrations C) (fibrations C)]
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : C
P : Precylinder A
⊢ (P.π.op ≫ P.i₀.op).unop = (𝟙 (op A)).unop

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : C
P : Precylinder A
⊢ (P.π.op ≫ P.i₁.op).unop = (𝟙 (op A)).unop

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ
P : Precylinder A
⊢ (P.π.unop ≫ P.i₀.unop).op = (𝟙 (unop A)).op

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ
P : Precylinder A
⊢ (P.π.unop ≫ P.i₁.unop).op = (𝟙 (unop A)).op

Tactic:
by simp

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
f₀ f₁ f₂ : X ⟶ Y
h : P.LeftHomotopy f₀ f₁
P' : Precylinder X
h' : P'.LeftHomotopy f₁ f₂
inst✝ : HasPushout P.i₁ P'.i₀
⊢ P.i₁ ≫ h.h = P'.i₀ ≫ h'.h

Tactic:
by simp

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 simp

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:
obtain ⟨P, ⟨h⟩⟩ := h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : CategoryWithWeakEquivalences C
f g : X ⟶ Y
Z : C
p : Y ⟶ Z
P : Cylinder X
h : P.LeftHomotopy f g
⊢ LeftHomotopyRel (f ≫ p) (g ≫ p)
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:
obtain ⟨P, ⟨h⟩⟩ := h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
f g : X ⟶ Y
P : Cylinder X
h : P.LeftHomotopy f g
⊢ ∃ P, P.IsGood ∧ Nonempty (P.LeftHomotopy f g)
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:
obtain ⟨P, ⟨h⟩⟩ := h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : CategoryWithWeakEquivalences C
f g : X ⟶ Y
P : Cylinder X
h : P.LeftHomotopy f g
⊢ LeftHomotopyRel g f
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:
obtain ⟨P, ⟨h⟩⟩ := h

Goal state after:
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₂
P : Cylinder X
h : P.LeftHomotopy f₀ f₁
⊢ LeftHomotopyRel f₀ f₂
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 simp

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 simp

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 simp

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:
obtain ⟨P, ⟨h⟩⟩ := h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : CategoryWithWeakEquivalences C
f g : X ⟶ Y
Z : C
i : Z ⟶ X
P : PathObject Y
h : P.RightHomotopy f g
⊢ RightHomotopyRel (i ≫ f) (i ≫ g)
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:
obtain ⟨P, ⟨h⟩⟩ := h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
⊢ ∃ P, P.IsGood ∧ Nonempty (P.RightHomotopy f g)
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:
obtain ⟨P, ⟨h⟩⟩ := h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : CategoryWithWeakEquivalences C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
⊢ RightHomotopyRel g f
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:
obtain ⟨P, ⟨h⟩⟩ := h

Goal state after:
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₂
P : PathObject Y
h : P.RightHomotopy f₀ f₁
⊢ RightHomotopyRel f₀ f₂
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 simp

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 simp

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 simp

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 simp

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 simp

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 simp

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 simp

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 simp

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 simp

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

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
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h✝¹ : CochainComplex.IsStrictlyGE T.obj₁.as n₁
n₂ : ℤ
h✝ : CochainComplex.IsStrictlyGE T.obj₂.as n₂
f : T.obj₁.as ⟶ T.obj₂.as
hf : (quotient C (ComplexShape.up ℤ)).map f = T.mor₁
⊢ min (n₁ - 1) n₂ < n₁

Tactic:
by simp

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

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
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h✝¹ : CochainComplex.IsStrictlyGE T.obj₁.as n₁
n₂ : ℤ
h✝ : CochainComplex.IsStrictlyGE T.obj₂.as n₂
f : T.obj₁.as ⟶ T.obj₂.as
hf : (quotient C (ComplexShape.up ℤ)).map f = T.mor₁
⊢ min (n₁ - 1) n₂ ≤ n₂

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : Plus C
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L = K.obj
⊢ (quotient C).obj { obj := L, property := ?m.38 } = K

Tactic:
ext; exact hL

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

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
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex.Plus C
f₀ f₁ : K.obj ⟶ L.obj
hf : Homotopy f₀ f₁
n : ℤ
⊢ (ComplexShape.up ℤ).Rel (n - 1) n

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
X Y : C
f : X ⟶ Y
hX : B X
hY : A Y
Z : C
s : Y ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f s b ∈ Pretriangulated.distinguishedTriangles
hs : B.trW s
W : C
s' : Y ⟶ W
g : Z ⟶ W
hW : A W
hs' : (A ⊓ B).trW s'
fac : s ≫ g = s'
U : C
hU : A U
a : U ⟶ Y
c : W ⟶ (shiftFunctor C 1).obj U
hT' : Triangle.mk a s' c ∈ Pretriangulated.distinguishedTriangles
t : (Triangle.mk f s b).obj₁ ⟶ (Triangle.mk a s' c).obj₁
ht : (Triangle.mk f s b).mor₁ ≫ 𝟙 Y = t ≫ (Triangle.mk a s' c).mor₁
ht' : (Triangle.mk f s b).mor₃ ≫ (shiftFunctor C 1).map t = g ≫ (Triangle.mk a s' c).mor₃
⊢ A ⊓ B ≤ B

Tactic:
by simp

Goal state after: