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

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ (mapHomologicalComplexObjXIso φ H i).inv = H.map (inrX φ i)

Tactic:
by_cases hi : c.Rel i (c.next i)

Goal state after:
case pos
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
hi : c.Rel i (c.next i)
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ (mapHomologicalComplexObjXIso φ H i).inv = H.map (inrX φ i)

case neg
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
hi : ¬c.Rel i (c.next i)
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ (mapHomologicalComplexObjXIso φ H i).inv = H.map (inrX φ i)
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

Tactic:
by_cases hi : c.Rel i (c.next i)

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
⊢ ∀ {X Y : CochainComplex C ℤ} (f : X ⟶ Y),
    (shiftFunctor C n₁₂).map f ≫ (Hom.isoOfComponents (fun i ↦ Y.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯).hom =
      (Hom.isoOfComponents (fun i ↦ X.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯).hom ≫
        (shiftFunctor C n₁ ⋙ shiftFunctor C n₂).map f

Tactic:
intros; ext; simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
x : Rˣ
⊢ (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn

Tactic:
apply leftUnshift_smul

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n : ℕ
f : T₁ ⟶ T₂
⊢ ↑n.succ • f = ↑n • f + f

Tactic:
by ext <;> apply SubNegMonoid.zsmul_succ'

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

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
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
inst✝³ : F₁.CommShift A
inst✝² : F₂.CommShift A
inst✝¹ : IsIso τ
inst✝ : CommShift τ A
⊢ CommShift (inv τ) A

Tactic:
have : NatTrans.CommShift (asIso τ).hom A := by assumption

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
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
inst✝³ : F₁.CommShift A
inst✝² : F₂.CommShift A
inst✝¹ : IsIso τ
inst✝ : CommShift τ A
this : CommShift (asIso τ).hom A
⊢ CommShift (inv τ) A
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
⊢ (g ≫ φ.hom₁) ≫ T'.invRotate.mor₂ = 0

Tactic:
by dsimp; rw [assoc, ← φ.comm₁, hf]

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

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✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasZeroObject D
inst✝⁸ : Preadditive C
inst✝⁷ : Preadditive D
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Pretriangulated D
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
inst✝² : F₁.CommShift ℤ
inst✝¹ : F₂.CommShift ℤ
inst✝ : NatTrans.CommShift e.hom ℤ
⊢ F₂.IsTriangulated → F₁.IsTriangulated

Tactic:
· intro
    have : NatTrans.CommShift e.symm.hom ℤ := inferInstanceAs (NatTrans.CommShift e.inv ℤ)
    exact isTriangulated_of_iso e.symm

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

Goal state before:
pp: case h_map.nil
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
X Y : Paths V
⊢ Φ.map Quiver.Path.nil = 𝟙 (Φ.obj X)

Tactic:
apply Functor.map_id

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

Goal state before:
pp: case refine_1
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 ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ ↑H ≫ S.f.f i ≫ S.X₂.d i (c.next i) = 0

Tactic:
reassoc_of% H.2,

Goal state after:
case refine_1
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 ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ k ≫ S.X₂.iCycles i ≫ S.X₂.d i (c.next i) = 0
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case inl
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : LocQuiver W
f : X.obj ⟶ Y.obj
⊢ G.obj X.obj ⟶ G.obj Y.obj

pp: case inr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : LocQuiver W
g : Y.obj ⟶ X.obj
hg : W g
⊢ G.obj X.obj ⟶ G.obj Y.obj

Tactic:
· exact G.map f

Goal state after:
case inr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : LocQuiver W
g : Y.obj ⟶ X.obj
hg : W g
⊢ G.obj X.obj ⟶ G.obj Y.obj
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✝² : Φ.functor.IsEquivalence
inst✝¹ : Φ.IsInduced
inst✝ : W₂.RespectsIso
⊢ W₂ ≤ W₁.inverseImage Φ.functor.inv

Tactic:
simp only [← Φ.inverseImage_eq]
    intro X Y f hf
    exact (W₂.arrow_mk_iso_iff
      (Arrow.isoMk (Φ.functor.asEquivalence.counitIso.app _)
        (Φ.functor.asEquivalence.counitIso.app _))).2 hf

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
| W f

Tactic:
← @IsCompatibleWithShift.condition _ _ W A _ _ _ a

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
| W.inverseImage (shiftFunctor C a) f
Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝¹² : Category.{v_1, u_1} C₁
inst✝¹¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst✝¹⁰ : AddMonoid M
inst✝⁹ : HasShift C₁ M
inst✝⁸ : HasShift C₂ M
inst✝⁷ : Φ.functor.CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst✝⁶ : Category.{v_3, u_4} D₁
inst✝⁵ : Category.{v_4, u_5} D₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : HasShift D₁ M
inst✝² : HasShift D₂ M
inst✝¹ : L₁.CommShift M
inst✝ : L₂.CommShift M
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
⊢ NatTrans.CommShift e.hom M

Tactic:
let := Φ.commShift M L₁ L₂ G e

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝¹² : Category.{v_1, u_1} C₁
inst✝¹¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst✝¹⁰ : AddMonoid M
inst✝⁹ : HasShift C₁ M
inst✝⁸ : HasShift C₂ M
inst✝⁷ : Φ.functor.CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst✝⁶ : Category.{v_3, u_4} D₁
inst✝⁵ : Category.{v_4, u_5} D₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : HasShift D₁ M
inst✝² : HasShift D₂ M
inst✝¹ : L₁.CommShift M
inst✝ : L₂.CommShift M
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
this : G.CommShift M := Φ.commShift M L₁ L₂ G e
⊢ NatTrans.CommShift e.hom M
Module: Mathlib.CategoryTheory.Localization.Triangulated

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
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 ℤ
inst✝² : Preadditive D
inst✝¹ : L.Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
T : Triangle D
⊢ T.rotate ∈ L.essImageDistTriang → T ∈ L.essImageDistTriang

Tactic:
rintro ⟨T', e', hT'⟩
    exact ⟨T'.invRotate, (triangleRotation D).unitIso.app T ≪≫ (invRotate D).mapIso e' ≪≫
      L.mapTriangleInvRotateIso.app T', inv_rot_of_distTriang T' hT'⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P.colimitsClosure J = (P.op.limitsClosure fun a ↦ (J a)ᵒᵖ).unop

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P.colimitsClosure J ≤ (P.op.limitsClosure fun a ↦ (J a)ᵒᵖ).unop

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ (P.op.limitsClosure fun a ↦ (J a)ᵒᵖ).unop ≤ P.colimitsClosure J
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
⊢ (P.strictLimitsClosureIter J κ.ord).isoClosure = P.limitsClosure J

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
⊢ (P.strictLimitsClosureIter J κ.ord).isoClosure ≤ P.limitsClosure J

case refine_2
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
⊢ P.limitsClosure J ≤ (P.strictLimitsClosureIter J κ.ord).isoClosure
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
X Y : C
φ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
e : L₁ ⋙ (Localization.uniq L₁ L₂ W).functor ≅ L₂ := Localization.compUniqFunctor L₁ L₂ W
⊢ (Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) ≫ e.hom.app Y =
    (Localization.compUniqFunctor L₁ L₂ W).hom.app X ≫
      φ.map L₂ ⋯ ≫ (Localization.compUniqFunctor L₁ L₂ W).inv.app Y ≫ e.hom.app Y

Tactic:
e.inv_hom_id_app,

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
X Y : C
φ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
e : L₁ ⋙ (Localization.uniq L₁ L₂ W).functor ≅ L₂ := Localization.compUniqFunctor L₁ L₂ W
⊢ (Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) ≫ e.hom.app Y =
    (Localization.compUniqFunctor L₁ L₂ W).hom.app X ≫ φ.map L₂ ⋯ ≫ 𝟙 (L₂.obj Y)
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
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
L : C ⥤ D
inst✝ : L.IsLocalization W
this : IsIso (L.map (z₂.s ≫ z₃.s))
⊢ z₁.map L ⋯ ≫ L.map (z₂.f ≫ z₃.s) = L.map { Y' := z₃.Y', f := z₁.f ≫ z₃.f, s := z₂.s ≫ z₃.s, hs := ⋯ }.f

Tactic:
h₃,

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
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
L : C ⥤ D
inst✝ : L.IsLocalization W
this : IsIso (L.map (z₂.s ≫ z₃.s))
⊢ z₁.map L ⋯ ≫ L.map (z₁.s ≫ z₃.f) = L.map { Y' := z₃.Y', f := z₁.f ≫ z₃.f, s := z₂.s ≫ z₃.s, hs := ⋯ }.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
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
⊢ F.homologicalKernel Z ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
simp only [mem_homologicalKernel_iff, h₁, ← h₂, ← h₃]

Goal state after:
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
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
⊢ (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) ↔ ∀ (n : ℤ), IsIso ((F.shift n).map 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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ ∃ φ, f = φ.map L ⋯

Tactic:
refine ⟨φ.unop, Quiver.Hom.op_inj ?_⟩

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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ f.op = (φ.unop.map L ⋯).op
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
h : RetractArrow f g
hg : Epi g
Z✝ : C
α β : x✝² ⟶ Z✝
w : f ≫ α = f ≫ β
⊢ Arrow.Hom.right h.r ≫ α = Arrow.Hom.right h.r ≫ β

Tactic:
← cancel_epi g,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
h : RetractArrow f g
hg : Epi g
Z✝ : C
α β : x✝² ⟶ Z✝
w : f ≫ α = f ≫ β
⊢ g ≫ Arrow.Hom.right h.r ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
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
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : C ⥤ D
τ : F ⟶ G
inst✝² : F.CommShift M
inst✝¹ : G.CommShift M
inst✝ : NatTrans.CommShift τ M
⊢ f.map F ≫ (shiftFunctor D a).map (τ.app Y) = τ.app X ≫ f.map G

Tactic:
map,

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
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : C ⥤ D
τ : F ⟶ G
inst✝² : F.CommShift M
inst✝¹ : G.CommShift M
inst✝ : NatTrans.CommShift τ M
⊢ (F.map f ≫ (Functor.commShiftIso F a).hom.app Y) ≫ (shiftFunctor D a).map (τ.app Y) = τ.app X ≫ f.map G
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
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : C ⥤ D
τ : F ⟶ G
inst✝² : F.CommShift M
inst✝¹ : G.CommShift M
inst✝ : NatTrans.CommShift τ M
⊢ (F.map f ≫ (Functor.commShiftIso F a).hom.app Y) ≫ (shiftFunctor D a).map (τ.app Y) = τ.app X ≫ f.map G

Tactic:
map,

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
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : C ⥤ D
τ : F ⟶ G
inst✝² : F.CommShift M
inst✝¹ : G.CommShift M
inst✝ : NatTrans.CommShift τ M
⊢ (F.map f ≫ (Functor.commShiftIso F a).hom.app Y) ≫ (shiftFunctor D a).map (τ.app Y) =
    τ.app X ≫ G.map f ≫ (Functor.commShiftIso G a).hom.app Y
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
h : QuasiIsoAt f i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Tactic:
exact h.quasiIso

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ δ 0 1 (descCochain g 0 (Cochain.ofHom (inr (f ≫ g))) ⋯) +
      (↑(descCocycle g (Cochain.ofHom (inr f)) 0 ⋯ ⋯)).comp (Cochain.ofHom (mappingConeCompTriangle f g).mor₁) ⋯ =
    0

Tactic:
ext p _ rfl
      dsimp [mappingConeCompTriangle, map]
      simp [ext_from_iff _ _ _ rfl, inl_v_d_assoc _ (p + 1) p (p + 2) (by lia) (by lia)]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : DerivedCategory C
f : K ⟶ L
hf : ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f)
g : Arrow (HomotopyCategory C (ComplexShape.up ℤ)) := Qh.mapArrow.objPreimage (Arrow.mk f)
⊢ MorphismProperty.isomorphisms (DerivedCategory C) (Qh.mapArrow.obj (Qh.mapArrow.objPreimage (Arrow.mk f))).hom

Tactic:
change IsIso (Qh.map g.hom)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : DerivedCategory C
f : K ⟶ L
hf : ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f)
g : Arrow (HomotopyCategory C (ComplexShape.up ℤ)) := Qh.mapArrow.objPreimage (Arrow.mk f)
⊢ IsIso (Qh.map g.hom)
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
⊢ ¬(c'.Rel (c'.prev (e.f k)) (e.f k) ∧ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f k))

Tactic:
simp only [not_and, not_forall, not_not]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hk : c.Rel j k
⊢ c'.Rel (c'.prev (e.f k)) (e.f k) → ∃ x, c'.Rel (e.f x) (e.f k)
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryGE j
inst✝ : e.IsTruncLE
i : ι
hi : e.f i = c'.prev (e.f j)
⊢ c'.Rel (e.f i) (e.f j)

Tactic:
simpa only [hi] using hj.1

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
⊢ ¬(c'.Rel (e.f i) (c'.next (e.f i)) ∧ ∀ (k : ι), ¬c'.Rel (e.f i) (e.f k))

Tactic:
simp only [not_and, not_forall, not_not]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
⊢ c'.Rel (e.f i) (c'.next (e.f i)) → ∃ x, c'.Rel (e.f i) (e.f x)