mathlib-initiative/mathlib-tactics huggingface dataset:
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 : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ ((1 • (x.negOnePow • (K.d (p + x) (p + 1 + x)).f q) ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow • 1 • (K.d (p + x) (p + 1 + x)).f q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯

Tactic:
rw [one_smul, Category.assoc, ι_totalDesc, one_smul, Linear.units_smul_comp]

Goal state after:
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:
assumption

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

Goal state before:
pp: case inl
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
p : ℤ
hp✝ : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ (δ (-1) 0 (α + Cochain.single β (-1))).v p p hpq = (Cochain.ofHom f).v p p hpq

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
⊢ (δ (-1) 0 (α + Cochain.single β (-1))).v (n + 1) (n + 1) hpq = (Cochain.ofHom f).v (n + 1) (n + 1) hpq

Tactic:
· rw [δ_add, Cochain.add_v, hα p p (by lia) (by lia), add_eq_left,
      δ_v (-1) 0 (neg_add_cancel 1) _ p p hpq (p - 1) (p + 1) rfl rfl,
      Cochain.single_v_eq_zero _ _ _ _ _ (by lia),
      Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]
    simp

Goal state after:
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
⊢ (δ (-1) 0 (α + Cochain.single β (-1))).v (n + 1) (n + 1) hpq = (Cochain.ofHom f).v (n + 1) (n + 1) hpq
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 : ℤ
e : (singleFunctor C n).obj X ≅ (CochainComplex.singleFunctor C n ⋙ Q).obj X := (singleFunctorIsoCompQ C n).app X
⊢ ((singleFunctor C n).obj X).IsGE n

Tactic:
dsimp only [Functor.comp_obj] at e

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
e : (singleFunctor C n).obj X ≅ Q.obj ((CochainComplex.singleFunctor C n).obj X) := (singleFunctorIsoCompQ C n).app X
⊢ ((singleFunctor C n).obj X).IsGE n
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✝
a✝ : HasLiftingProperty i p
X Y : C
i✝ : ι
⊢ HasLiftingProperty i p

Tactic:
assumption

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 : ℤ
e : (singleFunctor C n).obj X ≅ (CochainComplex.singleFunctor C n ⋙ Q).obj X := (singleFunctorIsoCompQ C n).app X
⊢ ((singleFunctor C n).obj X).IsLE n

Tactic:
dsimp only [Functor.comp_obj] at e

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
e : (singleFunctor C n).obj X ≅ Q.obj ((CochainComplex.singleFunctor C n).obj X) := (singleFunctorIsoCompQ C n).app X
⊢ ((singleFunctor C n).obj X).IsLE n
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:
← weakEquivalence_iff_of_objectProperty

Goal state after:
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
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:
simp only [fibration_iff]
  symm
  apply (fibrations C).arrow_mk_iso_iff
  exact Arrow.isoMk (Iso.refl _) (IsTerminal.uniqueUpToIso hY terminalIsTerminal)

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
J✝ : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst✝² : HasCoproduct X
inst✝¹ : HasCoproduct Y
h : ∀ (i : J), Cofibration (f i)
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
⊢ Cofibration (Limits.Sigma.map f)

Tactic:
simp only [cofibration_iff] at h ⊢
  exact MorphismProperty.colimMap _ (fun ⟨i⟩ ↦ h i)

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

Goal state before:
pp: case left
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 ((mapPair f₁ f₂).app { as := WalkingPair.left })

Tactic:
assumption

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

Goal state before:
pp: case right
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 ((mapPair f₁ f₂).app { as := WalkingPair.right })

Tactic:
assumption

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

Goal state before:
pp: case left
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 ((mapPair f₁ f₂).app { as := WalkingPair.left })

Tactic:
assumption

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

Goal state before:
pp: case right
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 ((mapPair f₁ f₂).app { as := WalkingPair.right })

Tactic:
assumption

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

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

Tactic:
have := coprod.inr ≫= sq.fac_left
        simp only [Q.inr_i_assoc, coprod.inr_desc] at this
        simp [reassoc_of% this]

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

Goal state before:
pp: case refine_2
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 Y → B.trW s → ∃ Z s' a, A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'
X Y : Cᵒᵖ
s : X ⟶ Y
hX : A.op X
hs : B.op.trW s
⊢ ∃ Z s' b, A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s'

Tactic:
obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.unop hX (trW_of_op _ hs)
    exact ⟨_, s'.op, b.op, hZ', trW_of_unop _ hs', by cat_disch⟩

Goal state after:
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:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ t.IsLE X n₀ ↔ ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0

Tactic:
by
  refine ⟨fun _ Y f _ ↦ t.zero f n₀ n₁ (by lia), fun hX ↦ ?_⟩
  rw [t.isLE_iff_isZero_truncGE_obj n₀ n₁ h, IsZero.iff_id_eq_zero]
  exact t.from_truncGE_obj_ext (by simpa using hX _ _ inferInstance)

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case zero.succ.succ.succ.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ 0) (hjk : 0 ≤ k),
    map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk
hij : 0 ≤ 0 + 1
hjk : 0 + 1 ≤ k + 1 + 1
⊢ f 0 ≫ map (fun n ↦ f (n + 1)) 0 0 ⋯ ≫ map (fun n ↦ f (n + 1)) 0 (k + 1) ⋯ =
    map f 0 (0 + 1) hij ≫ map (fun n ↦ f (n + 1)) 0 (k + 1) ⋯

Tactic:
simp [map]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case zero.succ.succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j + 1) (hjk : j + 1 ≤ k),
    map f 0 k ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) k hjk
hij : 0 ≤ j + 1 + 1
hjk : j + 1 + 1 ≤ k + 1 + 1
⊢ f 0 ≫ map (fun n ↦ f (n + 1)) 0 (j + 1) ⋯ ≫ map (fun n ↦ f (n + 1)) (j + 1) (k + 1) ⋯ =
    map f 0 (j + 1 + 1) hij ≫ map (fun n ↦ f (n + 1)) (j + 1) (k + 1) ⋯

Tactic:
simp [map]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ℕ ⥤ C
app : (n : ℕ) → F.obj n ⟶ G.obj n
naturality : ∀ (n : ℕ), F.map (homOfLE ⋯) ≫ app (n + 1) = app n ≫ G.map (homOfLE ⋯)
k : ℕ
hk :
  ∀ ⦃i j : ℕ⦄ (hk : j = i + k),
    F.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j k hk)) ≫ app j =
      app i ≫ G.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j k hk))
⊢ ∀ ⦃i j : ℕ⦄ (hk : j = i + (k + 1)),
    F.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j (k + 1) hk)) ≫ app j =
      app i ≫ G.map (homOfLE (CategoryTheory.NatTrans.ofSequence._proof_1 i j (k + 1) hk))

Tactic:
intro i j hk'
        obtain rfl : j = i + k + 1 := by lia
        simp only [← homOfLE_comp (show i ≤ i + k by lia) (show i + k ≤ i + k + 1 by lia),
          Functor.map_comp, assoc, naturality, reassoc_of% (hk rfl)]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
⊢ (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ (t.truncGELTToLTGE a b).app X =
    (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))

Tactic:
rw [← cancel_epi (inv ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))),
    IsIso.inv_hom_id_assoc]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
⊢ (t.truncGELTToLTGE a b).app X =
    inv ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) ≫
      (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
⊢ (t.truncGELTToLTGE a b).app X =
    inv ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) ≫
      (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))

Tactic:
exact t.truncGELTToLTGE_app_pentagon_uniqueness _ (by simp)

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:
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:
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:
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:
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
left✝¹ : Mono i
left✝ : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
fac : i ≫ p = f
⊢ weakEquivalences (Plus C) (ObjectProperty.homMk i)

Tactic:
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✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h✝ : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject Z
left✝ : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
sq : CommSq h.h f P.p (prod.lift f₀ f₁)
⊢ sq.lift ≫ P.p₀ = f₀

Tactic:
by
          have := sq.fac_right =≫ prod.fst
          rwa [Category.assoc, P.p_fst, prod.lift_fst] at this

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

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n₀✝ n₁ : ℤ
hn₁ : n₀✝ + 1 = n₁
hf : ∀ i ≤ n₀✝, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
x✝ : x₁ ≫ K.d n₁ (n₁ + 1) = 0
y₀ : A ⟶ L.X n₀
hy₀ : x₁ ≫ (ι f n₁).f n₁ = (y₀ ≫ (σ K L n₁).f n₀) ≫ (mid K L n₁).d n₀ n₁
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁_1, π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁

Tactic:
simp only [Category.assoc, Hom.comm, biprodX_ext_to_iff, biprod_lift_fst_f,
    biprod_inr_fst_f, comp_zero, biprod_lift_snd_f, biprod_inr_snd_f,
    Category.comp_id] at hy₀

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n₀✝ n₁ : ℤ
hn₁ : n₀✝ + 1 = n₁
hf : ∀ i ≤ n₀✝, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
x✝ : x₁ ≫ K.d n₁ (n₁ + 1) = 0
y₀ : A ⟶ L.X n₀
hy₀ : x₁ ≫ (i K n₁).f n₁ = 0 ∧ x₁ ≫ f.f n₁ = y₀ ≫ L.d n₀ n₁
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁_1, π ≫ x₁ = x₁_1 ≫ K.d n₀ n₁
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono (homologyMap f n)
⊢ Mono (homologyShortComplex f n).f

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
⊢ (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯)).left.hom ≫
      T.map (StructuredArrow.Hom.right φ).left =
    (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯)).left.hom

Tactic:
dsimp; rw [← StructuredArrow.w φ]; rfl

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE (n + 1)
⊢ Mono { mid := L, ι := f, π := 𝟙 L, ι_π := ⋯ }.ι

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
hw : w.GuitartExact
X₂ : C₂
⊢ (w.structuredArrowDownwards X₂).Initial

Tactic:
rw [guitartExact_iff_initial] at hw

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
hw : ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
X₂ : C₂
⊢ (w.structuredArrowDownwards X₂).Initial
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.obj.IsStrictlyGE n
L : CochainComplex C ℤ
i : K.obj ⟶ L
w✝¹ : QuasiIso i
w✝ : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE n
L' : CochainComplex (InjectiveObject C) ℤ := HomologicalComplex.liftObjectProperty (isInjective C) L ⋯
hL' : L'.IsStrictlyGE n
⊢ quasiIso C (ObjectProperty.homMk i)

Tactic:
assumption

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.IsGE n
⊢ K.IsGE n

Tactic:
assumption

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.IsGE n
this : K.obj.IsGE n
L : CochainComplex C ℤ
w✝¹ : L.IsStrictlyGE n
e : K.obj ≅ DerivedCategory.Q.obj L
M : CochainComplex.Plus (InjectiveObject C)
w✝ : M.obj.IsStrictlyGE n
i : { obj := L, property := ⋯ } ⟶ (InjectiveObject.ι C).mapCochainComplexPlus.obj M
hi : CochainComplex.Plus.quasiIso C i
⊢ QuasiIso i.hom

Tactic:
assumption

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

Goal state before:
pp: case refine_3
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
L✝ : Plus C ⥤ H
inst✝ : L✝.IsLocalization (quasiIso C)
K L : Plus C
f : K ⟶ L
hf : quasiIso C f
⊢ (CochainComplex.Plus.quasiIso C).map (quotient C) f

Tactic:
obtain ⟨K, rfl⟩ := Plus.quotient_obj_surjective K

Goal state after:
case refine_3
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
L✝ : Plus C ⥤ H
inst✝ : L✝.IsLocalization (quasiIso C)
L : Plus C
K : CochainComplex.Plus C
f : (quotient C).obj K ⟶ L
hf : quasiIso C f
⊢ (CochainComplex.Plus.quasiIso C).map (quotient C) f
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Category.{v_2, u_2} H
inst✝¹ : EnoughInjectives C
inst✝ : HasDerivedCategory C
K : DerivedCategory.Plus C
r : (localizerMorphism C).RightResolution (DerivedCategory.Plus.Qh.objPreimage K) :=
  Classical.arbitrary ((localizerMorphism C).RightResolution (DerivedCategory.Plus.Qh.objPreimage K))
this : IsIso (DerivedCategory.Plus.Qh.map r.w)
⊢ ((InjectiveObject.ι C).mapHomotopyCategoryPlus ⋙ DerivedCategory.Plus.Qh).essImage K

Tactic:
exact ⟨r.X₁, ⟨(asIso (DerivedCategory.Plus.Qh.map r.w)).symm ≪≫
      DerivedCategory.Plus.Qh.objObjPreimageIso K⟩⟩

Goal state after: