mathlib-initiative/mathlib-tactics huggingface dataset:
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 φ
i : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
⊢ f = (f ≫ (↑(fst φ)).v i j hij) ≫ (inl φ).v j i ⋯ + (f ≫ (snd φ).v i i ⋯) ≫ (inr φ).f i

Tactic:
apply ext_to φ i j hij

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
⊢ f ≫ (↑(fst φ)).v i j hij =
    ((f ≫ (↑(fst φ)).v i j hij) ≫ (inl φ).v j i ⋯ + (f ≫ (snd φ).v i i ⋯) ≫ (inr φ).f i) ≫ (↑(fst φ)).v i j hij

case h₂
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
⊢ f ≫ (snd φ).v i i ⋯ =
    ((f ≫ (↑(fst φ)).v i j hij) ≫ (inl φ).v j i ⋯ + (f ≫ (snd φ).v i i ⋯) ≫ (inr φ).f i) ≫ (snd φ).v i i ⋯
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case mpr
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
K : HomologicalComplex C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ (x.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = y.snd.hom i j) → x = y

Tactic:
obtain ⟨x₁, x₂⟩ := x
    obtain ⟨y₁, y₂⟩ := y
    rintro ⟨rfl, h⟩
    simp only [Sigma.mk.inj_iff, heq_eq_eq, true_and]
    ext i j
    by_cases hij : c.Rel j i
    · exact h _ _ hij
    · simp only [Homotopy.zero _ _ _ hij]

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

Goal state before:
pp: case neg
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 : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : ¬i + -1 = j
⊢ 0 = ho.hom i j

Tactic:
· rw [ho.zero i j (fun h' => h (by dsimp at h'; lia))]

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 L : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
⊢ (liftCochain φ α β h).comp (descCochain φ α' β' h') hp = α.comp α' ⋯ + β.comp β' ⋯

Tactic:
by
  simp [liftCochain, descCochain,
    Cochain.comp_assoc α (inl φ) _ _ (show -1 + n' = m' by lia) (by linarith)]

Goal state after:
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
m₁ m₂ m₃ : A
this :
  (Induced.add F s i (m₁ + m₂) m₃).hom ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
    eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom
⊢ ∀ (X : D),
    (Induced.add F s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom.app X ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj X)

Tactic:
intro X
          simpa using NatTrans.congr_app this X

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).inv.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
subst h
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_inv_app_f]

Goal state after:
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
this : (Induced.add F s i 0 n).hom = eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n)
⊢ ∀ (X : D), (Induced.add F s i 0 n).hom.app X = eqToHom ⋯ ≫ (s n).map ((Induced.zero F s i).inv.app X)

Tactic:
intro X
          simpa using NatTrans.congr_app this X

Goal state after:
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
this : (Induced.add F s i n 0).hom = eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv
⊢ ∀ (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:
intro X
          simpa using NatTrans.congr_app this X

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
A✝ : Type u_4
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a b : A
X : C
⊢ e.hom.app ((shiftFunctor C (a + b)).obj X) ≫
      H.map ((shiftFunctorAdd C a b).hom.app X) ≫
        (commShiftIso H b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor E b).map ((commShiftIso H a).hom.app X) ≫
            (shiftFunctor E b).map ((shiftFunctor E a).map (e.inv.app X)) ≫
              (shiftFunctor E b).map ((commShiftIso G a).inv.app (F.obj X)) ≫
                (commShiftIso G b).inv.app ((shiftFunctor D a).obj (F.obj X)) ≫
                  G.map ((shiftFunctorAdd D a b).inv.app (F.obj X)) =
    G.map (F.map ((shiftFunctorAdd C a b).hom.app X)) ≫
      e.hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        (commShiftIso H b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor E b).map (e.inv.app ((shiftFunctor C a).obj X)) ≫
            (commShiftIso G b).inv.app (F.obj ((shiftFunctor C a).obj X)) ≫
              G.map ((shiftFunctor D b).map ((OfComp.iso e a).hom.app X)) ≫
                G.map ((shiftFunctorAdd D a b).inv.app (F.obj X))

Tactic:
simp only [← NatTrans.naturality_assoc, ← commShiftIso_inv_naturality_assoc,
      ← Functor.map_comp_assoc]

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
A✝ : Type u_4
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a b : A
X : C
⊢ (F ⋙ G).map ((shiftFunctorAdd C a b).hom.app X) ≫
      e.hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        (commShiftIso H b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor E b).map
              ((commShiftIso H a).hom.app X ≫
                (shiftFunctor E a).map (e.inv.app X) ≫ (commShiftIso G a).inv.app (F.obj X)) ≫
            (commShiftIso G b).inv.app ((shiftFunctor D a).obj (F.obj X)) ≫
              G.map ((shiftFunctorAdd D a b).inv.app (F.obj X)) =
    G.map (F.map ((shiftFunctorAdd C a b).hom.app X)) ≫
      e.hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        (commShiftIso H b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor E b).map (e.inv.app ((shiftFunctor C a).obj X) ≫ G.map ((OfComp.iso e a).hom.app X)) ≫
            (commShiftIso G b).inv.app ((shiftFunctor D a).obj (F.obj X)) ≫
              G.map ((shiftFunctorAdd D a b).inv.app (F.obj X))
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ -(CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ) =
    (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).inv.app K ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
          (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ) ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app L

Tactic:
Functor.map_neg,

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ -(CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ) =
    (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).inv.app K ≫
      (-(HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ)) ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app L
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₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
comm₁₁ : (triangleh φ₁).mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
⊢ (quotient C (ComplexShape.up ℤ)).map (φ₁ ≫ b'') = (quotient C (ComplexShape.up ℤ)).map (a'' ≫ φ₂)

Tactic:
have comm₁₂ := e₂.hom.comm₁

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
comm₁₁ : (triangleh φ₁).mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁₂ : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ (triangleh φ₂).mor₁
⊢ (quotient C (ComplexShape.up ℤ)).map (φ₁ ≫ b'') = (quotient C (ComplexShape.up ℤ)).map (a'' ≫ φ₂)
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} A
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
inst✝² : HasShift D M
G : Type u_5
inst✝¹ : AddGroup G
inst✝ : HasShift C G
a : M
⊢ ((shiftFunctor C 0).associator (shiftFunctor C a) F).symm ≪≫ isoWhiskerRight (shiftFunctorAdd' C 0 a a ⋯).symm F =
    isoWhiskerRight (shiftFunctorZero C M) (shiftFunctor C a ⋙ F) ≪≫ (shiftFunctor C a ⋙ F).leftUnitor

Tactic:
rw [shiftFunctorAdd'_zero_add]
    cat_disch

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

Goal state before:
pp: case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
⊢ ∀ (X : V), (of V ⋙q (lift φ).toPrefunctor).obj X = φ.obj X

pp: case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of V ⋙q (lift φ).toPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
· rintro X
    rfl

Goal state after:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of V ⋙q (lift φ).toPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ ∀ (X : Paths V), Φ.obj X = (lift (of V ⋙q Φ.toPrefunctor)).obj X

pp: case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom ⋯ ≫ (lift (of V ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
· rintro X
    rfl

Goal state after:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom ⋯ ≫ (lift (of V ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this✝ : G.Full
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
⊢ P f

Tactic:
by
      rcases X with ⟨⟨X⟩⟩
      rcases Y with ⟨⟨Y⟩⟩
      simpa only [Functor.map_preimage] using! this _ _ (G.preimage f)

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

Goal state before:
pp: case mp
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
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : W.Q.map f = W.Q.map g
e : W.Q ⋙ (Localization.uniq W.Q L W).functor ≅ L := Localization.compUniqFunctor W.Q L W
⊢ L.map f = L.map g

Tactic:
rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]

Goal state after:
case mp
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
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : W.Q.map f = W.Q.map g
e : W.Q ⋙ (Localization.uniq W.Q L W).functor ≅ L := Localization.compUniqFunctor W.Q L W
⊢ e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map f ≫ e.hom.app Y =
    e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map g ≫ e.hom.app Y
Module: Mathlib.CategoryTheory.Localization.Predicate

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
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : L.map f = L.map g
e : L ⋙ (Localization.uniq L W.Q W).functor ≅ W.Q := Localization.compUniqFunctor L W.Q W
⊢ W.Q.map f = W.Q.map g

Tactic:
rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e 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
L : C ⥤ D
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : L.map f = L.map g
e : L ⋙ (Localization.uniq L W.Q W).functor ≅ W.Q := Localization.compUniqFunctor L W.Q W
⊢ e.inv.app X ≫ (L ⋙ (Localization.uniq L W.Q W).functor).map f ≫ e.hom.app Y =
    e.inv.app X ≫ (L ⋙ (Localization.uniq L W.Q W).functor).map g ≫ e.hom.app Y
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: 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₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : Φ.IsLocalizedFullyFaithful
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
L₁ : C₁ ⥤ D₁
F : D₁ ⥤ D₂
iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : L₁.EssSurj
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
⊢ IsIso (F.map (L₁.map f))

Tactic:
exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (Arrow.isoOfNatIso iso f)).1 (Localization.inverts L₂ W₂ _ (Φ.map _ hf))

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
⊢ G.Additive

Tactic:
suffices ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g by
      refine ⟨fun {X Y f g} => ?_⟩
      have hL := essSurj L W
      have eq := this ((L.objObjPreimageIso X).hom ≫ f ≫ (L.objObjPreimageIso Y).inv)
        ((L.objObjPreimageIso X).hom ≫ g ≫ (L.objObjPreimageIso Y).inv)
      rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp,
        ← comp_add, ← comp_add, ← add_comp, ← add_comp, Functor.map_comp, Functor.map_comp] at eq
      rw [← cancel_mono (G.map (L.objObjPreimageIso Y).inv),
        ← cancel_epi (G.map (L.objObjPreimageIso X).hom), eq]

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⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case succ
C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁴ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝³ : LinearOrder β
inst✝² : OrderBot β
inst✝¹ : SuccOrder β
inst✝ : WellFoundedLT β
b : β
hb : ¬IsMax b
hb' : P.strictLimitsClosureIter J b ≤ P.limitsClosure J
⊢ transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) b P ⊔
      ⨆ a, (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) b P).strictLimitsOfShape (J a) ≤
    P.limitsClosure J

Tactic:
sup_le_iff,

Goal state after:
case succ
C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁴ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝³ : LinearOrder β
inst✝² : OrderBot β
inst✝¹ : SuccOrder β
inst✝ : WellFoundedLT β
b : β
hb : ¬IsMax b
hb' : P.strictLimitsClosureIter J b ≤ P.limitsClosure J
⊢ transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) b P ≤ P.limitsClosure J ∧
    ⨆ a, (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) b P).strictLimitsOfShape (J a) ≤ P.limitsClosure J
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)
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.colimitsClosure J)

Tactic:
by
  rw [colimitsClosure_eq_unop_limitsClosure]
  have (a : α) : Small.{w} (J a)ᵒᵖ := Opposite.small
  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
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
⊢ α ≫ (shiftFunctor C a).map (-β) ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    -α ≫ (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
Functor.map_neg,

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
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
⊢ α ≫ (-(shiftFunctor C a).map β) ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    -α ≫ (shiftFunctor C a).map β ≫ (shiftFunctorAdd' C b a c h).inv.app Z
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
P Q : ObjectProperty C
inst✝ : Q.ContainsZero
⊢ P ≤ P.extensionProduct Q

Tactic:
by
  intro X hX
  rw [← extensionProduct_isoClosure_right]
  obtain ⟨Z, hZ, hQ⟩ := Q.exists_prop_of_containsZero
  refine ⟨_, _, _, _, _, contractible_distinguished X, hX, ?_⟩
  exact ⟨Z, hQ, ⟨IsZero.iso (isZero_zero C) hZ⟩⟩

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} E
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
h₁ : StrictUniversalPropertyFixedTarget L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget L₂ W₂ E
W₃ : MorphismProperty C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
F : C₁ ⥤ E
hF : W₃.IsInvertedBy F
⊢ (L₁ ⋙ L₂) ⋙ h₂.lift (h₁.lift F ⋯) ⋯ = F

Tactic:
rw [Functor.assoc, h₂.fac, h₁.fac]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
inst✝ : QuasiIso φ
⊢ QuasiIso ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ)

Tactic:
rw [quasiIso_shift_iff]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
inst✝ : QuasiIso φ
⊢ QuasiIso φ
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n : ℤ
⊢ (quasiIso C (up ℤ)).inverseImage (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n) = quasiIso C (up ℤ)

Tactic:
by ext; apply quasiIso_shift_iff

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0

Tactic:
simp only [next] at hj hj'
        obtain rfl : i' = i + n := by lia
        obtain rfl : j' = j + n := by lia
        dsimp at hf ⊢
        simp only [Linear.comp_units_smul] at hf
        apply (one_smul (M := ℤˣ) _).symm.trans _
        rw [← Int.units_mul_self n.negOnePow, mul_smul, comp_id, hf, smul_zero]

Goal state after: