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

Goal state before:
pp: case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }.d i j
i j : ι
hij : c.Rel i j
⊢ d₁ i j = d₂ i j

Tactic:
simpa only [comp_id, id_comp, eqToHom_refl] using h_d i j hij

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

Goal state before:
pp: ⊢ ¬∃ j, (ComplexShape.down ℕ).Rel 0 j

Tactic:
push Not

Goal state after:
⊢ ∀ (j : ℕ), ¬(ComplexShape.down ℕ).Rel 0 j
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ⊢ ¬∃ j, (ComplexShape.up ℕ).Rel j 0

Tactic:
push Not

Goal state after:
⊢ ∀ (j : ℕ), ¬(ComplexShape.up ℕ).Rel j 0
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
⊢ (if hi : i = j then (singleObjXIsoOfEq c j A i hi).hom ≫ φ ≫ (K.XIsoOfEq hi).inv else 0) ≫ K.d i k =
    0 ≫ if hi : k = j then (singleObjXIsoOfEq c j A k hi).hom ≫ φ ≫ (K.XIsoOfEq hi).inv else 0

Tactic:
rw [zero_comp]

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
⊢ (if hi : i = j then (singleObjXIsoOfEq c j A i hi).hom ≫ φ ≫ (K.XIsoOfEq hi).inv else 0) ≫ K.d i k = 0
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ ¬∃ j_1, c.Rel j_1 j

Tactic:
push Not

Goal state after:
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ ∀ (j_1 : ι), ¬c.Rel j_1 j
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬c.Rel i (c.next i)
⊢ ¬∃ j, c.Rel i j

Tactic:
rintro ⟨j, hj⟩

Goal state after:
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬c.Rel i (c.next i)
j : ι
hj : c.Rel i j
⊢ False
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬c.Rel i (c.next i)
j : ι
hj : c.Rel i j
⊢ False

Tactic:
have : c.next i = j := c.next_eq' hj

Goal state after:
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬c.Rel i (c.next i)
j : ι
hj : c.Rel i j
this : c.next i = j
⊢ False
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
i j : α
h : i ≠ j + 1
⊢ of.d X d i j = 0

Tactic:
by
  simp [of.d, dif_neg h]

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

Goal state before:
pp: V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
i j : α
h : i + 1 ≠ j
⊢ of.d X d i j = 0

Tactic:
by
  simp [of.d, dif_neg h]

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

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
i j : ι
P : C
inst✝ : Projective P
hij : ¬j = i
⊢ Projective (((single C c i).obj P).X j)

Tactic:
exact (isZero_single_obj_X _ _ _ _ hij).projective

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (linearCombination S ⇑(D R S)).ker = kerTotal R S

Tactic:
apply le_antisymm
  · conv_rhs => rw [← (KaehlerDifferential.kerTotal R S).ker_mkQ]
    rw [← KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination]
    exact LinearMap.ker_le_ker_comp _ _
  · rw [KaehlerDifferential.kerTotal, Submodule.span_le]
    rintro _ ((⟨⟨x, y⟩, rfl⟩ | ⟨⟨x, y⟩, rfl⟩) | ⟨x, rfl⟩) <;> simp [LinearMap.mem_ker]

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

Goal state before:
pp: case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
i j : ι
h✝ : ¬c.Rel j i
⊢ 0 ≫ g.f j = 0

Tactic:
rw [zero_comp]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v, u_1} C
inst✝³ : Category.{v', u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ -1 + e = d

Tactic:
← he,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v, u_1} C
inst✝³ : Category.{v', u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ -1 + (1 + d) = d
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
⊢ (γ.shift a).v p q hpq = (K.shiftFunctorObjXIso a p p' hp').hom ≫ γ.v p' q' ⋯ ≫ (L.shiftFunctorObjXIso a q q' hq').inv

Tactic:
subst hp' hq'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a p q : ℤ
hpq : p + n = q
⊢ (γ.shift a).v p q hpq =
    (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯ ≫ (L.shiftFunctorObjXIso a q (q + a) ⋯).inv
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
n : A
⊢ ∀ (X : D), (Induced.add F s i n 0).hom.app X = eqToHom ⋯ ≫ (Induced.zero F s i).inv.app ((s n).obj X)

Tactic:
suffices (Induced.add F s i n 0).hom =
            eqToHom (by rw [add_zero]; rfl) ≫ whiskerLeft (s n) (Induced.zero F s i).inv by
          intro X
          simpa using NatTrans.congr_app this X
        apply ((whiskeringLeft C D D).obj F).map_injective
        ext X
        dsimp
        erw [Induced.add_hom_app_obj, dcongr_arg (fun a => (i a).hom.app X) (add_zero n),
          ← cancel_mono ((s 0).map ((i n).hom.app X)), Category.assoc,
          Category.assoc, Category.assoc, Category.assoc, Category.assoc,
          Category.assoc, ← (s 0).map_comp, Iso.inv_hom_id_app, Functor.map_id, Category.comp_id,
          ← NatTrans.naturality, Induced.zero_inv_app_obj,
          shiftFunctorAdd_add_zero_hom_app]
        simp [eqToHom_map, eqToHom_app]

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

Goal state before:
pp: C : Type u_3
D : Type u_1
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
⊢ (shiftFunctorZero D A).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Tactic:
by
  simp only [ShiftMkCore.shiftFunctorZero_eq, HasShift.Induced.zero_hom_app_obj]

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 : ℤ
γ : Cochain K L n
a : ℤ
x : R
⊢ (x • γ).shift a = x • γ.shift a

Tactic:
ext p q hpq
  dsimp
  simp only [shift_v', smul_v]

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 M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n a n' : ℤ
hn' : n' + a = n
x : R
γ : Cochain K L n
⊢ (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'

Tactic:
simp only [rightShift_smul]

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 M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n a n' : ℤ
hn : n + a = n'
x : R
γ : Cochain K L n
⊢ (leftShiftAddEquiv K L n a n' hn) (x • γ) = x • (leftShiftAddEquiv K L n a n' hn) γ

Tactic:
by dsimp; simp only [leftShift_smul]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 B.obj₂

Tactic:
by rw [← comp_hom₂, e.inv_hom_id, id_hom₂]

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

Goal state before:
pp: case h₁
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 + 1) • f).hom₁ = (n • f + f).hom₁

Tactic:
apply AddMonoid.nsmul_succ

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

Goal state before:
pp: case h₂
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 + 1) • f).hom₂ = (n • f + f).hom₂

Tactic:
apply AddMonoid.nsmul_succ

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

Goal state before:
pp: case h₃
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 + 1) • f).hom₃ = (n • f + f).hom₃

Tactic:
apply AddMonoid.nsmul_succ

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 + 1) • f = n • f + f

Tactic:
by ext <;> apply AddMonoid.nsmul_succ

Goal state after:
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₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
⊢ x₃ ≫ T.mor₃ = 0

Tactic:
rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        comp_distTriang_mor_zero₂₃ _ hT', comp_zero]

Goal state after:
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
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
ha'' : ∀ (j : J), ∃ g, (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun j ↦ (T j).obj₃) j = g ≫ (T j).mor₂
b : (j : J) → A ⟶ (T j).obj₂ := fun j ↦ ⋯.choose
hb : ∀ (j : J), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun j ↦ (T j).obj₃) j = b j ≫ (T j).mor₂
j : J
⊢ (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun j ↦ (T j).obj₃) j =
    (Pi.lift b ≫ (productTriangle T).mor₂) ≫ Pi.π (fun j ↦ (T j).obj₃) j

Tactic:
rw [hb]; simp

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

Goal state before:
pp: case refine_2.refine_3
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₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
⊢ LeftFractionRel p₂ (a₂.comp₀ b z₂)

Tactic:
have eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f := by
        rw [← fac₂', reassoc_of% fac₂]

Goal state after:
case refine_2.refine_3
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₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
⊢ LeftFractionRel p₂ (a₂.comp₀ b z₂)
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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
⊢ ((Hom.mk z₁).comp (Hom.mk z₂)).comp (Hom.mk z₃) = (Hom.mk z₁).comp ((Hom.mk z₂).comp (Hom.mk z₃))

Tactic:
Hom.comp_eq z₁ z₂,

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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
⊢ (z₁.comp z₂).comp (Hom.mk z₃) = (Hom.mk z₁).comp ((Hom.mk z₂).comp (Hom.mk z₃))
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✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ L.map (α.f ≫ β.f ≫ γ.s) = L.map (T₁.mor₁ ≫ γ.f)

Tactic:
rw [← cancel_mono (L.map β.s), assoc, assoc, hγ, ← cancel_mono (L.map γ.s),
        assoc, assoc, assoc, hα, MorphismProperty.LeftFraction.map_comp_map_s,
        ← Functor.map_comp] at fac
      rw [fac, ← Functor.map_comp_assoc, hβ, Functor.map_comp, Functor.map_comp,
        Functor.map_comp, assoc, MorphismProperty.LeftFraction.map_comp_map_s_assoc]

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

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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
h : LeftFractionRel φ ψ
⊢ φ.map L ⋯ = ψ.map L ⋯

Tactic:
simp only [← Localization.Hom.map_mk _ L (Localization.inverts _ _)]

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
h : LeftFractionRel φ ψ
⊢ (Localization.Hom.mk φ).map L ⋯ = (Localization.Hom.mk ψ).map L ⋯
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
T : Triangle C
hT : T ∈ distinguishedTriangles
X₁ : C
h₁ : P X₁
e₁ : T.obj₁ ≅ X₁
X₃ : C
h₃ : P X₃
e₃ : T.obj₃ ≅ X₃
⊢ (Triangle.mk (e₁.inv ≫ T.mor₁) (T.mor₂ ≫ e₃.hom) (e₃.inv ≫ T.mor₃ ≫ (shiftFunctor C 1).map e₁.hom)).mor₃ ≫
      (shiftFunctor C 1).map e₁.symm.hom =
    e₃.symm.hom ≫ T.mor₃

Tactic:
by
          dsimp
          simp only [assoc, ← Functor.map_comp, e₁.hom_inv_id,
            Functor.map_id, comp_id]

Goal state after:
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
R : Type u_5
inst✝³ : Ring R
inst✝² : Preadditive C
inst✝¹ : Linear R C
inst✝ : ∀ (a : M), Functor.Linear R (shiftFunctor C a)
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ α ≫ (r • (shiftFunctor C a).map β) ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    r • α ≫ (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
Linear.smul_comp,

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
R : Type u_5
inst✝³ : Ring R
inst✝² : Preadditive C
inst✝¹ : Linear R C
inst✝ : ∀ (a : M), Functor.Linear R (shiftFunctor C a)
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ α ≫ (r • (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z) =
    r • α ≫ (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Category.{v_4, u_4} E'
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
inst✝² : HasShift E' A
F G✝ H : SingleFunctors C D A
G : D ⥤ E
G' : E ⥤ E'
inst✝¹ : G.CommShift A
inst✝ : G'.CommShift A
n a a' : A
ha' : n + a = a'
⊢ (((F.postcomp G).postcomp G').shiftIso n a a' ha').hom ≫ ((F.functor a).associator G G').hom =
    whiskerRight ((F.functor a').associator G G').hom (shiftFunctor E' n) ≫
      ((F.postcomp (G ⋙ G')).shiftIso n a a' ha').hom

Tactic:
ext X
    simp [Functor.commShiftIso_comp_inv_app]

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

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✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ K.restrictionToTruncGE' e ≫ truncGE'Map φ e = restrictionMap φ e ≫ L.restrictionToTruncGE' e

Tactic:
restrictionToTruncGE'_naturality

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ restrictionMap φ e ≫ L.restrictionToTruncGE' e = restrictionMap φ e ≫ L.restrictionToTruncGE' e
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case left.inr.inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ j₂ : ι₂
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inr j₂)
⊢ Sum.inr i₂ = Sum.inr j₂

Tactic:
obtain rfl := e₂.injective_f h

Goal state after:
case left.inr.inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inr i₂)
⊢ Sum.inr i₂ = Sum.inr i₂
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case right
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
n : ι
⊢ ∃ a, fromSum e₁ e₂ a = n

Tactic:
obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union n

Goal state after:
case right.inl
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
⊢ ∃ a, fromSum e₁ e₂ a = e₁.f i₁

case right.inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
⊢ ∃ a, fromSum e₁ e₂ a = e₂.f i₂