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

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
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
p✝ q✝ : ℤ
hpq✝ : p✝ + n = q✝
⊢ (x✝² * x✝¹) • (↑x✝).v p✝ q✝ hpq✝ = x✝² • x✝¹ • (↑x✝).v p✝ q✝ hpq✝

Tactic:
smul_smul

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
p✝ q✝ : ℤ
hpq✝ : p✝ + n = q✝
⊢ (x✝² * x✝¹) • (↑x✝).v p✝ q✝ hpq✝ = (x✝² * x✝¹) • (↑x✝).v p✝ q✝ hpq✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
n₁ n₂ : ℤ
⊢ (inr φ).f n₁ ≫ (mappingCone φ).d n₁ n₂ = G.d n₁ n₂ ≫ (inr φ).f n₂

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
⊢ (inl φ).comp (Cochain.ofHom (desc φ α β eq)) ⋯ = α

Tactic:
by
  simp

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

Goal state before:
pp: case neg.hq'
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
h : ¬q = q'' - 1
⊢ q'' ≠ q'

pp: case neg.hq'
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
h : ¬q = q'' - 1
⊢ q'' - 1 ≠ q

Tactic:
all_goals lia

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 φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (-(↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F).d (n + 1) (n + 2)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    (mapHomologicalComplexXIso φ H n).hom ≫
        (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1) ≫
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯

Tactic:
d_snd_v _ _ _ rfl

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 φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (-(↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F).d (n + 1) (n + 2)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    (mapHomologicalComplexXIso φ H n).hom ≫
        ((↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ).f (n + 1) +
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj G).d n (n + 1)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
⊢ ∀ {a b : Quotient r} (f : a ⟶ b), P f

Tactic:
by
  rintro ⟨x⟩ ⟨y⟩ ⟨f⟩
  exact h f

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : Preadditive V
c : ComplexShape ι
inst✝ : HasZeroObject V
⊢ IsZero ((quotient V c).obj 0)

Tactic:
rw [IsZero.iff_id_eq_zero, ← (quotient V c).map_id, id_zero, Functor.map_zero]

Goal state after:
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
F : C ⥤ D
inst✝ : F.Additive
n : ℤ
X✝ Y✝ : HomologicalComplex C (ComplexShape.up ℤ)
x✝ : X✝ ⟶ Y✝
⊢ (shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)).map x✝ ≫
      (HomologicalComplex.Hom.isoOfComponents
          (fun x ↦
            Iso.refl
              (((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                    Y✝).X
                x))
          ⋯).hom =
    (HomologicalComplex.Hom.isoOfComponents
          (fun x ↦
            Iso.refl
              (((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                    X✝).X
                x))
          ⋯).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) n).map x✝

Tactic:
ext; dsimp; rw [id_comp, comp_id]

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
f g h : T₁ ⟶ T₂
⊢ f + g + h = f + (g + h)

Tactic:
ext <;> apply add_assoc

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 : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₁ ≫ T.mor₂ = 0

Tactic:
obtain ⟨c, hc⟩ :=
    complete_distinguished_triangle_morphism _ _ (contractible_distinguished T.obj₁) H (𝟙 T.obj₁)
      T.mor₁ rfl
  simpa only [contractibleTriangle_mor₂, zero_comp] using hc.left.symm

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

Goal state before:
pp: case pos.e_a.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ m'.negOnePow * ((a * n' + a * (a - 1) / 2).negOnePow * a.negOnePow) =
    a.negOnePow * ((a * m' + a * (a - 1) / 2).negOnePow * m.negOnePow)

Tactic:
· simp only [← Int.negOnePow_add, ← hn', ← hm', ← hnm]
      congr 1
      linarith

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
h : a + b = c
⊢ CategoryTheory.shiftFunctorAdd' (Triangle C) a b c h = shiftFunctorAdd' C a b c h

Tactic:
subst h
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd]
  apply shiftFunctorAdd_eq

Goal state after:
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 : ℤ
z : Cocycle K L n
L' : CochainComplex C ℤ
g : L ⟶ L'
⊢ equivHomShift (equivHomShift.symm (z.postcomp g)) =
    equivHomShift (equivHomShift.symm z ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map g)

Tactic:
simp [equivHomShift_comp_shift]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
n : ℤ
K L : CochainComplex C ℤ
φ : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh φ
⊢ (Triangle.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj T ∈ distinguishedTriangles C

Tactic:
exact ⟨_, _, _, ⟨Functor.mapIso _ e ≪≫ CochainComplex.mappingCone.shiftTrianglehIso φ n⟩⟩

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

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
inst✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
F : C ⥤ D
inst✝¹⁰ : F.CommShift ℤ
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
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
⊢ ∃ X Y f e₁ e₂, F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁

Tactic:
let e := F.mapArrow.objObjPreimageIso (Arrow.mk T.mor₁)

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
inst✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
F : C ⥤ D
inst✝¹⁰ : F.CommShift ℤ
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
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
e : F.mapArrow.obj (F.mapArrow.objPreimage (Arrow.mk T.mor₁)) ≅ Arrow.mk T.mor₁ :=
  F.mapArrow.objObjPreimageIso (Arrow.mk T.mor₁)
⊢ ∃ X Y f e₁ e₂, F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: case h
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ⋯
S' : ShortComplex C := ⋯
ι : S ⟶ S' := ⋯
hS : S.Exact
T : ShortComplex C := ⋯
T' : ShortComplex C := ⋯
π : T' ⟶ T := ⋯
hT : T.Exact
⊢ (ComposableArrows.mk₂ ((composableArrows₃ K i j).map' 0 1 ComposableArrows.isComplex₂_iff._proof_2 ⋯)
      ((composableArrows₃ K i j).map' 1 2 ComposableArrows.isComplex₂_iff._proof_4 ⋯)).Exact

pp: case h₀
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ⋯
S' : ShortComplex C := ⋯
ι : S ⟶ S' := ⋯
hS : S.Exact
T : ShortComplex C := ⋯
T' : ShortComplex C := ⋯
π : T' ⟶ T := ⋯
hT : T.Exact
⊢ (composableArrows₃ K i j).δ₀.Exact

Tactic:
· exact hS.exact_toComposableArrows

Goal state after:
case h₀
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C := ⋯
S' : ShortComplex C := ⋯
ι : S ⟶ S' := ⋯
hS : S.Exact
T : ShortComplex C := ⋯
T' : ShortComplex C := ⋯
π : T' ⟶ T := ⋯
hT : T.Exact
⊢ (composableArrows₃ K i j).δ₀.Exact
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} A
F : C ⥤ A
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
X Y : C
n a a' : M
ha' : n + a = a'
f : X ⟶ Y
⊢ (F.shift a').map f ≫ (F.shiftIso n a a' ha').inv.app Y =
    (F.shiftIso n a a' ha').inv.app X ≫ (F.shift a).map ((shiftFunctor C n).map f)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X)

Tactic:
← h.iso.hom.naturality (T.unitIso.hom.app X)

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)
Module: Mathlib.CategoryTheory.Localization.Predicate

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
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
hP : P.inverseImage (uniq W.Q L W).functor = ⊤
⊢ P = ⊤

Tactic:
← P.map_inverseImage_eq_of_isEquivalence (uniq W.Q L W).functor,

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
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
hP : P.inverseImage (uniq W.Q L W).functor = ⊤
⊢ (P.inverseImage (uniq W.Q L W).functor).map (uniq W.Q L W).functor = ⊤
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case refine_3
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
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ f'' = ψ.thd.map L ⋯

Tactic:
rw [← cancel_mono (L.map (β.s ≫ γ.s)), hβ]

Goal state after:
case refine_3
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
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ β.map L ⋯ ≫ L.map (β.s ≫ γ.s) = ψ.thd.map L ⋯ ≫ L.map (β.s ≫ γ.s)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_2.refine_1.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
Z : C
u : w₁.Y' ⟶ Z
hu : W u
fac₃ : z₁.f ≫ w₁.s ≫ u = t₁ ≫ w₁.f ≫ u
⊢ W (b.s ≫ z₁.s ≫ w₁.s ≫ u)

Tactic:
exact W.comp_mem _ _ b.hs (W.comp_mem _ _ z₁.hs (W.comp_mem _ _ w₁.hs hu))

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

Goal state before:
pp: case refine_2.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
q : W.LeftFraction w₁.Y' w₂.Y'
fac₃ : z₂.s ≫ w₂.s ≫ q.s = z₁.s ≫ w₁.s ≫ q.f
eq : a₁.s ≫ t₁ ≫ w₁.f ≫ q.f = a₁.s ≫ t₁ ≫ w₂.f ≫ q.s
Z : C
u : q.Y' ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f ≫ q.f ≫ u = t₁ ≫ w₂.f ≫ q.s ≫ u
⊢ W (b.s ≫ z₂.s ≫ w₂.s ≫ q.s ≫ u)

Tactic:
exact W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs
          (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ q.hs hu)))

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

Goal state before:
pp: case refine_2.refine_2
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₁ p₂

Tactic:
obtain ⟨q, fac₃⟩ := exists_leftFraction (RightFraction.mk (z₁.s ≫ w₁.s)
        (W.comp_mem _ _ z₁.hs w₁.hs) (z₂.s ≫ w₂.s))
      dsimp at fac₃
      simp only [assoc] at fac₃
      have eq : a₁.s ≫ t₁ ≫ w₁.f ≫ q.f = a₁.s ≫ t₁ ≫ w₂.f ≫ q.s := by
        rw [← reassoc_of% fac₁', ← fac₃, reassoc_of% hst, reassoc_of% fac₂']
      obtain ⟨Z, u, hu, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a₁.hs eq
      simp only [assoc] at fac₄
      refine ⟨Z, q.f ≫ u, q.s ≫ u, ?_, ?_, ?_⟩
      · simp only [p₁, p₂, assoc, reassoc_of% fac₃]
      · rw [assoc, assoc, assoc, assoc, fac₄, reassoc_of% hft]
      · simp only [p₁, assoc, ← reassoc_of% fac₃]
        exact W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs
          (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ q.hs hu)))

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

Goal state before:
pp: 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 ≤ P.limitsClosure J

Tactic:
exact P.strictLimitsClosureIter_le_limitsClosure J κ.ord

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
inst✝¹ : Preadditive C
inst✝ : ∀ (a : M), (shiftFunctor C a).Additive
a b c : M
α : ShiftedHom X Y a
β₁ β₂ : ShiftedHom Y Z b
h : b + a = c
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

Tactic:
by
  rw [comp, comp, comp, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
h : ∀ (i : ℤ), QuasiIsoAt φ (n + i)
j : ℤ
⊢ QuasiIsoAt φ j

Tactic:
obtain ⟨i, rfl⟩ : ∃ i, j = n + i := ⟨j - n, by lia⟩

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
h : ∀ (i : ℤ), QuasiIsoAt φ (n + i)
i : ℤ
⊢ QuasiIsoAt φ (n + i)
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ i, e.f i = i'
this : h.choose = i
⊢ e.r i' = some i

Tactic:
dsimp [r]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ i, e.f i = i'
this : h.choose = i
⊢ (if h : ∃ i, e.f i = i' then some h.choose else none) = some i
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h =
    DerivedCategory.HomologySequence.δ (DerivedCategory.Q.mapTriangle.obj T) n₀ n₁ h ≫
      (DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₁

Tactic:
by
  dsimp [DerivedCategory.HomologySequence.δ]
  rw [dsimp% [ShiftedHom.map]
      DerivedCategory.shiftMap_homologyFunctor_map_Q T.mor₃ n₀ n₁ (by lia)]
  simp [Functor.shiftMap, homologyFunctor_shift, homologyδOfTriangle]

Goal state after: