mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
⊢ ⨅ i, I ^ i • ⊤ = ⊥

Tactic:
rw [eq_bot_iff]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
⊢ ⨅ i, I ^ i • ⊤ ≤ ⊥
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsNoetherianRing R
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
⊢ ⨅ i, I ^ i • ⊤ = ⊥

Tactic:
rw [eq_bot_iff]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsNoetherianRing R
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
⊢ ⨅ i, I ^ i • ⊤ ≤ ⊥
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ : M
X : C
inst✝ : F.Monoidal
⊢ (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (δ F (m₁ ⊗ 𝟙_ M) m₂).app X =
    (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (F.map (λ_ m₂).hom).app ((F.obj m₁).obj X) ≫ (F.obj m₂).map ((F.map (ρ_ m₁).inv).app X)

Tactic:
← obj_η_app_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ : M
X : C
inst✝ : F.Monoidal
⊢ (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (δ F (m₁ ⊗ 𝟙_ M) m₂).app X =
    (F.obj m₂).map ((η F).app ((F.obj m₁).obj X)) ≫ (F.obj m₂).map ((F.map (ρ_ m₁).inv).app X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
⊢ ∀ {X Y : Discrete A} (X' : Discrete A) (f : X ⟶ Y),
    MonoidalCategoryStruct.whiskerLeft ((Discrete.functor h.F).obj X') ((Discrete.functor h.F).map f) ≫
        (h.add X'.as Y.as).symm.hom =
      (h.add X'.as X.as).symm.hom ≫ (Discrete.functor h.F).map (MonoidalCategoryStruct.whiskerLeft X' f)

Tactic:
by
        rintro ⟨X⟩ ⟨Y⟩ ⟨X'⟩ ⟨⟨⟨rfl⟩⟩⟩
        ext
        simp

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorCompIsoId C n m h).hom.app X) =
    (shiftFunctorCompIsoId C m n ⋯).hom.app ((shiftFunctor C n).obj X)

Tactic:
dsimp [shiftFunctorCompIsoId]
  simpa only [Functor.map_comp, ← shiftFunctorAdd'_zero_add_inv_app n X,
    ← shiftFunctorAdd'_add_zero_inv_app n X]
    using shiftFunctorAdd'_assoc_inv_app n m n 0 0 n h
      (by rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]) (by rw [h, zero_add]) X

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
x y z : S
⊢ z • single x 1 + z • single y 1 - z • single (x + y) 1 ∈ kerTotal R S

Tactic:
← smul_add,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ z • (single x 1 + single y 1) - z • single (x + y) 1 ∈ kerTotal R S
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
x y z : S
⊢ z • single y x + z • single x y - z • single (x * y) 1 ∈ kerTotal R S

Tactic:
← smul_add,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ z • (single y x + single x y) - z • single (x * y) 1 ∈ kerTotal R S
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
hK : K.ExactAt i
L : HomologicalComplex C c
e : K ≅ L
⊢ L.ExactAt i

Tactic:
by
  rw [exactAt_iff] at hK ⊢
  exact ShortComplex.exact_of_iso ((shortComplexFunctor C c i).mapIso e) hK

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.fst.f i ≫ biprod.inl.f i + biprod.snd.f i ≫ biprod.inr.f i = 𝟙 ((K ⊞ L).X i)

Tactic:
simp [← comp_f, ← add_f_apply]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ g.f i = (dNext i) (-h.hom) + (prevD i) (-h.hom) + f.f i

Tactic:
by
    rw [map_neg, map_neg, h.comm, ← neg_add, ← add_assoc, neg_add_cancel, zero_add]

Goal state after:
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 : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q = q'
⊢ p + n = q'

Tactic:
rw [← hq', hpq]

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

Goal state before:
pp: case h₀
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
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ (f ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.fst = (g ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.fst

pp: case h₁
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
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ (f ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.snd = (g ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.snd

Tactic:
· simpa using! h₁

Goal state after:
case h₁
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
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ (f ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.snd = (g ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.snd
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
⊢ (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ z₃.v (p + n₁ + n₂) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫ (z₂.comp z₃ ⋯).v (p + n₁) q ⋯

Tactic:
comp_v z₂ z₃ rfl (p + n₁) (p + n₁ + n₂) q (by lia) (by lia),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
⊢ (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ z₃.v (p + n₁ + n₂) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯ ≫ z₃.v (p + n₁ + n₂) q ⋯
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Tactic:
simp only [nullHomotopicMap']
  rw [nullHomotopicMap_f r₂₁ r₁₀]
  split_ifs
  rfl

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

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : n + 1 = m
⊢ δ n m (z.map Φ) = (δ n m z).map Φ

Tactic:
ext p q hpq
    dsimp
    simp only [δ_v n m hnm _ p q hpq (q - 1) (p + 1) rfl rfl,
      Functor.map_add, Functor.map_comp, Functor.map_units_smul,
      Cochain.map_v, Functor.mapHomologicalComplex_obj_d]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Category.{v_1, u_2} C
inst✝² : Preadditive C
inst✝¹ : Linear R C
r : HomRel C
inst✝ : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
X Y : Quotient r
a : R
f₁ f₂ : X.as ⟶ Y.as
h₁₂ : HomRel.CompClosure r f₁ f₂
⊢ Quot.mk (HomRel.CompClosure r) (a • f₁) = Quot.mk (HomRel.CompClosure r) (a • f₂)

Tactic:
simp only [HomRel.compClosure_eq_self] at h₁₂

Goal state after:
R : Type u_1
C : Type u_2
inst✝⁴ : Semiring R
inst✝³ : Category.{v_1, u_2} C
inst✝² : Preadditive C
inst✝¹ : Linear R C
r : HomRel C
inst✝ : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
X Y : Quotient r
a : R
f₁ f₂ : X.as ⟶ Y.as
h₁₂ : r f₁ f₂
⊢ Quot.mk (HomRel.CompClosure r) (a • f₁) = Quot.mk (HomRel.CompClosure r) (a • f₂)
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
⊢ (homotopyEquivalences V c).IsInvertedBy (quotient V c)

Tactic:
by
  rintro K L _ ⟨e, rfl⟩
  change IsIso (isoOfHomotopyEquiv e).hom
  infer_instance

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
n : ℤ
⊢ ∀ (X : CochainComplex C ℤ),
    { f := fun x ↦ (𝟙 X).f (x + n), comm' := ⋯ } =
      𝟙 { X := fun i ↦ X.X (i + n), d := fun x x_1 ↦ n.negOnePow • X.d (x + n) (x_1 + n), shape := ⋯, d_comp_d' := ⋯ }

Tactic:
intros; rfl

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
n : ℤ
⊢ ∀ {X Y Z : CochainComplex C ℤ} (f : X ⟶ Y) (g : Y ⟶ Z),
    { f := fun x ↦ (f ≫ g).f (x + n), comm' := ⋯ } =
      { f := fun x ↦ f.f (x + n), comm' := ⋯ } ≫ { f := fun x ↦ g.f (x + n), comm' := ⋯ }

Tactic:
intros; rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
x✝ : CochainComplex C ℤ
i✝ : ℤ
⊢ ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app x✝).f i✝ = ((shiftFunctorZero' C 0 ⋯).hom.app x✝).f i✝

Tactic:
shiftFunctorZero_hom_app_f,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
x✝ : CochainComplex C ℤ
i✝ : ℤ
⊢ (XIsoOfEq x✝ ⋯).hom = ((shiftFunctorZero' C 0 ⋯).hom.app x✝).f i✝
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 a : ℤ
⊢ shift 0 a = 0

Tactic:
by
  change shiftAddHom K L n a 0 = 0
  apply map_zero

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 : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
⊢ commShiftIso F 0 = CommShift.isoZero' F A 0 ⋯

Tactic:
CommShift.isoZero'_eq_isoZero,

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 : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
⊢ commShiftIso F 0 = CommShift.isoZero F A
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
a b : A
X : C
⊢ (shiftFunctorAdd D a b).hom.app (F.obj X) =
    (i (a + b)).hom.app X ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X)

Tactic:
simp only [ShiftMkCore.shiftFunctorAdd_eq, HasShift.Induced.add_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
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = (a * m).negOnePow • ((γ.leftShift a n' hn').comp γ' ⋯).v p q hpq

Tactic:
simp only [Cochain.comp_v _ _ h' p (p + n') q rfl (by lia),
    γ.leftShift_v a n' hn' p (p + n') rfl (p + a) (by lia),
    (γ.comp γ' h).leftShift_v a t' (by lia) p q hpq (p + a) (by lia),
    smul_smul, Linear.units_smul_comp, assoc, Int.negOnePow_add, ← mul_assoc, ← h',
    comp_v _ _ h (p + a) (p + n') q (by lia) (by lia)]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ ((a * (n' + m)).negOnePow * (a * (a - 1) / 2).negOnePow) •
      (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (p + n') ⋯ ≫ γ'.v (p + n') q ⋯ =
    ((a * m).negOnePow * (a * n').negOnePow * (a * (a - 1) / 2).negOnePow) •
      (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (p + n') ⋯ ≫ γ'.v (p + n') q ⋯
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
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ T₁.invRotate.mor₁ ≫ a = (shiftFunctor C (-1)).map c ≫ T₂.invRotate.mor₁

Tactic:
by
    dsimp
    simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm,
      Functor.map_comp, shift_shift_neg', Functor.id_obj, assoc, Iso.inv_hom_id_app, comp_id]

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

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : IsZero T.obj₂
⊢ T.mor₁ = 0 ∧ T.mor₂ = 0

Tactic:
exact ⟨h.eq_of_tgt _ _, h.eq_of_src _ _⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
⊢ Octahedron' comm h₁₂ h₂₃ h₁₃

Tactic:
let m₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ o.m₃⟦-1⟧' ≫ (shiftShiftNeg Z₂₃ 1).hom

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
⊢ Octahedron' comm h₁₂ h₂₃ h₁₃
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) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)

Tactic:
rw [hInv_iso_hom_app]

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₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map ((iso T.symm.functor R L B.symm.functor).inv.app (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.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.Equivalence

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} D
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst✝ : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q)
⊢ L₂.IsLocalization W₂

Tactic:
exact
    { inverts := hW₂
      isEquivalence :=
        Localization.isEquivalence W₂.Q W₂ L₁ W₁ L₂ (Construction.lift L₂ hW₂)
          (E.functor ⋙ W₂.Q) (Localization.lift (E.functor ⋙ W₂.Q) h L₁) (by
            calc
              L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ _ := (leftUnitor _).symm
              _ ≅ _ := isoWhiskerRight E.counitIso.symm _
              _ ≅ E.inverse ⋙ E.functor ⋙ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                    Functor.associator _ _ _
              _ ≅ E.inverse ⋙ L₁ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                    isoWhiskerLeft E.inverse ((Functor.associator _ _ _).symm ≪≫
                      isoWhiskerRight iso _)
              _ ≅ E.inverse ⋙ E.functor ⋙ W₂.Q :=
                    isoWhiskerLeft _ (Localization.fac (E.functor ⋙ W₂.Q) h L₁)
              _ ≅ (E.inverse ⋙ E.functor) ⋙ W₂.Q := (Functor.associator _ _ _).symm
              _ ≅ 𝟭 C₂ ⋙ W₂.Q := isoWhiskerRight E.counitIso _
              _ ≅ W₂.Q := leftUnitor _)
          (Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Lifting.iso W₂.Q W₂ _ _) ≪≫ iso) }

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

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
X'' Y'' : C
eX' : L.obj X'' ≅ X'
eY' : L.obj Y'' ≅ Y'
f₁ f₂ : X' ⟶ Y'
⊢ add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂

Tactic:
have h₁ := comp_add W eX' eX eY (𝟙 _) f₁ f₂
  have h₂ := add_comp W eX' eY eY' f₁ f₂ (𝟙 _)
  simp only [id_comp] at h₁
  simp only [comp_id] at h₂
  rw [h₁, h₂]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁸ : Category.{v₁, u₁} C
inst✝¹⁷ : Category.{v₂, u₂} D
E : Type u₃
inst✝¹⁶ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝¹⁵ : L.IsLocalization W
A : Type w
inst✝¹⁴ : AddMonoid A
inst✝¹³ : HasShift C A
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
⊢ G.CommShift M

Tactic:
letI : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := ⟨e.symm⟩
  exact Functor.commShiftOfLocalization L₁ W₁ M (Φ.functor ⋙ L₂) G

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v + 1, u} (Cardinal.mk X) < Cardinal.lift.{max u (v + 1), v} κ
⊢ Small.{v, u} X

Tactic:
simpa only [Cardinal.small_iff_lift_mk_lt_univ] using h.trans (Cardinal.lift_lt_univ' κ)

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

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
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
⊢ G.Additive ↔ (L ⋙ G).Additive

Tactic:
by
  constructor
  · intro
    infer_instance
  · intro h
    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]
    intro X Y f g
    obtain ⟨φ, rfl, rfl⟩ := exists_leftFraction₂ L W f g
    rw [← φ.map_add L (inverts L W), ← cancel_mono (G.map (L.map φ.s)), ← G.map_comp,
      add_comp, ← G.map_comp, ← G.map_comp, LeftFraction.map_comp_map_s,
      LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, ← Functor.comp_map,
      Functor.map_add, Functor.comp_map, Functor.comp_map]

Goal state after: