mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
x₂ : X _⦋n₁⦌
hx₂ : x₂ ∈ X.nonDegenerate n₁
h' : mk ↑⟨x₂, hx₂⟩ ⋯ ≤ mk ↑⟨x₁, hx₁⟩ ⋯
f : ⦋(mk ↑⟨x₁, hx₁⟩ ⋯).dim⦌ ⟶ ⦋(mk ↑⟨x₂, hx₂⟩ ⋯).dim⦌
hf : Mono f
h : (ConcreteCategory.hom (X.map f.op)) (mk ↑⟨x₂, hx₂⟩ ⋯).simplex = (mk ↑⟨x₁, hx₁⟩ ⋯).simplex
⊢ mk ↑⟨x₁, hx₁⟩ ⋯ = mk ↑⟨x₂, hx₂⟩ ⋯

Tactic:
obtain rfl := SimplexCategory.eq_id_of_mono f

Goal state after:
X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
x₂ : X _⦋n₁⦌
hx₂ : x₂ ∈ X.nonDegenerate n₁
h' : mk ↑⟨x₂, hx₂⟩ ⋯ ≤ mk ↑⟨x₁, hx₁⟩ ⋯
hf : Mono (𝟙 ⦋(mk ↑⟨x₁, hx₁⟩ ⋯).dim⦌)
h : (ConcreteCategory.hom (X.map (𝟙 ⦋(mk ↑⟨x₁, hx₁⟩ ⋯).dim⦌).op)) (mk ↑⟨x₂, hx₂⟩ ⋯).simplex = (mk ↑⟨x₁, hx₁⟩ ⋯).simplex
⊢ mk ↑⟨x₁, hx₁⟩ ⋯ = mk ↑⟨x₂, hx₂⟩ ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
this : (ConcreteCategory.hom (X.map (g hf₁ f₂).op)) y₂ = ↑y₁
⊢ IsIso (factorThruImage (g hf₁ f₂))

Tactic:
← image.fac (g hf₁ f₂),

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
this : (ConcreteCategory.hom (X.map (factorThruImage (g hf₁ f₂) ≫ image.ι (g hf₁ f₂)).op)) y₂ = ↑y₁
⊢ IsIso (factorThruImage (g hf₁ f₂))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.op.N
⊢ mk (opObjEquiv x.simplex) ⋯ ≤ mk (opObjEquiv y.simplex) ⋯ ↔ x ≤ y

Tactic:
simp only [le_iff, Subcomplex.ofSimplex_le_iff, Subcomplex.mem_ofSimplex_obj_iff]

Goal state after:
X : SSet
x y : X.op.N
⊢ (∃ f,
      (ConcreteCategory.hom (X.map f.op)) (mk (opObjEquiv y.simplex) ⋯).simplex =
        (mk (opObjEquiv x.simplex) ⋯).simplex) ↔
    ∃ f, (ConcreteCategory.hom (X.op.map f.op)) y.simplex = x.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.N
⊢ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯ ≤
      mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯ ↔
    x ≤ y

Tactic:
simp only [le_iff, Subcomplex.ofSimplex_le_iff, Subcomplex.mem_ofSimplex_obj_iff]

Goal state after:
X Y : SSet
e : X ≅ Y
x y : X.N
⊢ (∃ f,
      (ConcreteCategory.hom (Y.map f.op))
          (mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯).simplex =
        (mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯).simplex) ↔
    ∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k✝ : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k✝
k : ℕ
⊢ f ≫ C.d 0 (k + 1) = 0

Tactic:
cases k

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
⊢ f ≫ C.d 0 (0 + 1) = 0

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n✝ : ℕ
⊢ f ≫ C.d 0 (n✝ + 1 + 1) = 0
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
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_3} C₃
inst✝³ : Category.{v_4, u_4} C₄
inst✝² : Category.{v_5, u_5} C₁₂
inst✝¹ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
inst✝ :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
j : J
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : p (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      { app := fun X₃ ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃), naturality := ⋯ }.app X₃ j =
    ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      (𝟙
            { obj := fun X₃ ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
              map := fun {x x_1} φ ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ, map_id := ⋯, map_comp := ⋯ }).app
        X₃ j

Tactic:
simp only [ι_mapTrifunctorMapMap, categoryOfGradedObjects_id, Functor.map_id,
      NatTrans.id_app, id_comp, comp_id]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : (up ℤ).Rel n₀ n₁
⊢ ((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁'

pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁'

Tactic:
· apply total.hom_ext
    intro p q hpq
    dsimp at h hpq
    dsimp [totalShift₁XIso]
    rw [ι_D₂_assoc, Linear.comp_units_smul, ι_totalDesc_assoc, ι_D₂,
      ((shiftFunctor₁ C x).obj K).d₂_eq _ _ rfl _ (by dsimp; lia),
      K.d₂_eq _ _ rfl _ (by dsimp; lia), smul_smul,
      Linear.units_smul_comp, Category.assoc, ι_totalDesc]
    dsimp
    congr 1
    rw [add_comm p, Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : ¬(up ℤ).Rel n₀ n₁
⊢ ((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁'
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasLimitsOfShape WalkingCospan C
X Y : Plus C
f : X ⟶ Y
x✝ : Mono f.hom
⊢ Mono ((ι C).map f)

Tactic:
by assumption

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
⊢ ∀ (a b : Cocycle K L n),
    a ≈ b →
      SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm a) =
        SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm b)

Tactic:
let := HasDerivedCategory.standard C

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ∀ (a b : Cocycle K L n),
    a ≈ b →
      SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm a) =
        SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm b)
Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ : Cocycle K L n
⊢ ∀ (b : Cocycle K L n),
    y₁ ≈ b →
      SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm y₁) =
        SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm b)

Tactic:
y₂

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
⊢ y₁ ≈ y₂ →
    SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm y₁) =
      SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm y₂)
Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : L.IsKInjective
⊢ Function.Bijective toSmallShiftedHom

Tactic:
let := HasDerivedCategory.standard C

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : L.IsKInjective
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Function.Bijective toSmallShiftedHom
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst✝ : Injective (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
hp : n + 1 ≤ n + 1
hpq : n + 1 + 0 = n + 1
⊢ (α.v (n + 1) n ⋯ + 0) ≫ L.d n (n + 1) +
      Int.negOnePow 0 • K.d (n + 1) (n + 2) ≫ (α + Cochain.single β (-1)).v (n + 2) (n + 1) ⋯ =
    (Cochain.ofHom f).v (n + 1) (n + 1) hpq

Tactic:
simp [hβ, u]

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 f

Tactic:
← hf.fac

Goal state after:
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)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated

Goal state before:
pp: case refine_2
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
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
⊢ w₁₃ ≫ (shiftFunctor Cᵒᵖ 1).map u₁₂ = o.m₁.op ≫ w₂₃

Tactic:
have eq₂ := congr($(o.comm₂).op)

Goal state after:
case refine_2
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
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  ((((opShiftFunctorEquivalence C 1).unitIso.inv.app (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁).unop ≫
          (shiftFunctor C 1).map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃.unop) ≫
        (shiftFunctor C 1).map o.m₁).op =
    ((Triangle.mk u₁₂ v₁₂ w₁₂).mor₁.unop ≫
        ((opShiftFunctorEquivalence C 1).unitIso.inv.app (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁).unop ≫
          (shiftFunctor C 1).map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃.unop).op
⊢ w₁₃ ≫ (shiftFunctor Cᵒᵖ 1).map u₁₂ = o.m₁.op ≫ w₂₃
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ IsIso { X₁ := 0, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }.g

Tactic:
by assumption

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

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : Category.{v_3, u_3} D₁
inst✝¹⁰ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : IsTriangulated C
inst✝³ : A.IsTriangulated
inst✝² : B.IsTriangulated
inst✝¹ : B.IsClosedUnderIsomorphisms
inst✝ : A.IsVerdierLeftLocalizing B
⊢ (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful

Tactic:
let L₁ := (B.inverseImage A.ι).trW.Q

Goal state after:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : Category.{v_3, u_3} D₁
inst✝¹⁰ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : IsTriangulated C
inst✝³ : A.IsTriangulated
inst✝² : B.IsTriangulated
inst✝¹ : B.IsClosedUnderIsomorphisms
inst✝ : A.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
⊢ (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
n m : ℤ
hnm : n + 1 = m
this : Epi π
l : Q.X n ⟶ X.X m
hl : π.f n ≫ l = (↑(cocycle₁' sq hsq)).v n m hnm
l' : Q.X n ⟶ ((KernelFork.ofι ι hι).map (HomologicalComplex.eval C (ComplexShape.up ℤ) m)).pt
hl' : l' ≫ Fork.ι ((KernelFork.ofι ι hι).map (HomologicalComplex.eval C (ComplexShape.up ℤ) m)) = l
⊢ ∃ φ, π.f n ≫ φ ≫ ι.f m = (↑(cocycle₁' sq hsq)).v n m hnm

Tactic:
exact ⟨l', by cat_disch⟩

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
hp : degreewiseEpiWithInjectiveKernel p
t : A ⟶ X
b : B ⟶ Y
hip✝ : QuasiIso i ∨ QuasiIso p
sq✝ : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝¹ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq✝ (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i)
    (kernelIsKernel p)
this✝ : ∀ (n : ℤ), Injective ((kernel p).X n)
d : ℤ
hd : X.IsStrictlyGE d
inst✝ : Fibration (ObjectProperty.homMk p)
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
sq : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
this : (kernel p).IsStrictlyGE d
⊢ (kernel p).IsKInjective

Tactic:
exact isKInjective_of_injective _ d

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CategoryWithCofibrations C
inst✝¹ : HasInitial C
X : C
inst✝ : IsCofibrant X
⊢ cofibrantObjects C X

Tactic:
by assumption

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CategoryWithFibrations C
inst✝¹ : HasTerminal C
X : C
inst✝ : IsFibrant X
⊢ fibrantObjects C X

Tactic:
by assumption

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : HasInitial C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant X
⊢ cofibrantObjects C X

Tactic:
by assumption

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : HasInitial C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant X
⊢ fibrantObjects C X

Tactic:
by assumption

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi✝ : i ≤ n₀
hi : i < n₀
φ : (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).obj (mid K L n₁) ⟶
  (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).obj L :=
  (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).map (π K L n₁)
⊢ ShortComplex.QuasiIso ((shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).map (π K L n₁))

Tactic:
have : IsIso φ.τ₁ := isIso_π_f ..

Goal state after:
case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi✝ : i ≤ n₀
hi : i < n₀
φ : (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).obj (mid K L n₁) ⟶
  (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).obj L :=
  (shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).map (π K L n₁)
this : IsIso φ.τ₁
⊢ ShortComplex.QuasiIso ((shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).map (π K L n₁))
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
d : ℤ
left✝² : K.IsStrictlyGE (d + 1)
right✝ : L.IsStrictlyGE d
K' : CochainComplex C ℤ
w✝ : K'.IsStrictlyGE d
i : { obj := K, property := ⋯ }.obj ⟶ K'
p : K' ⟶ { obj := L, property := ⋯ }.obj
left✝¹ : Mono i
left✝ : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
fac : i ≫ p = f
⊢ weakEquivalences (Plus C) (ObjectProperty.homMk i)

Tactic:
by assumption

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
d : ℤ
left✝ : K.IsStrictlyGE (d + 1)
right✝ : L.IsStrictlyGE d
K' : CochainComplex C ℤ
w✝² : K'.IsStrictlyGE d
i : { obj := K, property := ⋯ }.obj ⟶ K'
p : K' ⟶ { obj := L, property := ⋯ }.obj
w✝¹ : Mono i
hp : degreewiseEpiWithInjectiveKernel p
w✝ : QuasiIso p
fac : i ≫ p = f
⊢ weakEquivalences (Plus C) (ObjectProperty.homMk p)

Tactic:
by assumption

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : X ⟶ Y
h : RightHomotopyRel x✝¹ x✝
⊢ LeftHomotopyRel x✝¹ x✝

Tactic:
exact h.leftHomotopyRel

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D₁
inst✝² : Category.{v_4, u_4} D₂
inst✝¹ : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.HasRightResolutions
⊢ Φ.op.HasLeftResolutions

Tactic:
by
  rwa [← hasRightResolutions_iff_op]

Goal state after: