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
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₁
Y Z : C
b : Y ⟶ Z
hY : P Y
hZ : P Z
⊢ ∃ X, ∃ (_ : P X), ∃ a c, Triangle.mk a b c ∈ distinguishedTriangles

Tactic:
obtain ⟨X, a, c, h⟩ := distinguished_cocone_triangle₁ b

Goal state after:
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 : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₁
Y Z : C
b : Y ⟶ Z
hY : P Y
hZ : P Z
X : C
a : X ⟶ Y
c : Z ⟶ (shiftFunctor C 1).obj X
h : Triangle.mk a b c ∈ distinguishedTriangles
⊢ ∃ X, ∃ (_ : P X), ∃ a c, Triangle.mk a b c ∈ distinguishedTriangles
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ c'.Rel (e.f j) (c'.next (e.f j))

pp: case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k)

Tactic:
· simpa only [c'.next_eq' hj] using hj

Goal state after:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k)
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

Tactic:
apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k

Tactic:
· rw [c'.next_eq_self _ hj, ← hjk, c.next_eq_self j]
    intro hj'
    apply hj
    rw [← e.rel_iff] at hj'
    simpa only [c'.next_eq' hj'] using hj'

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 ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

Tactic:
apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

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 ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'

Tactic:
apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

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
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : e.f j = j'
hij : j = i
⊢ i' = j'

Tactic:
by rw [← hj, hij, h]

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)
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c' j').map (K.πTruncGE e))

Tactic:
have : Epi φ.τ₁ := by
      by_cases hi : ∃ i, e.f i = c'.prev j'
      · obtain ⟨i, hi⟩ := hi
        dsimp [φ, πTruncGE]
        rw [e.epi_liftExtend_f_iff _ _ hi]
        infer_instance
      · apply IsZero.epi (isZero_extend_X _ _ _ (by simpa using hi))

Goal state after:
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)
this : Epi φ.τ₁
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c' j').map (K.πTruncGE e))
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case left.inr.inl
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
j₁ : ι₁
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inl j₁)
⊢ Sum.inr i₂ = Sum.inl j₁

pp: case left.inr.inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ j₂ : ι₂
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inr j₂)
⊢ Sum.inr i₂ = Sum.inr j₂

Tactic:
· exact (ac.disjoint _ _ h.symm).elim

Goal state after:
case left.inr.inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ j₂ : ι₂
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inr j₂)
⊢ Sum.inr i₂ = Sum.inr j₂
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
⊢ Function.Bijective (fromSum e₁ e₂)

Tactic:
constructor
  · rintro (i₁ | i₂) (j₁ | j₂) h
    · obtain rfl := e₁.injective_f h
      rfl
    · exact (ac.disjoint _ _ h).elim
    · exact (ac.disjoint _ _ h.symm).elim
    · obtain rfl := e₂.injective_f h
      rfl
  · intro n
    obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union n
    · exact ⟨Sum.inl i₁, rfl⟩
    · exact ⟨Sum.inr i₂, rfl⟩

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

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex C c
x✝ : Subtype e₁.BoundaryLE
i₁ : ι₁
h : e₁.BoundaryLE i₁
⊢ (fun x ↦
        match x with
        | ⟨i₂, h⟩ => ⟨indexOfBoundaryGE ac h, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨i₁, h⟩ => ⟨indexOfBoundaryLE ac h, ⋯⟩)
        ⟨i₁, h⟩) =
    ⟨i₁, h⟩

Tactic:
by
    ext
    have h' := of_boundaryLE ac h
    have h'' := of_boundaryGE ac h'.snd
    exact fst_inj h'' h'

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ (singleObjCyclesSelfIso c j A).hom ≫ (singleObjHomologySelfIso c j A).inv = ((single C c j).obj A).homologyπ j

Tactic:
by
  simp only [← cancel_mono (singleObjHomologySelfIso _ _ _).hom, assoc,
    Iso.inv_hom_id, comp_id, homologyπ_singleObjHomologySelfIso_hom]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
i : ℤ
k : ℕ
h : ∀ (i_1 : ℕ) (i' : ℤ), (embeddingUpIntLE (i + ↑k)).f i_1 = i' → QuasiIsoAt φ i'
hi : i ≤ i + ↑k
⊢ QuasiIsoAt φ i

Tactic:
exact h k _ (by dsimp; lia)

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝³ : L.IsLocalization W
X Y Z : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y Z
inst✝ : HasSmallLocalizedHom W X Z
α : SmallHom W X Y
β : SmallHom W Y Z
⊢ (equiv W L) (α.comp β) = (equiv W L) α ≫ (equiv W L) β

Tactic:
let := small_of_hasSmallLocalizedHom.{w} W W.Q X Y
  let := small_of_hasSmallLocalizedHom.{w} W W.Q Y Z
  obtain ⟨α, rfl⟩ := (equivShrink _).surjective α
  obtain ⟨β, rfl⟩ := (equivShrink _).surjective β
  dsimp [equiv, comp]
  rw [Equiv.symm_apply_apply]
  simp only [homEquiv_refl, homEquiv_comp]

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₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
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
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
⊢ ∀ (g : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4),
    g ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0 → g = 0

Tactic:
f₂

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₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
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
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
⊢ f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0 → f₂ = 0
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case neg
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₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ IsZero (S.X₃.homology i)

Tactic:
have := hS.epi_g
    have := HomologicalComplex.epi_homologyMap_of_epi_of_not_rel S.g i hi
    rw [IsZero.iff_id_eq_zero,
      ← cancel_epi (HomologicalComplex.homologyMap S.g i),
      ← cancel_epi (HomologicalComplex.homologyMap S.f i)]
    simp [← HomologicalComplex.homologyMap_comp]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
A : C
i : ι
γ : A ⟶ K.homology i
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ z, ∃ (hz : z ≫ K.d i (c.next i) = 0), π ≫ γ = K.liftCycles z (c.next i) ⋯ hz ≫ K.homologyπ i

Tactic:
exact (K.sc i).eq_liftCycles_homologyπ_up_to_refinements γ

Goal state after:
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
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    𝟙 (((singleFunctors C).functor 0).obj S.X₃) ≫
      inv
          (Q.map
            (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
        Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
          (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory C) 1).map
              ((𝟙 (((CochainComplex.singleFunctors C).postcomp Q).functor 0)).app S.X₁)

Tactic:
Category.id_comp,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    inv
        (Q.map
          (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
      Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
          (shiftFunctor (DerivedCategory C) 1).map
            ((𝟙 (((CochainComplex.singleFunctors C).postcomp Q).functor 0)).app S.X₁)
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
x✝ : Cᵒᵖ
⊢ (F.map ((shiftFunctorZero C A).inv.app (Opposite.unop x✝))).op ≫
      ((shiftFunctorZero D A).hom.app (F.obj (Opposite.unop x✝))).op =
    (OppositeShift.functor A F).map ((shiftFunctorZero (OppositeShift C A) A).hom.app x✝) ≫
      (shiftFunctorZero (OppositeShift D A) A).inv.app ((OppositeShift.functor A F).obj x✝)

Tactic:
erw [oppositeShiftFunctorZero_inv_app, oppositeShiftFunctorZero_hom_app]

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
x✝ : Cᵒᵖ
⊢ (F.map ((shiftFunctorZero C A).inv.app (Opposite.unop x✝))).op ≫
      ((shiftFunctorZero D A).hom.app (F.obj (Opposite.unop x✝))).op =
    (OppositeShift.functor A F).map ((shiftFunctorZero C A).inv.app (Opposite.unop x✝)).op ≫
      ((shiftFunctorZero D A).hom.app (Opposite.unop ((OppositeShift.functor A F).obj x✝))).op
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
x✝ : C
⊢ ((OppositeShift.functor A F).map ((shiftFunctorZero Cᵒᵖ A).inv.app (Opposite.op x✝))).unop ≫
      ((shiftFunctorZero Dᵒᵖ A).hom.app ((OppositeShift.functor A F).obj (Opposite.op x✝))).unop =
    F.map ((shiftFunctorZero C A).hom.app x✝) ≫ (shiftFunctorZero D A).inv.app (F.obj x✝)

Tactic:
oppositeShiftFunctorZero_hom_app,

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
x✝ : C
⊢ ((OppositeShift.functor A F).map ((shiftFunctorZero Cᵒᵖ A).inv.app (Opposite.op x✝))).unop ≫
      ((shiftFunctorZero D A).inv.app (Opposite.unop ((OppositeShift.functor A F).obj (Opposite.op x✝)))).op.unop =
    F.map ((shiftFunctorZero C A).hom.app x✝) ≫ (shiftFunctorZero D A).inv.app (F.obj x✝)
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: case e_a
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
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ ((shiftMonoidalFunctor C B).map (Functor.LaxMonoidal.μ (Discrete.addMonoidalFunctor φ) { as := a₁ } { as := a₂ })).app
      X =
    (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X

Tactic:
rw [Discrete.addMonoidalFunctor_μ]

Goal state after:
case e_a
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
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ ((shiftMonoidalFunctor C B).map (Discrete.eqToHom ⋯)).app X =
    (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.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 : a + b = 0
inst✝ : G.CommShift A
X : C
⊢ b + a = 0

Tactic:
by simp [eq_neg_of_add_eq_zero_left h]

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 : a + b = 0
inst✝ : G.CommShift A
Y : C
⊢ b + a = 0

Tactic:
by simp [eq_neg_of_add_eq_zero_left h]

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

Goal state before:
pp: case mpr
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
T : Triangle Cᵒᵖ
⊢ (∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))) →
    Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
· rintro ⟨T', hT', ⟨e⟩⟩
    refine isomorphic_distinguished _ hT' _ ?_
    exact Iso.unop ((triangleOpEquivalence C).unitIso.app (Opposite.op T') ≪≫
      (triangleOpEquivalence C).inverse.mapIso e.symm)

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
inst✝ : G.CommShift A
a : A
⊢ CommShift.CompatibilityUnit adj (iso adj a) (Functor.commShiftIso G a)

Tactic:
by
  intro
  rw [LeftAdjointCommShift.iso_hom_app adj _ _ (add_neg_cancel a)]
  simp only [Functor.id_obj, Functor.comp_obj, Functor.map_shiftFunctorCompIsoId_inv_app,
    Functor.map_comp, assoc, unit_naturality_assoc, right_triangle_components_assoc]
  slice_rhs 4 5 => rw [← Functor.map_comp, Iso.inv_hom_id_app]
  simp only [Functor.comp_obj, Functor.map_id, id_comp]
  rw [shift_shiftFunctorCompIsoId_inv_app, ← Functor.comp_map,
    (shiftFunctorCompIsoId C _ _ (neg_add_cancel a)).hom.naturality_assoc]
  simp

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ r • G.map e.inv ≫ 𝟙 (G.obj (L.obj (L.objPreimage X))) ≫ G.map e.hom = r • 𝟙 (G.obj X)

Tactic:
Category.id_comp,

Goal state after:
case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ r • G.map e.inv ≫ G.map e.hom = r • 𝟙 (G.obj X)
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 = LinearMap.id (v i)

Tactic:
id_apply,

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 ι
⊢ ∑ j, e.toMatrix (⇑v) j i • e j = v i
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hf : ↑↑x = 1
g : G
n : ℕ
hn : (fun x_1 ↦ x ^ x_1) n = ⟨f.toHomUnits g, ⋯⟩
⊢ f g = 1 g

Tactic:
simpa [hf, Subtype.ext_iff, Units.ext_iff] using hn.symm

Goal state after: