mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C₁ : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁸ : HasSmallLocalizedHom W₁ X Y
inst✝⁷ : HasSmallLocalizedHom W₁ Y Z
inst✝⁶ : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst✝⁵ : HasSmallLocalizedHom W₂ X' X'
inst✝⁴ : HasSmallLocalizedHom W₂ Y' Y'
inst✝³ : HasSmallLocalizedHom W₂ Z' Z'
inst✝² : HasSmallLocalizedHom W₂ X' Y'
inst✝¹ : HasSmallLocalizedHom W₂ Y' Z'
inst✝ : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
eZ : Φ.functor.obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
⊢ Φ.smallHomMap' eX eZ (f.comp g) = (Φ.smallHomMap' eX eY f).comp (Φ.smallHomMap' eY eZ g)

Tactic:
by
  have := hasSmallLocalizedHom_of_isos.{w'} W₂ eX.symm eY.symm
  have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm (Iso.refl Y')
  have := hasSmallLocalizedHom_of_isos.{w'} W₂ eX.symm (Iso.refl Z')
  have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm eZ.symm
  have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm (Iso.refl Z')
  have := hasSmallLocalizedHom_of_isos.{w'} W₂ (Iso.refl Y') eY.symm
  have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm eY.symm
  simp only [smallHomMap', smallHomMap_comp, SmallHom.comp_assoc]
  congr 2
  rw [← SmallHom.comp_assoc, SmallHom.mk_comp_mk, eY.hom_inv_id, SmallHom.mk_id_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
⊢ (Functor.commShiftIso Q a).hom.app ((CochainComplex.singleFunctor C 0).obj X) ≫
      x ≫ (Functor.commShiftIso Q b).inv.app ((CochainComplex.singleFunctor C 0).obj Y) =
    (Functor.commShiftIso Q a).hom.app ((CochainComplex.singleFunctor C 0).obj X) ≫
      y ≫ (Functor.commShiftIso Q b).inv.app ((CochainComplex.singleFunctor C 0).obj Y)

Tactic:
have : (((CochainComplex.singleFunctor C 0).obj X)⟦a⟧).IsStrictlyLE (-a) :=
        CochainComplex.isStrictlyLE_shift _ 0 _ _ (by lia)

Goal state after:
case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
this : ((shiftFunctor (CochainComplex C ℤ) a).obj ((CochainComplex.singleFunctor C 0).obj X)).IsStrictlyLE (-a)
⊢ (Functor.commShiftIso Q a).hom.app ((CochainComplex.singleFunctor C 0).obj X) ≫
      x ≫ (Functor.commShiftIso Q b).inv.app ((CochainComplex.singleFunctor C 0).obj Y) =
    (Functor.commShiftIso Q a).hom.app ((CochainComplex.singleFunctor C 0).obj X) ≫
      y ≫ (Functor.commShiftIso Q b).inv.app ((CochainComplex.singleFunctor C 0).obj Y)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : (singleFunctor C 0).FullyFaithful
e : (X ⟶ Y) ≃ Ext X Y 0 := (h.homEquiv.trans (ShiftedHom.homEquiv ↑0 ⋯)).trans homEquiv.symm
f : X ⟶ Y
⊢ homEquiv.symm ((ShiftedHom.homEquiv 0 ⋯) (h.homEquiv f)) = mk₀ f

Tactic:
apply homEquiv.injective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
this : HasDerivedCategory C := ⋯
h : (singleFunctor C 0).FullyFaithful
e : (X ⟶ Y) ≃ Ext X Y 0 := ⋯
f : X ⟶ Y
⊢ homEquiv (homEquiv.symm ((ShiftedHom.homEquiv 0 ⋯) (h.homEquiv f))) = homEquiv (mk₀ f)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂✝ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃✝ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w✝¹ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
⊢ (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ = 0

Tactic:
rw [sub_comp, assoc, assoc, assoc, ← NatTrans.naturality, ← reassoc_of% h₃, h₁, sub_self]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂✝ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃✝ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w✝³ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝² : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ = 0
A₃ : C
π₃ : A₃ ⟶ A₂
w✝¹ : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)
A₄ : C
π₄ : A₄ ⟶ A₃
w✝ : Epi π₄
f₀ : A₄ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
⊢ π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ = π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1 + (π₄ ≫ π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₄ ≫ π₃ ≫ f₁ ≫ φ.app 1)

Tactic:
rw [add_sub_cancel]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X ≫
      (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).hom.app X) ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫
          ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X

Tactic:
shiftFunctorAdd'_op_hom_app X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    ((shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
        ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
          (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
            (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).inv.app X)) ≫
      (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).hom.app X) ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫
          ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ ((opShiftFunctorEquivalence C 0).unitIso.hom.app X).unop =
    (((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫
        ((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop).op).unop

Tactic:
dsimp [opShiftFunctorEquivalence]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).inv.app X).unop ≫
      (shiftFunctorCompIsoId C 0 0 ⋯).hom.app (Opposite.unop X) =
    (shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop ≫ (shiftFunctorZero C ℤ).hom.app (Opposite.unop X)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ ((opShiftFunctorEquivalence C 0).unitIso.inv.app X).unop =
    (((shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop).op ≫
        ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op).unop

Tactic:
dsimp [opShiftFunctorEquivalence]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctorCompIsoId C 0 0 ⋯).inv.app (Opposite.unop X) ≫
      (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).hom.app X).unop =
    (shiftFunctorZero C ℤ).inv.app (Opposite.unop X) ≫ (shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ (opShiftFunctorEquivalence C p).unitIso.hom.app X =
    (opShiftFunctorEquivalence C n).unitIso.hom.app X ≫
      ((shiftFunctor C n).map ((opShiftFunctorEquivalence C m).unitIso.hom.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((opShiftFunctorEquivalence C m).functor.obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op

Tactic:
dsimp [opShiftFunctorEquivalence]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C p).map ((shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op =
    (((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
        ((shiftFunctor C n).map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop).op) ≫
      ((shiftFunctor C n).map
            ((shiftFunctor C m).map ((shiftFunctorOpIso C m (-m) ⋯).inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop ≫
              (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n : ℤ
hmn : -n + n = 0
⊢ (shiftFunctor Cᵒᵖ (-n)).map ((opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op X)) =
    (opShiftFunctorEquivalence C n).counitIso.inv.app ((shiftFunctor Cᵒᵖ (-n)).obj (Opposite.op X)) ≫
      (shiftFunctor Cᵒᵖ n).map
          ((shiftFunctor C n).map ((shiftFunctorOpIso C (-n) n hmn).hom.app (Opposite.op X)).unop).op ≫
        (shiftFunctor Cᵒᵖ n).map ((shiftFunctorOpIso C (-n) n hmn).inv.app (Opposite.op ((shiftFunctor C n).obj X))) ≫
          (shiftFunctorComm Cᵒᵖ n (-n)).inv.app (Opposite.op ((shiftFunctor C n).obj X))

Tactic:
dsimp [opShiftFunctorEquivalence]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n : ℤ
hmn : -n + n = 0
⊢ (shiftFunctor Cᵒᵖ (-n)).map
      (((shiftFunctorCompIsoId C n (-n) ⋯).hom.app X).op ≫
        (shiftFunctorOpIso C n (-n) ⋯).inv.app (Opposite.op ((shiftFunctor C n).obj X))) =
    (((shiftFunctorCompIsoId C n (-n) ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ (-n)).obj (Opposite.op X)))).op ≫
        (shiftFunctorOpIso C n (-n) ⋯).inv.app
          (Opposite.op ((shiftFunctor C n).obj (Opposite.unop ((shiftFunctor Cᵒᵖ (-n)).obj (Opposite.op X)))))) ≫
      (shiftFunctor Cᵒᵖ n).map
          ((shiftFunctor C n).map ((shiftFunctorOpIso C (-n) n hmn).hom.app (Opposite.op X)).unop).op ≫
        (shiftFunctor Cᵒᵖ n).map ((shiftFunctorOpIso C (-n) n hmn).inv.app (Opposite.op ((shiftFunctor C n).obj X))) ≫
          (shiftFunctorComm Cᵒᵖ n (-n)).inv.app (Opposite.op ((shiftFunctor C n).obj X))
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝² x✝¹ : A
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' (PullbackShift C φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor (PullbackShift C φ) (φ x✝²)).obj x✝) ≫
          (shiftFunctor (PullbackShift D φ) (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
            (shiftFunctorAdd' (PullbackShift D φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) ≫
              (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) =
    F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' C (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (((𝟙 (F.obj ((shiftFunctor C (φ x✝¹)).obj ((shiftFunctor C (φ x✝²)).obj x✝))) ≫
                (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor C (φ x✝²)).obj x✝)) ≫
              (shiftFunctor D (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝)) ≫
            (shiftFunctorAdd' D (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)) ≫
          (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)

Tactic:
rw [id_comp, assoc, assoc]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝² x✝¹ : A
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' (PullbackShift C φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor (PullbackShift C φ) (φ x✝²)).obj x✝) ≫
          (shiftFunctor (PullbackShift D φ) (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
            (shiftFunctorAdd' (PullbackShift D φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) ≫
              (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) =
    F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' C (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor C (φ x✝²)).obj x✝) ≫
          (shiftFunctor D (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
            (shiftFunctorAdd' D (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) ≫
              (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C

Tactic:
obtain ⟨Z, g, h, H⟩ := Pretriangulated.distinguished_cocone_triangle₁ f.unop
  refine ⟨_, g.op, (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
    (shiftFunctor Cᵒᵖ (1 : ℤ)).map h.op, ?_⟩
  simp only [mem_distinguishedTriangles_iff]
  refine Pretriangulated.isomorphic_distinguished _ H _ ?_
  exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp)
    (Quiver.Hom.op_inj (by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]))

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
P Y : C
n : ℕ
inst✝ : Projective P
e : Ext P Y (n + 1)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ e = 0

Tactic:
apply homEquiv.injective

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
P Y : C
n : ℕ
inst✝ : Projective P
e : Ext P Y (n + 1)
this : HasDerivedCategory C := ⋯
⊢ homEquiv e = homEquiv 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X I : C
n : ℕ
inst✝ : Injective I
e : Ext X I (n + 1)
K : CochainComplex C ℤ := (CochainComplex.singleFunctor C 0).obj X
this✝ : K.IsStrictlyGE (-↑n)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ e = 0

Tactic:
apply homEquiv.injective

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X I : C
n : ℕ
inst✝ : Injective I
e : Ext X I (n + 1)
K : CochainComplex C ℤ := ⋯
this✝ : K.IsStrictlyGE (-↑n)
this : HasDerivedCategory C := ⋯
⊢ homEquiv e = homEquiv 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: K : Type u_7
K₁ : Type u_8
V₁ : Type u_10
V₂ : Type u_11
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : (B x) x ≠ 0
⊢ K₁ ∙ x ⊓ Submodule.orthogonalBilin B (K₁ ∙ x) = ⊥

Tactic:
by
  rw [← Finset.coe_singleton]
  refine eq_bot_iff.2 fun y h ↦ ?_
  obtain ⟨μ, -, rfl⟩ := Submodule.mem_span_finset.1 h.1
  replace h := h.2 x (by simp [Submodule.mem_span] : x ∈ Submodule.span K₁ ({x} : Finset V₁))
  rw [Finset.sum_singleton] at h ⊢
  suffices hμzero : μ x = 0 by rw [hμzero, zero_smul, Submodule.mem_bot]
  rw [map_smulₛₗ] at h
  exact Or.elim (smul_eq_zero.mp h)
      (fun y ↦ by simpa using y)
      (fun hfalse ↦ False.elim <| hx hfalse)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: case intro
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
e : Basis ι R M
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
val✝ : Fintype ι
⊢ ∑ j, e.toMatrix (⇑v) j i • e j = v i

Tactic:
e.sum_toMatrix_smul_self

Goal state after:
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
e : Basis ι R M
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
val✝ : Fintype ι
⊢ v i = v i
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ∈ rootsOfUnity k M ↔ ↑ζ ^ k = 1

Tactic:
by
  rw [mem_rootsOfUnity]; norm_cast

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ (↑A).adjugate.det = 1

Tactic:
rw [det_adjugate, A.prop, one_pow]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha)⁻¹ = diag2 a⁻¹ ⋯

Tactic:
apply inv_eq_of_mul_eq_one_right

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ diag2 a ha * diag2 a⁻¹ ⋯ = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c b c' : F
hc : c' = b * (a ^ 2 - 1)
i j : Fin 2
⊢ ↑(diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b)) i j =
    ↑(SpecialLinearGroup.transvection ⋯ c') i j

Tactic:
fin_cases i <;> fin_cases j <;>
    simp [hc, SpecialLinearGroup.transvection_coe, diag2_coe, inv_inv, mul_add, add_mul,
      mul_inv_cancel₀ ha, inv_mul_cancel₀ ha, mul_comm a b, mul_assoc b a a, ← pow_two,
      mul_sub_one, ← sub_eq_add_neg]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
j : Fin 2
c : F
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ SpecialLinearGroup.transvection h c ∈ commutator SL(2, F)

Tactic:
· obtain rfl : j = 0 := by fin_cases j <;> tauto
    exact transvection_mem_commutator₁ ha hasq c

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ 1 * x = x

Tactic:
by
  suffices mulHom A One.one = AddMonoidHom.id (⨁ i, A i) from DFunLike.congr_fun this x
  apply addHom_ext; intro i xi
  simp only [One.one]
  rw [mulHom_of_of]
  exact of_eq_of_gradedMonoid_eq (one_mul <| GradedMonoid.mk i xi)

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
n : ℕ
fι : Fin n → ι
fA : (a : Fin n) → A (fι a)
⊢ (List.map (fun a ↦ (of A (fι a)) (fA a)) (List.finRange n)).prod =
    (of A ((List.finRange n).dProdIndex fι)) ((List.finRange n).dProd fι fA)

Tactic:
ofList_dProd

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
n : ℕ
fι : Fin n → ι
fA : (a : Fin n) → A (fι a)
⊢ (List.map (fun a ↦ (of A (fι a)) (fA a)) (List.finRange n)).prod =
    (List.map (fun a ↦ (of A (fι a)) (fA a)) (List.finRange n)).prod