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

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ sq.kernelFork.pt
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ m ≫ (PullbackCone.mk fst snd ⋯).snd =
    PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ (PullbackCone.mk fst snd ⋯).snd

Tactic:
replace hm := hm =≫ biprod.snd
          dsimp at hm ⊢
          simp only [assoc, biprod.lift_snd] at hm
          rw [hm]
          symm
          apply PullbackCone.IsLimit.lift_snd h

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

Goal state before:
pp: case neg
ι : 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
h : Homotopy (extendMap f e) (extendMap g e)
i : ι
this :
  (K.extendXIso e ⋯).hom ≫ f.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) h.hom + (prevD (e.f i)) h.hom + (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
hi : ¬c.Rel i (c.next i)
⊢ (dNext (e.f i)) h.hom =
    (K.extendXIso e ⋯).hom ≫
      ((dNext i) fun i j ↦ (K.extendXIso e ⋯).inv ≫ h.hom (e.f i) (e.f j) ≫ (L.extendXIso e ⋯).hom) ≫
        (L.extendXIso e ⋯).inv

Tactic:
· rw [dNext_eq_zero _ _ hi]
        by_cases hi' : c'.Rel (e.f i) (c'.next (e.f i))
        · simp [dNext_eq _ hi', extend_d_from_eq_zero _ _ _ _ _ rfl hi]
        · simp [dNext_eq_zero _ _ hi']

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
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_5} C₃
inst✝²⁰ : Category.{v_4, u_6} C₄
inst✝¹⁹ : Category.{v_6, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
⊢ ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
    d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Tactic:
by
  simp [D₃]

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
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
⊢ (h.extend e).ofExtend.hom i j = h.hom i j

Tactic:
simp [ofExtend_hom, h.extend_hom_eq e rfl rfl]

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

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 : ℤ
X : C
i : ℤ
h✝ : t.IsLE X i
⊢ n + (i - n) = i

Tactic:
omega

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

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 : ℤ
X : C
i : ℤ
h✝ : t.IsGE X i
⊢ n + (i - n) = i

Tactic:
omega

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ s ≫ u = f ≫ ⋯.lift

Tactic:
rw [CommSq.fac_left]

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

Goal state before:
pp: case refine_2
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
⊢ Q.map (K.πTruncGE 1) = e₂.hom ≫ e₂.inv ≫ Q.map (K.πTruncGE 1)

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
case refine_2
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
⊢ Q.map (K.πTruncGE 1) = Q.map (K.πTruncGE 1)
Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder

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

Tactic:
rw [← P.inl_i]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝⁶ : HasBinaryCoproduct A A
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : HasInitial C
inst✝³ : (cofibrations C).IsStableUnderComposition
inst✝² : (cofibrations C).IsStableUnderCobaseChange
inst✝¹ : IsCofibrant A
inst✝ : P.IsGood
⊢ Cofibration (coprod.inl ≫ P.i)
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 ⋯
⊢ Fibration hf.p

Tactic:
simpa only [fibration_iff] using hf.hp

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

Goal state before:
pp: case h_obj
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Quotient r ⥤ E
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ ∀ (X : Quotient r), F₁.obj X = F₂.obj X

Tactic:
rintro ⟨X⟩
      exact Functor.congr_obj h X

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.ι
⊢ L.op.IsLocalization W.op

Tactic:
refine isLocalization_of_essSurj_of_full_of_exists_cylinders L.op W.op hW.op
    (fun X Y f₀ f₁ hf ↦ ?_)

Goal state after:
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
hf : L.op.map f₀ = L.op.map f₁
⊢ ∃ P x, W.op P.π
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
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
⊢ triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc = triangleFunctorNatTransOfLE t a c ⋯

Tactic:
apply NatTrans.ext
  ext1 X
  exact triangle_map_ext t (triangleFunctor_obj_distinguished _ _ _)
    (triangleFunctor_obj_distinguished _ _ _) (a - 1) c inferInstance inferInstance (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
⊢ (∃ I,
      ∃ (_ : Injective I),
        ∃ f, ∃ (w : f ≫ g = 0), Nonempty { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting) →
    epiWithInjectiveKernel g

Tactic:
rintro ⟨I, _, f, w, ⟨σ⟩⟩

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
I : C
w✝ : Injective I
f : I ⟶ X
w : f ≫ g = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting
⊢ epiWithInjectiveKernel g
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
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this : CatCommSq (A.op.triangulatedLocalizerMorphism B.op).functor (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op (CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F).symm) }
⊢ L₂.op.IsLocalization B.op.trW

Tactic:
trW_op

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
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this : CatCommSq (A.op.triangulatedLocalizerMorphism B.op).functor (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op (CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F).symm) }
⊢ L₂.op.IsLocalization B.trW.op
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case zero.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
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

Tactic:
obtain (_ | _ | k) := k
          · lia
          · obtain rfl : j = 0 := by lia
            rw [map_id, comp_id]
          · simp only [map, Nat.reduceAdd]
            rw [hj (fun n ↦ f (n + 1)) (k + 1) (by lia) (by lia)]
            obtain _ | j := j
            all_goals simp [map]

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]
  exact t.truncGELTToLTGE_app_pentagon_uniqueness _ (by simp)

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

Goal state before:
pp: case pos
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₁)
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

Tactic:
have eq' : t.liftTruncLT m₁ (b - 1) b (by lia) = (t.truncGELTToLTGE a b).app X :=
      t.to_truncLT_obj_ext
        (by dsimp; exact t.from_truncGE_obj_ext (by simpa using H.comm₁))

Goal state after:
case pos
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
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
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.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
⊢ L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom f₂) =
    StructuredArrow.Hom.right (CostructuredArrow.hom f₁)

Tactic:
rw [← CostructuredArrow.w φ]

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
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
⊢ L.map (StructuredArrow.Hom.right φ.left) ≫ StructuredArrow.Hom.right (CostructuredArrow.hom f₂) =
    StructuredArrow.Hom.right ((w.structuredArrowDownwards X₂).map φ.left ≫ CostructuredArrow.hom f₂)
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 : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : K.IsStrictlyGE n
this✝² : HasDerivedCategory C
L : CochainComplex C ℤ
i : K ⟶ L
w✝¹ : Mono i
w✝ : QuasiIso i
hL : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE (n - 1)
this✝¹ : L.IsGE n
this✝ : QuasiIso (L.πTruncGE n)
this : Injective (opcycles L n)
q : ℤ
h : q < n
⊢ Injective ((L.truncGE n).X q)

Tactic:
exact (isZero_of_isStrictlyGE _ n _ h).injective

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₄
w : TwoSquare T L R B
inst✝² : ∀ (F : C₁ ⥤ D), L.HasLeftKanExtension F
inst✝¹ : ∀ (F : C₂ ⥤ D), R.HasPointwiseLeftKanExtension F
inst✝ : w.GuitartExact
⊢ IsIso w.lanBaseChange

Tactic:
by
  rw [NatTrans.isIso_iff_isIso_app]
  infer_instance

Goal state after:
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
K : CochainComplex (InjectiveObject C) ℤ
n✝ : ℤ
hn : K.IsStrictlyGE n✝
L : HomologicalComplex C (ComplexShape.up ℤ) := ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K
n : ℤ
⊢ Injective (L.X n)

Tactic:
dsimp [L]

Goal state after:
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
K : CochainComplex (InjectiveObject C) ℤ
n✝ : ℤ
hn : K.IsStrictlyGE n✝
L : HomologicalComplex C (ComplexShape.up ℤ) := ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K
n : ℤ
⊢ Injective (K.X n).obj
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
d : ℤ
inst✝¹ : K.IsStrictlyLE d
inst✝ : ∀ (n : ℤ), Projective (K.X n)
L : CochainComplex Cᵒᵖ ℤ := (opEquivalence C).functor.obj (op K)
n : ℤ
⊢ Injective (L.X n)

Tactic:
dsimp [L]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
d : ℤ
inst✝¹ : K.IsStrictlyLE d
inst✝ : ∀ (n : ℤ), Projective (K.X n)
L : CochainComplex Cᵒᵖ ℤ := (opEquivalence C).functor.obj (op K)
n : ℤ
⊢ Injective (op (K.X (-n)))
Module: Mathlib.Algebra.Homology.EulerCharacteristic

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
j✝ : ℤ
⊢ j✝.negOnePow = -(j✝ + 1).negOnePow

Tactic:
simp [Int.negOnePow_succ]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ : ι
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
hi₀₁ : c.Rel i₀ k₀
h : i₀ ≠ k₀
φ₁ : X₁ ⟶ K.X k₀
comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0
⊢ (if k₀ = k₀ then 𝟙 ((double f hi₀₁).X k₀) ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ 𝟙 (K.X k₀) else 0) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
⊢ shiftFunctor C (m + n) ≅ shiftFunctor C m ⋙ shiftFunctor C n

Tactic:
by
  refine NatIso.ofComponents (fun X => mkIso (shiftAdd X.obj _ _) ?_) (fun f => ?_)
  · dsimp
    rw [← cancel_epi ((shiftFunctorAdd C m n).inv.app X.obj)]
    simp only [Category.assoc, Iso.inv_hom_id_app_assoc]
    rw [← NatTrans.naturality_assoc]
    dsimp
    simp only [Functor.map_comp, Category.assoc,
      shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app 1 m n X.obj,
      Iso.inv_hom_id_app_assoc]
  · ext; dsimp; exact NatTrans.naturality _ _

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

Goal state before:
pp: case neg
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i₁ i₂ j : I
h₁ : c.Rel i₂ (c.next i₂)
h₂ : ¬c.π c c (i₁, c.next i₂) = j
⊢ mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j = 0

Tactic:
· rw [mapBifunctor.d₂_eq_zero' _ _ _ _ _ h₁ _ h₂]

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

Goal state before:
pp: case e_a
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i : I
⊢ GradedObject.Monoidal.tensorUnit₀.hom ≫ GradedObject.Monoidal.tensorUnit₀.inv ≫ (tensorUnitIso C c).hom 0 =
    GradedObject.Monoidal.tensorUnit₀.hom ≫ (singleObjXSelf c 0 (𝟙_ C)).inv

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
case e_a
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i : I
⊢ (tensorUnitIso C c).hom 0 = GradedObject.Monoidal.tensorUnit₀.hom ≫ (singleObjXSelf c 0 (𝟙_ C)).inv
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
⊢ mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ =
    (mapBifunctorLeftUnitor F X e p hp Y).hom ≫
      (mapBifunctorLeftUnitor F X e p hp Y).inv ≫ mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
⊢ mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ = mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ