mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ (↑(inr φ)).v p q hpq ≫ (fst φ).f q = 0

Tactic:
simp [inr, fst, Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero p),
    Cochain.leftShift_v _ _ _ _ _ _ _ _ hpq]

Goal state after:
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✝³ : P.IsTriangulated
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : F.Full
⊢ ∀ T ∈ distinguishedTriangles, F.essImage T.obj₁ → F.essImage T.obj₃ → F.essImage T.obj₂

Tactic:
by
    rintro T hT ⟨X₁, ⟨e₁⟩⟩ ⟨X₃, ⟨e₃⟩⟩
    have ⟨h, hh⟩ := F.map_surjective (e₃.hom ≫ T.mor₃ ≫ e₁.inv⟦1⟧' ≫
      (F.commShiftIso (1 : ℤ)).inv.app X₁)
    obtain ⟨X₂, f, g, H⟩ := distinguished_cocone_triangle₂ h
    exact ⟨X₂, ⟨Triangle.π₂.mapIso
      (isoTriangleOfIso₁₃ _ _ (F.map_distinguished _ H) hT e₁ e₃
        (by simp [hh, ← Functor.map_comp]))⟩⟩

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

Goal state before:
pp: case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ Quiver.Hom.op 0 = 0

Tactic:
op_zero,

Goal state after:
case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ 0 = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel i j
⊢ Quiver.Hom.op 0 ≫ (K.cyclesOpIso i).inv = 0

Tactic:
op_zero,

Goal state after:
case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel i j
⊢ 0 ≫ (K.cyclesOpIso i).inv = 0
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.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ c'.prev (e.f j) = e.f i

Tactic:
obtain rfl : j = i := by
      simpa only [c.prev_eq_self j (by simpa only [hij] using hij')] using hij
    apply c'.prev_eq_self
    intro hj'
    simp only [BoundaryGE, not_and, not_forall, not_not] at hj
    obtain ⟨i, hi⟩ := hj hj'
    rw [e.rel_iff] at hi
    rw [c.prev_eq' hi] at hij
    exact hij' (by simpa only [hij] using hi)

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
⊢ ¬e.BoundaryLE i

Tactic:
dsimp [BoundaryLE]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
⊢ ¬(c'.Rel (e.f i) (c'.next (e.f i)) ∧ ∀ (k : ι), ¬c'.Rel (e.f i) (e.f k))
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
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Projective (K.X i)
i' : ι'
⊢ Projective ((K.extend e).X i')

Tactic:
by_cases! hi' : ∃ i, e.f i = i'

Goal state after:
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 : ι), Projective (K.X i)
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ Projective ((K.extend e).X i')

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
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Projective (K.X i)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Projective ((K.extend e).X i')
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
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Projective (K.X i)
i' : ι'
⊢ Projective ((K.extend e).X i')

Tactic:
by
  by_cases! hi' : ∃ i, e.f i = i'
  · obtain ⟨i, hi⟩ := hi'
    exact Projective.of_iso (K.extendXIso e hi).symm inferInstance
  · exact (isZero_extend_X K e i' hi').projective

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
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Injective (K.X i)
i' : ι'
⊢ Injective ((K.extend e).X i')

Tactic:
by_cases! hi' : ∃ i, e.f i = i'

Goal state after:
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' : ι'
hi' : ∃ i, e.f i = i'
⊢ Injective ((K.extend e).X i')

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
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Injective (K.X i)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Injective ((K.extend e).X i')
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 : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).pOpcycles =
    (K.extendXIso e hj').inv ≫
      ((K.extendXIso e hj').hom ≫ (K.sc j).homologyData.right.p) ≫ (K.sc j).homologyData.right.opcyclesIso.inv

Tactic:
rw [assoc, Iso.inv_hom_id_assoc, ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv]

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).pOpcycles = (K.sc' (c.prev j) j (c.next j)).pOpcycles
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

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
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
⊢ K.πTruncGE e ≫ truncGEMap φ e = φ ≫ L.πTruncGE e

Tactic:
by
  apply (e.homEquiv _ _).injective
  ext1
  dsimp [truncGEMap, πTruncGE]
  rw [e.homRestrict_comp_extendMap, e.homRestrict_liftExtend, e.homRestrict_precomp,
    e.homRestrict_liftExtend, restrictionToTruncGE'_naturality]

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

Goal state before:
pp: case inr
ι : 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
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
i₂ : ι₂
⊢ φ.f (e₂.f i₂) = HomologicalComplex.Hom.f 0 (e₂.f i₂)

Tactic:
· apply (hK.isZero i₂).eq_of_src

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

Goal state before:
pp: 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
n : ℤ
⊢ QuasiIso (truncLEMap φ n) ↔ ∀ i ≤ n, QuasiIsoAt φ i

Tactic:
by
  rw [HomologicalComplex.quasiIso_truncLEMap_iff]
  constructor
  · intro h i hi
    obtain ⟨k, rfl⟩ := Int.le.dest hi
    exact h k _ (by dsimp; lia)
  · rintro h i i' rfl
    exact h _ (by dsimp; lia)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (∀ (X Y : C),
      HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ
        ((CochainComplex.singleFunctor C 0).obj X) ((CochainComplex.singleFunctor C 0).obj Y)) ↔
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))

Tactic:
simp only [hasSmallLocalizedShiftedHom_iff _ _ Q]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        ((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)))) ↔
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (homologyFunctor C (up ℤ) 0).homologySequenceδ
        (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
          ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ (Functor.commShiftIso (quotient C (up ℤ)) 1).hom.app S.X₁))
        n₀ n₁ h ≫
      (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁ =
    (homologyFunctorFactors C (up ℤ) n₀).hom.app (mappingCone S.f) ≫
      HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
        hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁)

Tactic:
← cancel_epi ((homologyFunctorFactors C (up ℤ) n₀).inv.app _),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
      (homologyFunctor C (up ℤ) 0).homologySequenceδ
          (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
            ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ (Functor.commShiftIso (quotient C (up ℤ)) 1).hom.app S.X₁))
          n₀ n₁ h ≫
        (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁ =
    (homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
      (homologyFunctorFactors C (up ℤ) n₀).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
          hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁)
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
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ (extFunctorObj (Opposite.unop X₁) n).map g ≫
      AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f.unop).comp α ⋯) ⋯) =
    AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f.unop).comp α ⋯) ⋯) ≫
      (extFunctorObj (Opposite.unop X₂) n).map g

Tactic:
ext α
        dsimp
        symm
        apply Ext.comp_assoc
        all_goals lia

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
⊢ Ext S.X₃ S.X₁ 1

Tactic:
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.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (HomologicalComplex.XIsoOfEq S.X₁ ⋯).hom)
        (n₁ + 1) ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₁ n₁ ≫ 𝟙 (HomologicalComplex.homology S.X₁ n₁) =
    S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁

Tactic:
simp only [hab, add_comp, assoc, inl_v_triangle_mor₃_f_assoc,
    shiftFunctorObjXIso, neg_comp, Iso.inv_hom_id, comp_neg, comp_id,
    inr_f_triangle_mor₃_f_assoc, zero_comp, comp_zero, add_zero]

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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y))
⊢ adj.unit.app (G.obj ((shiftFunctor D a).obj Y)) ≫ G.map (adj.counit.app ((shiftFunctor D a).obj Y)) =
    e₂.hom.app Y ≫
      (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫
        e₂.inv.app (F.obj (G.obj Y)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
erw [← e₂.inv.naturality]

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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y))
⊢ adj.unit.app (G.obj ((shiftFunctor D a).obj Y)) ≫ G.map (adj.counit.app ((shiftFunctor D a).obj Y)) =
    e₂.hom.app Y ≫
      (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app Y
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✝ F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : OppositeShift C A
⊢ ((NatTrans.OppositeShift.natIsoId D A).hom ≫
            natTrans A adj.counit ≫ (NatTrans.OppositeShift.natIsoComp A G F).hom).app
        ((functor A F).obj x✝) ≫
      (functor A F).map
        (((NatTrans.OppositeShift.natIsoComp A F G).inv ≫
              natTrans A adj.unit ≫ (NatTrans.OppositeShift.natIsoId C A).inv).app
          x✝) =
    𝟙 ((functor A F).obj x✝)

Tactic:
by
    dsimp [OppositeShift.natTrans, NatTrans.OppositeShift.natIsoComp,
      NatTrans.OppositeShift.natIsoId, OppositeShift.functor]
    simp only [comp_id, id_comp, Quiver.Hom.unop_op]
    rw [← op_comp, adj.left_triangle_components]
    rfl

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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))
⊢ e₂.inv.app Y =
    (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
erw [← e₂.inv.naturality]

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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))
⊢ e₂.inv.app Y =
    (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫
      (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app ((𝟭 D).obj Y)
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₃
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ a₃ h).hom.app X =
    (pullbackShiftIso C φ a₃ b₃ h₃).hom.app X ≫
      (shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app X ≫
        (pullbackShiftIso C φ a₂ b₂ h₂).inv.app ((shiftFunctor C b₁).obj X) ≫
          (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).inv.app X)

Tactic:
rw [← cancel_epi ((shiftFunctorAdd' _ a₁ a₂ a₃ h).inv.app X), Iso.inv_hom_id_app,
    pullbackShiftFunctorAdd'_inv_app φ X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃, assoc, assoc, assoc,
    Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app_assoc, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]
  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
⊢ 𝟙 ((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 (𝟙 ((shiftFunctor C b₁).op.obj 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:
erw [Functor.map_id, id_comp, Iso.inv_hom_id_app_assoc]

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 ≫
        ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : HasDerivedCategory C
X Y Z : C
n : ℕ
x : Ext X Y n
f : Y ⟶ Z
⊢ x.hom ≫ (shiftFunctor (DerivedCategory C) ↑n).map ((singleFunctor C 0).map f) = (x.comp (mk₀ f) ⋯).hom

Tactic:
by
  simp only [comp_hom, mk₀_hom, ShiftedHom.comp_mk₀]

Goal state after:
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
⊢ Submodule.span K₁ ↑{x} ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ ↑{x}) = ⊥

Tactic:
refine eq_bot_iff.2 fun y h ↦ ?_

Goal state after:
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
y : V₁
h : y ∈ Submodule.span K₁ ↑{x} ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ ↑{x})
⊢ y ∈ ⊥
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: K : Type u_7
V : Type u_9
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : (B x) x ≠ 0
⊢ K ∙ x ⊔ Submodule.orthogonalBilin B (K ∙ x) = ⊤

Tactic:
rw [orthogonal_span_singleton_eq_to_lin_ker]
  exact (B x).span_singleton_sup_ker_eq_top hx

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
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ (↑g).det ≠ 0

Tactic:
g.det_coe

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ 1 ≠ 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 : ↥(center (SpecialLinearGroup n R))
⊢ ↑↑A = (scalar n) ↑↑(center_equiv_rootsOfUnity A)

Tactic:
unfold center_equiv_rootsOfUnity Or.by_cases
  split_ifs with h
  · subsingleton
  dsimp only
  generalize_proofs _ eq
  generalize max (Fintype.card n) 1 = c at eq
  subst eq
  rw [center_equiv_rootsOfUnity'_apply, rootsOfUnity.val_mkOfPowEq_coe,
    scalar_eq_coe_self_center]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
Q : QuadraticMap R N P
f : M →ₗ[R] N
B : BilinMap R N P
h : ∀ (x y : N), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ Q (f (x + y)) = Q (f x) + Q (f y) + ((LinearMap.compl₁₂ B f f) x) y

Tactic:
by simp_rw [f.map_add]; exact h (f x) (f y)

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
f g : M →ₗ[R] R
x✝¹ x✝ : M
⊢ (f x✝¹ + f x✝) * (g x✝¹ + g x✝) - f x✝¹ * g x✝¹ - f x✝ * g x✝ = f x✝¹ * g x✝ + g x✝¹ * f x✝

Tactic:
ring_nf

Goal state after: