mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.restriction e).homologyπ j ≫
      ShortComplex.homologyMap
          ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e) ≫
            (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫ (natIsoSc' C c' i' j' k' hi'' hk'').inv.app K) ≫
        (K.sc j').homologyι =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j' ≫ (K.sc j').homologyι

Tactic:
apply (ShortComplex.π_homologyMap_ι _).trans

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ ((K.restriction e).sc j).iCycles ≫
      ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e) ≫
            (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫
              (natIsoSc' C c' i' j' k' hi'' hk'').inv.app K).τ₂ ≫
        (K.sc j').pOpcycles =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j' ≫ (K.sc j').homologyι
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'
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
hk'' : e.f k = k'
this : (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' = (K.extend e).d j' k'
⊢ (K.extend e).d j' k' = (K.extendXIso e hj').hom ≫ h.p ≫ h.g' ≫ (K.extendXIso e hk'').inv

Tactic:
K.extend_d_eq e hj' hk'',

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'
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
hk'' : e.f k = k'
this : (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' = (K.extend e).d j' k'
⊢ (K.extendXIso e hj').hom ≫ K.d j k ≫ (K.extendXIso e hk'').inv =
    (K.extendXIso e hj').hom ≫ h.p ≫ h.g' ≫ (K.extendXIso e hk'').inv
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.sc j').homologyπ ≫
      ShortComplex.homologyMap
          ((natIsoSc' C c' i' j' k' hi'' hk'').hom.app K ≫
            (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv ≫
              (natIsoSc' C c i j k hi hk).inv.app (K.restriction e)) ≫
        (K.restriction e).homologyι j =
    (K.sc j').homologyπ ≫ K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv

Tactic:
apply (ShortComplex.π_homologyMap_ι _).trans

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.sc j').iCycles ≫
      ((natIsoSc' C c' i' j' k' hi'' hk'').hom.app K ≫
            (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv ≫
              (natIsoSc' C c i j k hi hk).inv.app (K.restriction e)).τ₂ ≫
        ((K.restriction e).sc j).pOpcycles =
    (K.sc j').homologyπ ≫ K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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✝⁴ : 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
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
i : ι
hi : e.f i = i'
⊢ QuasiIsoAt (truncGEMap φ e) i'

Tactic:
simpa only [this i i' hi] using h i i' hi

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

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' : ι'
⊢ Epi (homologyMap (K.shortComplexTruncLE e).g i')

Tactic:
by_cases hi' : ∃ j', c'.Rel i' j'
  · obtain ⟨j', hj'⟩ := hi'
    exact ((K.shortComplexTruncLE_shortExact e).homology_exact₃ i' j' hj').epi_f (by simp)
  · exact epi_homologyMap_of_epi_of_not_rel _ _ (by simpa using hi')

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:
ext
    have h' := of_boundaryLE ac h
    have h'' := of_boundaryGE ac h'.snd
    exact fst_inj h'' h'

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

Goal state before:
pp: C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{v_2, u_2} C₁
inst✝⁷ : Category.{v_3, u_3} C₂
inst✝⁶ : Category.{v_4, u_4} C₃
inst✝⁵ : Category.{v_5, u_5} D₁
inst✝⁴ : Category.{v_6, u_6} D₂
inst✝³ : Category.{v_7, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f

Tactic:
by
  let G := Φ.localizedFunctor L₁ L₂
  let G' := Ψ.localizedFunctor L₂ L₃
  let e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso _ _ _ _
  let e' : Ψ.functor ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso _ _ _ _
  rw [Φ.homMap_apply L₁ L₂ G e, Ψ.homMap_apply L₂ L₃ G' e',
    (Φ.comp Ψ).homMap_apply L₁ L₃ (G ⋙ G')
      (Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ e' ≪≫
      (Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerRight e _ ≪≫
      Functor.associator _ _ _)]
  dsimp
  simp only [Functor.map_comp, assoc, comp_id, id_comp]

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
T : Triangle (CochainComplex C ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (homologyFunctor C (up ℤ) 0).homologySequenceδ ((quotient C (up ℤ)).mapTriangle.obj T) n₀ n₁ h =
    (homologyFunctorFactors C (up ℤ) n₀).hom.app T.obj₃ ≫
      (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯ ≫
        (homologyFunctorFactors C (up ℤ) n₁).inv.app T.obj₁

Tactic:
by
  apply homologyFunctor_shiftMap

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

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (ShiftedHom.mk₀ 0 mk₀._proof_1 ((singleFunctor C 0).map (biprod.lift (𝟙 X) (𝟙 X)))).comp
      ((ShiftedHom.mk₀ 0 mk₀._proof_1 ((singleFunctor C 0).map biprod.fst)).comp α.hom ⋯) ⋯ =
    α.hom

Tactic:
rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp,
      biprod.lift_fst, Functor.map_id, ShiftedHom.mk₀_id_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle ≅ triangleOfSES ⋯

Tactic:
refine Triangle.isoMk _ _ (e.app S.X₁) (e.app S.X₂) (e.app S.X₃) ?_ ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₁ ≫ (e.app S.X₂).hom = (e.app S.X₁).hom ≫ (triangleOfSES ⋯).mor₁

case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₂ ≫ (e.app S.X₃).hom = (e.app S.X₂).hom ≫ (triangleOfSES ⋯).mor₂

case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (e.app S.X₁).hom =
    (e.app S.X₃).hom ≫ (triangleOfSES ⋯).mor₃
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₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫
      HomologicalComplex.cyclesMap (descShortComplex S) n₀ ≫ HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
HomologicalComplex.liftCycles_comp_cyclesMap_assoc

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₁
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₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
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).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

Tactic:
← cancel_epi ((shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X),

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
⊢ (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X ≫ (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).inv.app 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
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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
⊢ IsIso (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)

Tactic:
let ψ : mk₄ (R₁.map' 0 1) (R₁.map' 1 2) (0 : _ ⟶ (0 : C)) (0 : _ ⟶ (0 : C)) ⟶
      mk₄ (R₂.map' 0 1) (R₂.map' 1 2) (0 : _ ⟶ (0 : C)) (0 : _ ⟶ (0 : C)) :=
    homMk₄ (app' φ 0) (app' φ 1) (app' φ 2) 0 0 (naturality' φ 0 1)
      (naturality' φ 1 2) (by simp) (by simp)
  refine isIso_of_epi_of_isIso_of_isIso_of_mono ?_ ?_ ψ h₀ h₁ inferInstance inferInstance
  · refine exact_of_δ₀ (hR₁.exact 0).exact_toComposableArrows (exact_of_δ₀ ?_ ?_)
    · refine exact₂_mk _ (by simp) ?_
      rwa [ShortComplex.exact_iff_epi _ (by simp)]
    · refine exact₂_mk _ (by simp) ?_
      rw [ShortComplex.exact_iff_epi _ (by simp)]
      infer_instance
  · refine exact_of_δ₀ (hR₂.exact 0).exact_toComposableArrows (exact_of_δ₀ ?_ ?_)
    · refine exact₂_mk _ (by simp) ?_
      rwa [ShortComplex.exact_iff_epi _ (by simp)]
    · refine exact₂_mk _ (by simp) ?_
      rw [ShortComplex.exact_iff_epi _ (by simp)]
      infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ (((shiftFunctor C c).map ((shiftFunctorAdd' Cᵒᵖ b a c ⋯).hom.app (Opposite.op X)).unop).op ≫
          ((shiftFunctorAdd' C a b c ⋯).inv.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ b ⋙ shiftFunctor Cᵒᵖ a).obj (Opposite.op X)))).op ≫
            ((shiftFunctor C b).map
                  ((opShiftFunctorEquivalence C a).unitIso.inv.app
                      ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop).op ≫
              (opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C c).map (Quiver.Hom.unop (f.comp g h)) =
    comp
      (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g))
      ((opEquiv a).symm f) ⋯

Tactic:
comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ (((shiftFunctor C c).map ((shiftFunctorAdd' Cᵒᵖ b a c ⋯).hom.app (Opposite.op X)).unop).op ≫
          ((shiftFunctorAdd' C a b c ⋯).inv.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ b ⋙ shiftFunctor Cᵒᵖ a).obj (Opposite.op X)))).op ≫
            ((shiftFunctor C b).map
                  ((opShiftFunctorEquivalence C a).unitIso.inv.app
                      ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop).op ≫
              (opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C c).map
        (f ≫ (shiftFunctor Cᵒᵖ a).map g ≫ (shiftFunctorAdd' Cᵒᵖ b a c h).inv.app (Opposite.op X)).unop =
    comp
      (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g))
      ((opEquiv a).symm f) ⋯
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n a : ℤ
x y : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ (opEquiv' n a a' h).symm (x + y) = (opEquiv' n a a' h).symm x + (opEquiv' n a a' h).symm y

Tactic:
by
  dsimp [opEquiv']
  rw [opEquiv_symm_add, Preadditive.add_comp]

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
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
a : A
b : B
h : b = φ a
⊢ commShiftIso (PullbackShift.functor φ F) a =
    isoWhiskerRight (pullbackShiftIso C φ a b h) F ≪≫
      commShiftIso F b ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ a b h).symm

Tactic:
by
  obtain rfl : b = φ a := h
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ (ConcreteCategory.hom
        ((preadditiveYoneda.obj B).homologySequenceδ ((triangleOpEquivalence C).functor.obj (op T)) n₀ n₁ h))
      x =
    T.mor₃ ≫ (shiftFunctor C 1).map x ≫ (shiftFunctorAdd' C n₀ 1 n₁ h).inv.app B

Tactic:
by
  simp only [Functor.homologySequenceδ, preadditiveYoneda_shiftMap_apply,
    ShiftedHom.comp, ← Category.assoc]
  congr 2
  apply (ShiftedHom.opEquiv _).injective
  rw [Equiv.apply_symm_apply]
  rfl

Goal state after:
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
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ (triangleOpEquivalence C).functor.obj (Opposite.op T) ∈ distinguishedTriangles

Tactic:
rw [mem_distTriang_op_iff']
  exact ⟨T, hT, ⟨Iso.refl _⟩⟩

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
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ iCycles K i ≫ π.f i =
    iCycles K i ≫
      (iCyclesIso K i (i + 1) ⋯ ⋯).inv ≫
        homologyπ K i ≫
          homologyMap π i ≫
            (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv

Tactic:
iCyclesIso_hom_inv_id_assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ iCycles K i ≫ π.f i =
    homologyπ K i ≫
      homologyMap π i ≫
        (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
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
μ : V₁ → K₁
h : J₁' (μ x) • (B x) x = 0
y : J₁' (μ x) = 0
⊢ μ x = 0

Tactic:
simpa using y

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

Goal state before:
pp: ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Finite κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
this : DecidableEq κ'
⊢ LinearMap.id ∘ₗ f = f

Tactic:
LinearMap.id_comp

Goal state after:
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Finite κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
this : DecidableEq κ'
⊢ f = f
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
⊢ f g = 1 g

Tactic:
obtain ⟨n, hn⟩ := hx ⟨f.toHomUnits g, g, rfl⟩

Goal state after:
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