mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
Y Z Z' : C
f₁ f₂ : Y ⟶ Z
s : Z ⟶ Z'
hs : P.trW s
hf₁ : f₁ ≫ s = f₂ ≫ s
⊢ ∃ X' t, ∃ (_ : P.trW t), t ≫ f₁ = t ≫ f₂

Tactic:
by
    rw [P.trW_iff'] at hs
    obtain ⟨Z, g, h, H, mem⟩ := hs
    have hf₂ : (f₁ - f₂) ≫ s = 0 := by rw [sub_comp, hf₁, sub_self]
    obtain ⟨q, hq⟩ := Triangle.coyoneda_exact₂ _ H _ hf₂
    obtain ⟨Y', r, t, mem'⟩ := distinguished_cocone_triangle₁ q
    refine ⟨Y', r, ?_, ?_⟩
    · exact ⟨_, _, _, mem', mem⟩
    · have eq := comp_distTriang_mor_zero₁₂ _ mem'
      dsimp at eq
      rw [← sub_eq_zero, ← comp_sub, hq, reassoc_of% eq, zero_comp]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ embeddingUpNat.IsRelIff

Tactic:
by dsimp [embeddingUpNat]; infer_instance

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
this : (K.extendOpIso e).inv.f i' ≫ (K.op.extend e.op).d i' j' = ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'
⊢ (K.op.extend e.op).d i' j' = (K.extendOpIso e).hom.f i' ≫ (K.extendOpIso e).inv.f i' ≫ (K.op.extend e.op).d i' j'

Tactic:
← comp_f_assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
this : (K.extendOpIso e).inv.f i' ≫ (K.op.extend e.op).d i' j' = ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'
⊢ (K.op.extend e.op).d i' j' = ((K.extendOpIso e).hom ≫ (K.extendOpIso e).inv).f i' ≫ (K.op.extend e.op).d i' j'
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Injective (K.X i)
i' : ι'
i : ι
hi : e.f i = i'
⊢ Injective ((K.extend e).X i')

Tactic:
exact Injective.of_iso (K.extendXIso e hi).symm inferInstance

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : (e.extendFunctor C).obj K ⟶ (e.extendFunctor C).obj L
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ ((e.extendFunctor C).map { f := fun i ↦ (K.extendXIso e ⋯).inv ≫ φ.f (e.f i) ≫ (L.extendXIso e ⋯).hom, comm' := ⋯ }).f
      i' =
    φ.f i'

Tactic:
· exact (K.isZero_extend_X _ _ (by tauto)).eq_of_src _ _

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
⊢ ((K.extend e).sc' i' j' k').f ≫ (K.extendXIso e hj').hom ≫ h.p = 0

Tactic:
by
    dsimp
    rw [← d_comp_eq_zero_iff K e hj' hi hi']
    exact h.wp

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
hi : ¬∃ i, e.f i = c'.prev j'
⊢ Epi φ.τ₁

Tactic:
apply IsZero.epi (isZero_extend_X _ _ _ (by simpa using hi))

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
⊢ Mono (homologyMap φ.τ₃ i)

Tactic:
by_cases hi : ∃ j, c.Rel i j

Goal state after:
case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
hi : ∃ j, c.Rel i j
⊢ Mono (homologyMap φ.τ₃ i)

case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
hi : ¬∃ j, c.Rel i j
⊢ Mono (homologyMap φ.τ₃ i)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
by_cases hi : ∃ j, c.Rel i j

Goal state after:
case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ∃ j, c.Rel i j
⊢ Epi (homologyMap φ.τ₃ i)

case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
⊢ Epi (homologyMap φ.τ₃ i)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : IsZero (S.X₁.homology i)
h₃ : IsZero (S.X₃.homology i)
⊢ IsZero (S.X₂.homology i)

Tactic:
exact (hS.homology_exact₂ i).isZero_X₂ (h₁.eq_of_src _ _) (h₃.eq_of_tgt _ _)

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
⊢ triangleOfSES hS ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)

Tactic:
by
  have := CochainComplex.mappingCone.quasiIso_descShortComplex hS
  refine Iso.symm (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))) ?_ ?_ ?_)
  · dsimp [triangleOfSES]
    simp only [comp_id, id_comp]
  · dsimp
    simp only [← Q.map_comp, CochainComplex.mappingCone.inr_descShortComplex, id_comp]
  · dsimp [triangleOfSESδ]
    rw [CategoryTheory.Functor.map_id, comp_id, IsIso.hom_inv_id_assoc]

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' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11

Tactic:
obtain ⟨A₁, π₁, _, f₂, h₁⟩ :=
    surjective_up_to_refinements_of_epi (app' φ 2 _) (g₁ ≫ R₂.map' 1 2)

Goal state after:
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
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ g₁ = x ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ Ext S.X₃ S.X₁ 1

Tactic:
by
  have := hS.hasSmallLocalizedHom_S'_X₃_K
  have := hS.hasSmallLocalizedShiftedHom_K_S'_X₁
  change SmallHom W (S').X₃ ((S').X₁⟦(1 : ℤ)⟧)
  exact (SmallHom.mkInv qis hqis).comp (SmallHom.mk W δ)

Goal state after:
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 φ
⊢ (shiftFunctorZero (PullbackShift C φ) A).hom.app X =
    (pullbackShiftIso C φ 0 0 ⋯).hom.app X ≫ (shiftFunctorZero C B).hom.app X

Tactic:
by
  rw [← cancel_epi ((shiftFunctorZero _ A).inv.app X), Iso.inv_hom_id_app,
    pullbackShiftFunctorZero_inv_app, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
  rfl

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
⊢ (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app 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)

Tactic:
erw [@pullbackShiftFunctorAdd'_hom_app (OppositeShift C ℤ) _ _ _ _ _ _ _ X
    a₁ a₂ a₃ h b₁ b₂ b₃ (by dsimp; lia) (by dsimp; lia) (by dsimp; lia)]

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
⊢ (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₃ b₃ ⋯).hom.app X ≫
      (shiftFunctorAdd' (OppositeShift C ℤ) b₁ b₂ b₃ ⋯).hom.app X ≫
        (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₂ b₂ ⋯).inv.app
            ((shiftFunctor (OppositeShift C ℤ) b₁).obj X) ≫
          (shiftFunctor (PullbackShift (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯)) a₂).map
            ((pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₁ b₁ ⋯).inv.app 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)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n : ℤ
X : Cᵒᵖ
⊢ ((shiftFunctor Cᵒᵖ n).map
          ((NatIso.op (shiftFunctorCompIsoId C (-n) n ⋯) ≪≫
                  Functor.isoWhiskerRight (shiftFunctorOpIso C n (-n) ⋯).symm (shiftFunctor C n).op).hom.app
            X) ≫
        ((shiftFunctor C n).op.isoWhiskerLeft (shiftFunctorOpIso C n (-n) ⋯) ≪≫
                NatIso.op (shiftFunctorCompIsoId C n (-n) ⋯).symm).hom.app
          ((shiftFunctor Cᵒᵖ n).obj X)).unop =
    (𝟙 ((shiftFunctor Cᵒᵖ n).obj X)).unop

Tactic:
dsimp [shiftFunctorOpIso]
    erw [comp_id, Functor.map_id, comp_id]
    change (shiftFunctorCompIsoId C n (-n) (add_neg_cancel n)).inv.app (X.unop⟦-n⟧) ≫
      ((shiftFunctorCompIsoId C (-n) n (neg_add_cancel n)).hom.app X.unop)⟦-n⟧' = 𝟙 _
    rw [shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app n X.unop, Iso.inv_hom_id_app]

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

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
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : b + a = 0
inst✝ : F.CommShift A
X : D
⊢ (iso adj a).hom.app X =
    (shiftFunctorCompIsoId C b a h).inv.app (G.obj ((shiftFunctor D a).obj X)) ≫
      (shiftFunctor C a).map (adj.unit.app ((shiftFunctor C b).obj (G.obj ((shiftFunctor D a).obj X)))) ≫
        (shiftFunctor C a).map (G.map ((Functor.commShiftIso F b).hom.app (G.obj ((shiftFunctor D a).obj X)))) ≫
          (shiftFunctor C a).map (G.map ((shiftFunctor D b).map (adj.counit.app ((shiftFunctor D a).obj X)))) ≫
            (shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a b ⋯).hom.app X))

Tactic:
obtain rfl : b = -a := by rw [← add_left_inj a, h, neg_add_cancel]

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
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : F.CommShift A
X : D
h : -a + a = 0
⊢ (iso adj a).hom.app X =
    (shiftFunctorCompIsoId C (-a) a h).inv.app (G.obj ((shiftFunctor D a).obj X)) ≫
      (shiftFunctor C a).map (adj.unit.app ((shiftFunctor C (-a)).obj (G.obj ((shiftFunctor D a).obj X)))) ≫
        (shiftFunctor C a).map (G.map ((Functor.commShiftIso F (-a)).hom.app (G.obj ((shiftFunctor D a).obj X)))) ≫
          (shiftFunctor C a).map (G.map ((shiftFunctor D (-a)).map (adj.counit.app ((shiftFunctor D a).obj X)))) ≫
            (shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app X))
Module: Mathlib.CategoryTheory.Shift.Adjunction

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
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : b + a = 0
inst✝ : F.CommShift A
Y : D
⊢ (iso adj a).inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D b a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a b ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
obtain rfl : b = -a := by rw [← add_left_inj a, h, neg_add_cancel]

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
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : F.CommShift A
Y : D
h : -a + a = 0
⊢ (iso adj a).inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))
Module: Mathlib.CategoryTheory.Shift.Adjunction

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
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
X : C
⊢ (Functor.commShiftIso (𝟭 C) a).hom.app X ≫ (shiftFunctor C a).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C a).obj X) ≫ (Functor.commShiftIso (F ⋙ G) a).hom.app X

Tactic:
simpa only [Functor.commShiftIso_id_hom_app, Functor.comp_obj, Functor.id_obj, id_comp,
    Functor.commShiftIso_comp_hom_app] using! LeftAdjointCommShift.compatibilityUnit_iso adj a X

Goal state after:
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : PullbackShift C φ
⊢ (functor φ F).map
        (((NatTrans.PullbackShift.natIsoId C φ).hom ≫
              natTrans φ adj.unit ≫ (NatTrans.PullbackShift.natIsoComp φ F G).hom).app
          x✝) ≫
      ((NatTrans.PullbackShift.natIsoComp φ G F).inv ≫
            natTrans φ adj.counit ≫ (NatTrans.PullbackShift.natIsoId D φ).inv).app
        ((functor φ F).obj x✝) =
    𝟙 ((functor φ F).obj x✝)

Tactic:
simp [PullbackShift.natTrans, NatTrans.PullbackShift.natIsoComp,
      NatTrans.PullbackShift.natIsoId, PullbackShift.functor]

Goal state after:
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : PullbackShift D φ
⊢ ((NatTrans.PullbackShift.natIsoId C φ).hom ≫ natTrans φ adj.unit ≫ (NatTrans.PullbackShift.natIsoComp φ F G).hom).app
        ((functor φ G).obj x✝) ≫
      (functor φ G).map
        (((NatTrans.PullbackShift.natIsoComp φ G F).inv ≫
              natTrans φ adj.counit ≫ (NatTrans.PullbackShift.natIsoId D φ).inv).app
          x✝) =
    𝟙 ((functor φ G).obj x✝)

Tactic:
simp [PullbackShift.natTrans, NatTrans.PullbackShift.natIsoComp,
      NatTrans.PullbackShift.natIsoId, PullbackShift.functor]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ (Units.map ↑σ) ↑ξ ∈ rootsOfUnity n S

Tactic:
rw [mem_rootsOfUnity, ← map_pow, Units.ext_iff, Units.coe_map, ξ.prop]

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ ↑σ ↑1 = ↑1
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (i : n), 0 < ∑ j, A i j
⊢ A.det ≠ 0

Tactic:
rw [← Matrix.det_transpose]

Goal state after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (i : n), 0 < ∑ j, A i j
⊢ Aᵀ.det ≠ 0
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
⊢ Matrix.toLin' (↑A * ↑A⁻¹) = LinearMap.id

Tactic:
← coe_mul,

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ Matrix.toLin' ↑(A * A⁻¹) = LinearMap.id
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
⊢ Matrix.toLin' (↑A⁻¹ * ↑A) = LinearMap.id

Tactic:
← coe_mul,

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ Matrix.toLin' ↑(A⁻¹ * A) = LinearMap.id