mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: case refine_3
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
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ w₁₃ ≫
      (shiftFunctor C 1).map ((shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₃) ≫
        (shiftFunctor C 1).map ((shiftFunctor C (-1)).map o.m₃) ≫
          (shiftFunctor C 1).map ((shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Z₂₃) =
    w₂₃

Tactic:
shift_shiftFunctorCompIsoId_hom_app,

Goal state after:
case refine_3
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
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ w₁₃ ≫
      (shiftFunctor C 1).map ((shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₃) ≫
        (shiftFunctor C 1).map ((shiftFunctor C (-1)).map o.m₃) ≫
          (shiftFunctorCompIsoId C (-1) 1 ⋯).hom.app ((shiftFunctor C 1).obj Z₂₃) =
    w₂₃
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k :
  A ⟶
    { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
        zero := ⋯ }.X₂
hk :
  k ≫
      { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
          zero := ⋯ }.g =
    0
⊢ { l //
    l ≫
        { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
            zero := ⋯ }.f =
      k }

Tactic:
dsimp at k hk ⊢
    have H := KernelFork.IsLimit.lift' hi (k ≫ S.X₂.iCycles i) (by
      dsimp
      rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp])
    dsimp at H
    refine ⟨S.X₁.liftCycles H.1 _ rfl ?_, ?_⟩
    · rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]
    · rw [← cancel_mono (S.X₂.iCycles i), liftCycles_comp_cyclesMap, liftCycles_i, H.2]

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝ : Φ.IsLocalizedEquivalence
⊢ Φ.op.IsLocalizedEquivalence

Tactic:
let G := Φ.localizedFunctor W₁.Q W₂.Q
  let : CatCommSq Φ.op.functor W₁.Q.op W₂.Q.op G.op :=
    ⟨NatIso.op (CatCommSq.iso Φ.functor W₁.Q W₂.Q G).symm⟩
  have := Φ.isEquivalence W₁.Q W₂.Q G
  exact IsLocalizedEquivalence.mk' Φ.op W₁.Q.op W₂.Q.op G.op

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case succ
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) k'
hkj : k ≤ Order.succ k'
⊢ (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k')

Tactic:
obtain hkj | rfl := hkj.lt_or_eq
    · refine (hkk' ((Order.lt_succ_iff_of_not_isMax hk').mp hkj)).trans ?_
      dsimp
      rw [transfiniteIterate_succ _ _ _ hk']
      apply hφ
    · rfl

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
f g : L.obj X ⟶ L.obj Y
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
obtain ⟨φ, rfl, rfl⟩ := exists_leftFraction₂ L W f g

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
⊢ G.map (φ.fst.map L ⋯ + φ.snd.map L ⋯) = G.map (φ.fst.map L ⋯) + G.map (φ.snd.map L ⋯)
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT (α i) κ
⊢ HasCardinalLT ((i : ι) × α i) κ

Tactic:
have : Fact (Cardinal.lift.{max u v} κ).IsRegular := ⟨Cardinal.IsRegular.lift Fact.out⟩
  have := hasCardinalLT_sigma'
    (fun (i : ULift.{max v w} ι) ↦ ULift.{max u w} (α (ULift.down i)))
    (Cardinal.lift.{max u v} κ) (by simpa)
    (fun i ↦ by simpa using hα (ULift.down i))
  rw [hasCardinalLT_lift_iff] at this
  exact this.of_surjective (fun ⟨i, a⟩ ↦ ⟨ULift.down i, ULift.down a⟩)
    (fun ⟨i, a⟩ ↦ ⟨⟨ULift.up i, ULift.up a⟩, rfl⟩)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
B : BinaryFan X Y
hB : IsLimit B
hX : P X
hY : P Y
⊢ ∀ (j : Discrete WalkingPair), P ((Limits.pair X Y).obj j)

Tactic:
by rintro ⟨_ | _⟩ <;> assumption

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
a b c : A
h : a + b = c
inst✝ : P.IsClosedUnderIsomorphisms
⊢ (P.shift b).shift a = P.shift c

Tactic:
by
  ext X
  exact P.prop_iff_of_iso ((shiftFunctorAdd' C a b c h).symm.app X)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
B : BinaryCofan X Y
hB : IsColimit B
hX : P X
hY : P Y
⊢ ∀ (j : Discrete WalkingPair), P ((Limits.pair X Y).obj j)

Tactic:
by rintro ⟨_ | _⟩ <;> assumption

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasFiniteCoproducts C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
this : P.IsClosedUnderIsomorphisms
⊢ P.IsClosedUnderFiniteCoproducts

Tactic:
have := hasFiniteCoproducts_of_has_binary_and_initial (C := P.FullSubcategory)

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasFiniteCoproducts C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
this✝ : P.IsClosedUnderIsomorphisms
this : HasFiniteCoproducts P.FullSubcategory
⊢ P.IsClosedUnderFiniteCoproducts
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : C ⥤ E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' ⟶ Z
t₂ : a₂.Y' ⟶ Z
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
h : W (a₁.s ≫ t₁)
this : IsIso (F.map (a₁.s ≫ t₁))
⊢ a₁.map F hF ≫ F.map (a₁.s ≫ t₁) = a₂.map F hF ≫ F.map (a₁.s ≫ t₁)

Tactic:
F.map_comp,

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : C ⥤ E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' ⟶ Z
t₂ : a₂.Y' ⟶ Z
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
h : W (a₁.s ≫ t₁)
this : IsIso (F.map (a₁.s ≫ t₁))
⊢ a₁.map F hF ≫ F.map a₁.s ≫ F.map t₁ = a₂.map F hF ≫ F.map a₁.s ≫ F.map t₁
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : C ⥤ E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' ⟶ Z
t₂ : a₂.Y' ⟶ Z
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
h : W (a₁.s ≫ t₁)
this : IsIso (F.map (a₁.s ≫ t₁))
⊢ F.map (a₂.f ≫ t₂) = a₂.map F hF ≫ F.map (a₂.s ≫ t₂)

Tactic:
F.map_comp,

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : C ⥤ E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' ⟶ Z
t₂ : a₂.Y' ⟶ Z
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
h : W (a₁.s ≫ t₁)
this : IsIso (F.map (a₁.s ≫ t₁))
⊢ F.map a₂.f ≫ F.map t₂ = a₂.map F hF ≫ F.map (a₂.s ≫ t₂)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : C ⥤ E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' ⟶ Z
t₂ : a₂.Y' ⟶ Z
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
h : W (a₁.s ≫ t₁)
this : IsIso (F.map (a₁.s ≫ t₁))
⊢ F.map a₂.f ≫ F.map t₂ = a₂.map F hF ≫ F.map (a₂.s ≫ t₂)

Tactic:
F.map_comp,

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : C ⥤ E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' ⟶ Z
t₂ : a₂.Y' ⟶ Z
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
h : W (a₁.s ≫ t₁)
this : IsIso (F.map (a₁.s ≫ t₁))
⊢ F.map a₂.f ≫ F.map t₂ = a₂.map F hF ≫ F.map a₂.s ≫ F.map t₂
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction f.Y' g.Y'
fac : g.f ≫ z.s = f.s ≫ z.f
this✝ : IsIso (F.map g.s)
this : IsIso (F.map z.s)
⊢ F.map (f.f ≫ z.f) = f.map F hF ≫ F.map (f.s ≫ z.f)

Tactic:
F.map_comp,

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction f.Y' g.Y'
fac : g.f ≫ z.s = f.s ≫ z.f
this✝ : IsIso (F.map g.s)
this : IsIso (F.map z.s)
⊢ F.map f.f ≫ F.map z.f = f.map F hF ≫ F.map (f.s ≫ z.f)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction f.Y' g.Y'
fac : g.f ≫ z.s = f.s ≫ z.f
this✝ : IsIso (F.map g.s)
this : IsIso (F.map z.s)
⊢ F.map f.f ≫ F.map z.f = f.map F hF ≫ F.map (f.s ≫ z.f)

Tactic:
F.map_comp,

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction f.Y' g.Y'
fac : g.f ≫ z.s = f.s ≫ z.f
this✝ : IsIso (F.map g.s)
this : IsIso (F.map z.s)
⊢ F.map f.f ≫ F.map z.f = f.map F hF ≫ F.map f.s ≫ F.map z.f
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
⊢ F.homologicalKernel.trW f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f
  apply (F.homologicalKernel.trW_iff_of_distinguished _ hT).trans
  have h₁ := fun n => (F.homologySequence_exact₃ _ hT n _ rfl).isZero_X₂_iff
  have h₂ := fun n => F.homologySequence_mono_shift_map_mor₁_iff _ hT n _ rfl
  have h₃ := fun n => F.homologySequence_epi_shift_map_mor₁_iff _ hT n
  dsimp at h₁ h₂ h₃ ⊢
  simp only [mem_homologicalKernel_iff, h₁, ← h₂, ← h₃]
  constructor
  · intro h n
    obtain ⟨m, rfl⟩ : ∃ (m : ℤ), n = m + 1 := ⟨n - 1, by simp⟩
    have := (h (m + 1)).1
    have := (h m).2
    apply isIso_of_mono_of_epi
  · intros
    constructor <;> infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
⊢ c = 0

Tactic:
← h,

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
⊢ b + a = 0
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
c : M
h : 0 + 0 = c
⊢ c = 0

Tactic:
← h,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
c : M
h : 0 + 0 = c
⊢ 0 + 0 = 0
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderRetracts ↔ P.retracts ≤ P

Tactic:
isStableUnderRetracts_iff

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f) ↔ P.retracts ≤ P
Module: Mathlib.CategoryTheory.Localization.Triangulated

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✝¹⁴ : HasShift C ℤ
inst✝¹³ : Preadditive C
inst✝¹² : HasZeroObject C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
inst✝⁹ : HasShift D ℤ
inst✝⁸ : L.CommShift ℤ
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : W.HasLeftCalculusOfFractions
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.IsTriangulated
inst✝ : IsTriangulated C
this : (L.mapComposableArrows 2).EssSurj
⊢ IsTriangulated D

Tactic:
exact isTriangulated_of_essSurj_mapComposableArrows_two L

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
p : ℤ
⊢ (inl φ).v p p ⋯ ≫ (fst φ).f p = 𝟙 (K.X p)

Tactic:
by
  simp [inl, fst, Cochain.rightShift_v (n := -1) _ _ _ _ p _ _ (p + -1) (by lia),
    Cochain.leftShift_v (n := 1) _ _ _ _ _ p _ (p + -1) (by lia)]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasBinaryBiproducts C
⊢ (triangle φ).rotate ≅ mappingCone.triangle φ

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
    ((shiftFunctorCompIsoId _ (-1 : ℤ) 1 (by lia)).app _)
    (by simp) (by simp [triangle]) ?_
  dsimp
  ext n
  simp [fst, mappingCone.triangle, Cochain.leftShift_v _ _ _ _ _ _ _ _ rfl,
    Cochain.rightShift_v _ _ _ _ _ _ _ _ rfl,
    shiftFunctorCompIsoId, shiftFunctorAdd'_inv_app_f', shiftFunctorZero_hom_app_f]

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : e.r (e.f k) = some i
⊢ e.f i = e.f k

Tactic:
r_f

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i k : ι
hi : some k = some i
⊢ e.f i = e.f k
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁴ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝³ : HasZeroMorphisms V
K L : HomologicalComplex Vᵒᵖ c
φ : K ⟶ L
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : QuasiIsoAt φ i
⊢ QuasiIsoAt ((unopFunctor V c).map φ.op) i

Tactic:
quasiIsoAt_unopFunctor_map_iff

Goal state after:
ι : Type u_1
V : Type u_2
inst✝⁴ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝³ : HasZeroMorphisms V
K L : HomologicalComplex Vᵒᵖ c
φ : K ⟶ L
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : QuasiIsoAt φ i
⊢ QuasiIsoAt φ i
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inr
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ (extend.XIso K hi).hom ≫ 0 ≫ (extend.XIso K hj).inv = 0

pp: case inr.inr.a
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ ¬c.Rel i j

Tactic:
zero_comp,

Goal state after:
case inr.inr
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ (extend.XIso K hi).hom ≫ 0 = 0

case inr.inr.a
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ ¬c.Rel i j
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inr.inr
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
⊢ (extend.XIso K hi).hom ≫ 0 ≫ (extend.XIso K hk).inv = 0

Tactic:
zero_comp,

Goal state after:
case inr.inr.inr
ι : 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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
⊢ (extend.XIso K hi).hom ≫ 0 = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr
ι : 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✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
⊢ (K.extendXIso e hi).hom ≫ 0 ≫ (K.extendXIso e ⋯).inv = 0

pp: case inr.a
ι : 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✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
⊢ ¬c.Rel i j

Tactic:
zero_comp,

Goal state after:
case inr
ι : 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✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
⊢ (K.extendXIso e hi).hom ≫ 0 = 0

case inr.a
ι : 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✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
⊢ ¬c.Rel i j