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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
hφ : ∀ (k : ℕ) (x : ↑(X k)), (↑(φ k x)).EqUpTo (↑x) (d + ↑k)
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
⊢ (↑(Cochain.InductionUp.sequence φ x₀ k₀)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 • K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence φ x₀ k₀)).v (n + 1) n ⋯ =
    (↑(Cochain.InductionUp.sequence φ x₀ k₀)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 • K.d n (n + 1) ≫ (limitSequence φ hφ x₀).v (n + 1) n ⋯

Tactic:
limitSequence_eqUpTo φ hφ x₀ k₀ (n + 1) n (by lia) (by lia)

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
hφ : ∀ (k : ℕ) (x : ↑(X k)), (↑(φ k x)).EqUpTo (↑x) (d + ↑k)
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
⊢ (↑(Cochain.InductionUp.sequence φ x₀ k₀)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 • K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence φ x₀ k₀)).v (n + 1) n ⋯ =
    (↑(Cochain.InductionUp.sequence φ x₀ k₀)).v n (n - 1) ⋯ ≫ L.d (n - 1) n +
      Int.negOnePow 0 • K.d n (n + 1) ≫ (↑(Cochain.InductionUp.sequence φ x₀ k₀)).v (n + 1) 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
K : CochainComplex C ℤ
n : ℤ
inst✝ : K.IsGE n
⊢ (Q.obj K).IsGE n

Tactic:
rw [isGE_Q_obj_iff]

Goal state after:
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
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

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

Tactic:
exact MorphismProperty.of_isPushout
    ((IsPushout.of_isColimit_binaryCofan_of_isInitial
    (colimit.isColimit (pair X Y)) initialIsInitial).flip) hY

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLE n).obj X
h : f₁ ≫ (t.truncLEι n).app X = f₂ ≫ (t.truncLEι n).app X
inst✝ : t.IsLE Y n
this : t.IsLE Y (n + 1 - 1)
⊢ (f₁ ≫ (t.truncLEIsoTruncLT n (n + 1) ⋯).hom.app X) ≫ (t.truncLTι (n + 1)).app X =
    (f₂ ≫ (t.truncLEIsoTruncLT n (n + 1) ⋯).hom.app X) ≫ (t.truncLTι (n + 1)).app X

Tactic:
by simpa

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 : ℤ
h : b ≤ a
X : C
⊢ b ≤ a - 1 + 1

Tactic:
by simpa

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
⊢ IsIso ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))

Tactic:
by
  rw [← t.isLE_iff_isIso_truncLTι_app (b - 1) b (by lia)]
  infer_instance

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
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
⊢ ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ t.liftTruncLT m₁ (b - 1) b ⋯) ≫
      (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncLT b).map m₁ ≫ (t.truncLTι b).app ((t.truncGE a).obj X)

Tactic:
by simp [truncGELT]

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 : ℤ
inst✝ : Mono f
T : ShortComplex C :=
  { X₁ := homology K n, X₂ := homology L n, X₃ := homology (cokernel f) n, f := homologyMap f n,
    g := homologyMap (cokernel.π f) n, zero := ⋯ }
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ Mono (homologyMap ((cokernel f).πTruncGE n ≫ p f n) n) ∧ IsIso (𝟙 T.X₂) ∧ Epi (𝟙 T.X₁)

Tactic:
rw [homologyMap_comp]

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 : ℤ
inst✝ : Mono f
T : ShortComplex C :=
  { X₁ := homology K n, X₂ := homology L n, X₃ := homology (cokernel f) n, f := homologyMap f n,
    g := homologyMap (cokernel.π f) n, zero := ⋯ }
φ : T ⟶ homologyShortComplex f n :=
  { τ₁ := 𝟙 T.X₁, τ₂ := 𝟙 T.X₂, τ₃ := homologyMap ((cokernel f).πTruncGE n ≫ p f n) n, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ Mono (homologyMap ((cokernel f).πTruncGE n) n ≫ homologyMap (p f n) n) ∧ IsIso (𝟙 T.X₂) ∧ Epi (𝟙 T.X₁)
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
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₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁴ : L.functor.EssSurj
inst✝³ : R.functor.Full
inst✝² : R.IsInduced
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : B.HasLeftResolutions
⊢ T.HasLeftResolutions

Tactic:
intro X₂
  let ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary _
  obtain ⟨X₁, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage L.functor ρ.X₁
  exact ⟨{
    X₁ := X₁
    w := R.functor.preimage (iso.hom.app X₁ ≫ B.functor.map e.hom ≫ ρ.w)
    hw := by
      simp only [← R.inverseImage_eq, MorphismProperty.inverseImage_iff, Functor.map_preimage]
      refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw
      exact Arrow.isoMk (iso.app _ ≪≫ B.functor.mapIso e) (Iso.refl _) }⟩

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

Goal state before:
pp: case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact → w.GuitartExact

Tactic:
intro h
    have : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom := by
      ext X₁
      simp only [Functor.comp_obj, whiskerVertical_app, assoc, Iso.hom_inv_id_app_assoc,
        ← B.map_comp, Iso.hom_inv_id_app, B.map_id, comp_id]
    rw [this]
    exact whiskerVertical (w.whiskerVertical α.hom β.inv) α.symm β.symm

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

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 : B.op.obj X₃ ⟶ R.op.obj X₂
f : (w.op.StructuredArrowRightwards g)ᵒᵖ
⊢ (R.map (StructuredArrow.right (Opposite.unop f)).hom.unop ≫
        w.app (Opposite.unop (StructuredArrow.right (Opposite.unop f)).left) ≫
          B.map (StructuredArrow.hom (Opposite.unop f)).left.unop).op =
    g.unop.op

Tactic:
simpa using! CostructuredArrow.w f.unop.hom

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 : w.CostructuredArrowDownwards g
⊢ ∃ X₁ a b, ∃ (comm : R.map a ≫ w.app X₁ ≫ B.map b = g), f = mk w g X₁ a b comm

Tactic:
obtain ⟨g, φ, rfl⟩ := CostructuredArrow.mk_surjective f
  obtain ⟨X₁, a, rfl⟩ := g.mk_surjective
  obtain ⟨b, hb, rfl⟩ := StructuredArrow.homMk_surjective φ
  exact ⟨X₁, a, b, by simpa using hb, rfl⟩

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
F : C₂ ⥤ D
E : R.LeftExtension F
w : TwoSquare T L R B
inst✝¹ : w.GuitartExact
inst✝ : B.EssSurj
x✝ : (E.compTwoSquare w).IsPointwiseLeftKanExtension
⊢ (fun h ↦ h.compTwoSquare w) ((fun h ↦ E.isPointwiseLeftKanExtensionOfCompTwoSquare w h) x✝) = x✝

Tactic:
subsingleton

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
F : C₂ ⥤ D
E : R.LeftExtension F
w : TwoSquare T L R B
inst✝¹ : w.GuitartExact
inst✝ : B.EssSurj
x✝ : E.IsPointwiseLeftKanExtension
⊢ (fun h ↦ E.isPointwiseLeftKanExtensionOfCompTwoSquare w h) ((fun h ↦ h.compTwoSquare w) x✝) = x✝

Tactic:
subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
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₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₂'.RespectsIso
inst✝⁴ : L.IsLocalizedEquivalence
inst✝³ : R.IsLocalizedEquivalence
inst✝² : R.functor.EssSurj
inst✝¹ : T.IsRightDerivabilityStructure
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.hom
⊢ B.IsRightDerivabilityStructure

Tactic:
rw [isRightDerivabilityStructure_iff_op]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
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₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₂'.RespectsIso
inst✝⁴ : L.IsLocalizedEquivalence
inst✝³ : R.IsLocalizedEquivalence
inst✝² : R.functor.EssSurj
inst✝¹ : T.IsRightDerivabilityStructure
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.hom
⊢ B.op.IsLeftDerivabilityStructure
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughProjectives C
inst✝ : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn : ∀ (X : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
X : C
P : ProjectivePresentation X := Classical.arbitrary (ProjectivePresentation X)
S : ShortComplex C := { X₁ := Limits.kernel P.f, X₂ := P.p, X₃ := X, f := kernel.ι P.f, g := P.f, zero := ⋯ }
this : Projective (S.map F).X₂
hS : S.ShortExact
x₃ : Ext S.X₃ Y (n + 1)
⊢ (Ext.mk₀ S.g).comp x₃ ⋯ = 0

Tactic:
subsingleton

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughProjectives C
inst✝ : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn : ∀ (X : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
X : C
P : ProjectivePresentation X := Classical.arbitrary (ProjectivePresentation X)
S : ShortComplex C := { X₁ := Limits.kernel P.f, X₂ := P.p, X₃ := X, f := kernel.ι P.f, g := P.f, zero := ⋯ }
this : Projective (S.map F).X₂
hS : S.ShortExact
y₃ : Ext (F.obj S.X₃) (F.obj Y) (n + 1)
⊢ (Ext.mk₀ (S.map F).g).comp y₃ ⋯ = 0

Tactic:
subsingleton

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughInjectives C
inst✝ : F.PreservesInjectiveObjects
X : C
n : ℕ
hn : ∀ (Y : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
Y : C
I : InjectivePresentation Y := Classical.arbitrary (InjectivePresentation Y)
S : ShortComplex C := { X₁ := Y, X₂ := I.J, X₃ := cokernel I.f, f := I.f, g := cokernel.π I.f, zero := ⋯ }
this : Injective (S.map F).X₂
hS : S.ShortExact
x₁ : Ext X S.X₁ (n + 1)
⊢ x₁.comp (Ext.mk₀ S.f) ⋯ = 0

Tactic:
subsingleton

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughInjectives C
inst✝ : F.PreservesInjectiveObjects
X : C
n : ℕ
hn : ∀ (Y : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
Y : C
I : InjectivePresentation Y := Classical.arbitrary (InjectivePresentation Y)
S : ShortComplex C := { X₁ := Y, X₂ := I.J, X₃ := cokernel I.f, f := I.f, g := cokernel.π I.f, zero := ⋯ }
this : Injective (S.map F).X₂
hS : S.ShortExact
y₁ : Ext (F.obj X) (F.obj S.X₁) (n + 1)
⊢ y₁.comp (Ext.mk₀ (S.map F).f) ⋯ = 0

Tactic:
subsingleton

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

Goal state before:
pp: β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j : β
w : ¬(ComplexShape.up' b).Rel i j
⊢ (if h : i + b = j then X.d i ≫ X.objEqToHom ⋯ else 0) = 0

Tactic:
dsimp at w

Goal state after:
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j : β
w : ¬i + b = j
⊢ (if h : i + b = j then X.d i ≫ X.objEqToHom ⋯ else 0) = 0
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ (match Int.negSucc 0 with
      | Int.ofNat n => fL.f n
      | Int.negSucc n => fK.f n) ≫
      h'.cochainComplex.d (Int.negSucc 0) (Int.negSucc 0 + 1) =
    h.cochainComplex.d (Int.negSucc 0) (Int.negSucc 0 + 1) ≫
      match Int.negSucc 0 + 1 with
      | Int.ofNat n => fL.f n
      | Int.negSucc n => fK.f n

Tactic:
by simpa

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
L : CochainComplex C ℤ
g : L ⟶ K
⊢ ↑(toSingleMk (g.f p ≫ f) h p' hp' ⋯) = ↑((toSingleMk f h p' hp' hf).precomp g)

Tactic:
exact (Cochain.toSingleEquiv h).injective (by simp [Cochain.toSingleMk_precomp])

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K ((singleFunctor C q).obj X) (n - 1)
g : K.X p'' ⟶ X
hα : n.negOnePow • Cochain.toSingleMk (K.d p p'' ≫ g) h = Cochain.toSingleMk f h
hg : Cochain.toSingleMk g ⋯ = α
⊢ (Cochain.toSingleEquiv h).symm (K.d p p'' ≫ (n.negOnePow • g)) = (Cochain.toSingleEquiv h).symm f

Tactic:
by simpa

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X : C
⊢ F.map (𝟙 ((toKaroubi C).obj X)) ≫ τ.app X ≫ G.map ((toKaroubi C).obj X).decompId_p = τ.app X

Tactic:
Karoubi.decompId_p_toKaroubi,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X : C
⊢ F.map (𝟙 ((toKaroubi C).obj X)) ≫
      τ.app X ≫ G.map (𝟙 { X := ((toKaroubi C).obj X).X, p := 𝟙 ((toKaroubi C).obj X).X, idem := ⋯ }) =
    τ.app X
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯) ≫ (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) =
    X.toCycles f₃ f₄ f₃₄ h₃₄ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫
        X.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.fromOpcycles f₄ f₅ f₄₅ h₄₅ n₁ ≫ X.δ f₂₃ f₄₅ n₁ n₂ hn₂

Tactic:
fromOpcyles_δ ..,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫ (X.H n₂).map (twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯) ≫ (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) =
    X.toCycles f₃ f₄ f₃₄ h₃₄ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.δFromOpcycles f₂₃ f₄ f₅ n₁ n₂ ⋯
Module: Mathlib.Order.WithBotTop

Goal state before:
pp: ι : Type u_1
inst✝ : Preorder ι
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
⊢ coe x✝² ≤ coe x✝¹

Tactic:
by simpa

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ (parallelPair (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).map
        WalkingParallelPairHom.left ≫
      (Iso.refl
          ((parallelPair (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).obj
            WalkingParallelPair.one)).hom =
    (Iso.refl
          ((parallelPair (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).obj
            WalkingParallelPair.zero)).hom ≫
      (parallelPair (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯) 0).map WalkingParallelPairHom.left

Tactic:
by simpa

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
⊢ (parallelPair (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0).map
        WalkingParallelPairHom.left ≫
      (Iso.refl
          ((parallelPair (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0).obj
            WalkingParallelPair.one)).hom =
    (Iso.refl
          ((parallelPair (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0).obj
            WalkingParallelPair.zero)).hom ≫
      (parallelPair (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯) 0).map WalkingParallelPairHom.left

Tactic:
by simpa

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) ≫
      biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯) =
    0

Tactic:
by ext <;> simp

Goal state after: