mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℤ
⊢ ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast.map' 1 2
        _proof_246✝ _proof_363✝ ≫
      (homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n =
    (homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂ ≫
      (composableArrows₅ hS n (n + 1) ⋯).δlast.map' 1 2 _proof_246✝ _proof_363✝

Tactic:
by

Goal state after:
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
a b : A
⊢ NatIso.removeOp (commShiftIso (OppositeShift.functor A F) (a + b)).symm =
    CommShift.isoAdd (NatIso.removeOp (commShiftIso (OppositeShift.functor A F) a).symm)
      (NatIso.removeOp (commShiftIso (OppositeShift.functor A F) b).symm)

Tactic:
by

Goal state after:
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 G : C ⥤ D
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
τ : F ⟶ G
inst✝ : CommShift τ A
x✝ : A
⊢ (Functor.commShiftIso (OppositeShift.functor A G) x✝).hom ≫
      Functor.whiskerRight (OppositeShift.natTrans A τ) (shiftFunctor (OppositeShift D A) x✝) =
    (shiftFunctor (OppositeShift C A) x✝).whiskerLeft (OppositeShift.natTrans A τ) ≫
      (Functor.commShiftIso (OppositeShift.functor A F) x✝).hom

Tactic:
by

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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
⊢ Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)

Tactic:
by

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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
⊢ R₂.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0

Tactic:
by

Goal state after:
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
x✝ : A
⊢ (Functor.commShiftIso (𝟭 (OppositeShift C A)) x✝).hom ≫
      Functor.whiskerRight (OppositeShift.natIsoId C A).hom (shiftFunctor (OppositeShift C A) x✝) =
    (shiftFunctor (OppositeShift C A) x✝).whiskerLeft (OppositeShift.natIsoId C A).hom ≫
      (Functor.commShiftIso (OppositeShift.functor A (𝟭 C)) x✝).hom

Tactic:
by

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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Mono (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
⊢ (mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app' φ 0 ⋯ =
    𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 _proof_297✝) ≫
      (mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 homMk₁._proof_4 _proof_298✝

Tactic:
by

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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Mono (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 _proof_297✝)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯
    ⋯
⊢ (mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2
      mono_of_epi_of_mono_of_mono'._proof_4 =
    0

Tactic:
by

Goal state after:
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
E : Type u_4
inst✝³ : Category.{v_3, u_4} E
inst✝² : HasShift E A
G : D ⥤ E
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝ : A
⊢ (Functor.commShiftIso (OppositeShift.functor A (F ⋙ G)) x✝).hom ≫
      Functor.whiskerRight (OppositeShift.natIsoComp A F G).hom (shiftFunctor (OppositeShift E A) x✝) =
    (shiftFunctor (OppositeShift C A) x✝).whiskerLeft (OppositeShift.natIsoComp A F G).hom ≫
      (Functor.commShiftIso (OppositeShift.functor A F ⋙ OppositeShift.functor A G) x✝).hom

Tactic:
by

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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Mono (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 _proof_297✝)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯
    ⋯
⊢ (mk₂
            ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9
              mono_of_epi_of_mono_of_mono'._proof_11)
            ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
              mono_of_epi_of_mono_of_mono'._proof_4)).map'
        0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      (mk₂
            ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9
              mono_of_epi_of_mono_of_mono'._proof_11)
            ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
              mono_of_epi_of_mono_of_mono'._proof_4)).map'
        1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0

Tactic:
by

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 : ℤ
⊢ ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast.map' 2 3
        _proof_299✝ _proof_364✝ ≫
      (homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁ =
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n) ≫
      (composableArrows₅ hS n (n + 1) ⋯).δlast.map' 2 3 _proof_299✝ _proof_364✝

Tactic:
by

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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Mono (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 _proof_297✝)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯
    ⋯
⊢ Epi (app' ψ 0 mono_of_epi_of_mono_of_mono'._proof_13)

Tactic:
by

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₂
⊢ CompatibilityCounit adj e₁ e₂

Tactic:
by

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

Tactic:
by

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

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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Mono (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 _proof_297✝)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯
    ⋯
⊢ {
        X₁ :=
          (mk₂
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9
                  mono_of_epi_of_mono_of_mono'._proof_11)
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)).obj
            ⟨0, ⋯⟩,
        X₂ :=
          (mk₂
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9
                  mono_of_epi_of_mono_of_mono'._proof_11)
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)).obj
            ⟨1, ⋯⟩,
        X₃ :=
          (mk₂
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9
                  mono_of_epi_of_mono_of_mono'._proof_11)
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)).obj
            ⟨2, ⋯⟩,
        f :=
          (mk₂
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9
                  mono_of_epi_of_mono_of_mono'._proof_11)
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)).map'
            0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
        g :=
          (mk₂
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9
                  mono_of_epi_of_mono_of_mono'._proof_11)
                ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)).map'
            1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
        zero := ⋯ }.f =
    0

Tactic:
by

Goal state after:
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
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
⊢ NatTrans.CommShift (OppositeShift.adjunction A adj).unit A

Tactic:
by

Goal state after:
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
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
⊢ NatTrans.CommShift (OppositeShift.adjunction A adj).counit A

Tactic:
by

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
a : A
b : B
h : b = φ a
⊢ shiftFunctor (PullbackShift C φ) a = shiftFunctor C b

Tactic:
by

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₃
⊢ 0 = φ 0

Tactic:
by

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).inv.app X =
    (shiftFunctorZero C B).inv.app X ≫ (pullbackShiftIso C φ 0 0 ⋯).inv.app X

Tactic:
by

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 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₀ : Mono (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
⊢ Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)

Tactic:
by

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 2
φ : R₁ ⟶ R₂
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)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Epi (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
⊢ (mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 _proof_299✝ _proof_300✝ ≫
      𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝) =
    app' φ 2 ⋯ ≫ (mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0).map' 2 3 _proof_299✝ _proof_300✝

Tactic:
by

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 2
φ : R₁ ⟶ R₂
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)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Epi (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝)) ⋯ ⋯
    ⋯
⊢ (mk₂
            ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
              mono_of_epi_of_mono_of_mono'._proof_4)
            ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
              mono_of_epi_of_mono_of_mono'._proof_7)).map'
        0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      (mk₂
            ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
              mono_of_epi_of_mono_of_mono'._proof_4)
            ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
              mono_of_epi_of_mono_of_mono'._proof_7)).map'
        1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0

Tactic:
by

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

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 : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ IsIso
    ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)

Tactic:
by

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₃
⊢ φ 0 = 0

Tactic:
by

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
⊢ e₂.inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
by

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 2
φ : R₁ ⟶ R₂
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)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Epi (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝)) ⋯ ⋯
    ⋯
⊢ (mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0).map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11
      mono_of_epi_of_mono_of_mono'._proof_7 =
    0

Tactic:
by

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 : ℤ
⊢ QuasiIsoAt (descShortComplex S) n

Tactic:
by

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).inv.app X =
    (shiftFunctorZero' C (φ 0) ⋯).inv.app X ≫ (pullbackShiftIso C φ 0 (φ 0) ⋯).inv.app X

Tactic:
by

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 2
φ : R₁ ⟶ R₂
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)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Epi (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝)) ⋯ ⋯
    ⋯
⊢ Mono (app' ψ 3 mono_of_epi_of_mono_of_mono'._proof_7)

Tactic:
by

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
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
S : ShortComplex (CochainComplex C ℤ)
⊢ (mapHomologicalComplexIso S.f F).hom ≫ descShortComplex (S.map (F.mapHomologicalComplex (up ℤ))) =
    (F.mapHomologicalComplex (up ℤ)).map (descShortComplex S)

Tactic:
by

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 (φ 0) ⋯).hom.app X

Tactic:
by

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 ℤ
⊢ ∀ (a b : ℤ), -(a + b) = -a + -b

Tactic:
by

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 ℤ
n m : ℤ
hnm : n + m = 0
⊢ m = -n

Tactic:
by

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 ℤ
n m : ℤ
hnm : n + m = 0
⊢ shiftFunctor Cᵒᵖ n = (shiftFunctor C m).op

Tactic:
obtain rfl : m = -n := by lia
  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 ℤ
n m : ℤ
hnm : n + m = 0
⊢ shiftFunctor Cᵒᵖ n = (shiftFunctor C m).op

Tactic:
by

Goal state after: