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

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ Z✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ autoParam
    ((CategoryTheory.shiftFunctor C n).map (f.f ≫ g.f) =
      (CategoryTheory.shiftFunctor C n).map f.f ≫ (CategoryTheory.shiftFunctor C n).map g.f)
    ext._auto_1

Tactic:
;

Goal state after:
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ Z✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ autoParam
    ((CategoryTheory.shiftFunctor C n).map (f.f ≫ g.f) =
      (CategoryTheory.shiftFunctor C n).map f.f ≫ (CategoryTheory.shiftFunctor C n).map g.f)
    ext._auto_1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : n + 1 = m
⊢ h.d n m ≫ h.d m p = 0

pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : ¬n + 1 = m
⊢ h.d n m ≫ h.d m p = 0

Tactic:
;

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : n + 1 = m
⊢ h.d n m ≫ h.d m p = 0

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : ¬n + 1 = m
⊢ h.d n m ≫ h.d m p = 0
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : n + 1 = m
hmp : m + 1 = p
⊢ h.d n m ≫ h.d m p = 0

pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : n + 1 = m
hmp : ¬m + 1 = p
⊢ h.d n m ≫ h.d m p = 0

Tactic:
;

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : n + 1 = m
hmp : m + 1 = p
⊢ h.d n m ≫ h.d m p = 0

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : n + 1 = m
hmp : ¬m + 1 = p
⊢ h.d n m ≫ h.d m p = 0
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
p : ℤ
n : ℕ
hmp : Int.ofNat (n + 1) + 1 = p
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
⊢ ↑n + 1 + 1 = ↑n + 2

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
p : ℤ
n : ℕ
hmp : Int.ofNat (n + 1) + 1 = p
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
⊢ ↑n + 1 + 1 = ↑n + 2
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
p : ℤ
n : ℕ
hmp : Int.ofNat (n + 1) + 1 = p
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
⊢ p = Int.ofNat (n + 2)

Tactic:
by simp [← hmp]; lia

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case refine_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ autoParam
    (((shiftFunctor C (m + n)).map f ≫ (mkIso (shiftAdd Y✝.obj m n) ⋯).hom).f =
      ((mkIso (shiftAdd X✝.obj m n) ⋯).hom ≫ (shiftFunctor C m ⋙ shiftFunctor C n).map f).f)
    ext._auto_1

Tactic:
;

Goal state after:
case refine_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ autoParam
    (((shiftFunctor C (m + n)).map f ≫ (mkIso (shiftAdd Y✝.obj m n) ⋯).hom).f =
      ((mkIso (shiftAdd X✝.obj m n) ⋯).hom ≫ (shiftFunctor C m ⋙ shiftFunctor C n).map f).f)
    ext._auto_1
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case refine_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ autoParam
    ((CategoryTheory.shiftFunctor C (m + n)).map f.f ≫ (mkIso (shiftAdd Y✝.obj m n) ⋯).hom.f =
      (mkIso (shiftAdd X✝.obj m n) ⋯).hom.f ≫
        (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C m).map f.f))
    ext._auto_1

Tactic:
;

Goal state after:
case refine_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ autoParam
    ((CategoryTheory.shiftFunctor C (m + n)).map f.f ≫ (mkIso (shiftAdd Y✝.obj m n) ⋯).hom.f =
      (mkIso (shiftAdd X✝.obj m n) ⋯).hom.f ≫
        (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C m).map f.f))
    ext._auto_1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
⊢ -1 - ↑n = Int.negSucc n

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
⊢ -1 - ↑n = Int.negSucc n
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
⊢ -1 - (↑n + 1) = Int.negSucc (n + 1)

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
⊢ -1 - (↑n + 1) = Int.negSucc (n + 1)
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
this : n ≠ 0
⊢ (ComplexShape.embeddingUpIntGE 0).f (n - 1) = m - 1

Tactic:
;

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
this : n ≠ 0
⊢ (ComplexShape.embeddingUpIntGE 0).f (n - 1) = m - 1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ ↑n = m

Tactic:
;

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ ↑n = m
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ -1 - (↑n + 1) = m - 1

Tactic:
;

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ -1 - (↑n + 1) = m - 1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ -1 - ↑n = m

Tactic:
;

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ -1 - ↑n = m
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
this : n ≠ 0
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n - 1) = m + 1

Tactic:
;

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
this : n ≠ 0
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n - 1) = m + 1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
⊢ (match -1 with
    | Int.ofNat n => 𝟙 (L.X n)
    | Int.negSucc n => 𝟙 (K.X n)) =
    𝟙 (K.X 0)

Tactic:
;

Goal state after:
case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
⊢ (match -1 with
    | Int.ofNat n => 𝟙 (L.X n)
    | Int.negSucc n => 𝟙 (K.X n)) =
    𝟙 (K.X 0)
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ ((match -1 with
      | Int.ofNat n => fL.f n
      | Int.negSucc n => fK.f n) ≫
      match -1 with
      | Int.ofNat n => fL'.f n
      | Int.negSucc n => fK'.f n) =
    match -1 with
    | Int.ofNat n => fL.f n ≫ fL'.f n
    | Int.negSucc n => fK.f n ≫ fK'.f n

Tactic:
;

Goal state after:
case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ ((match -1 with
      | Int.ofNat n => fL.f n
      | Int.negSucc n => fK.f n) ≫
      match -1 with
      | Int.ofNat n => fL'.f n
      | Int.negSucc n => fK'.f n) =
    match -1 with
    | Int.ofNat n => fL.f n ≫ fL'.f n
    | Int.negSucc n => fK.f n ≫ fK'.f n
Module: Mathlib.Algebra.Homology.LeftResolution.Transport

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst✝¹ : Category.{v_3, u_4} C'
inst✝ : Category.{v_4, u_3} A'
ι : C ⥤ A
Λ : LeftResolution ι
ι' : C' ⥤ A
G : C ⥤ C'
e : G ⋙ ι' ≅ ι
x✝ : A
⊢ Epi (𝟙 (ι'.obj (G.obj (Λ.F.obj x✝))) ≫ e.hom.app (Λ.F.obj x✝) ≫ Λ.π.app x✝)

Tactic:
;

Goal state after:
A : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst✝¹ : Category.{v_3, u_4} C'
inst✝ : Category.{v_4, u_3} A'
ι : C ⥤ A
Λ : LeftResolution ι
ι' : C' ⥤ A
G : C ⥤ C'
e : G ⋙ ι' ≅ ι
x✝ : A
⊢ Epi (𝟙 (ι'.obj (G.obj (Λ.F.obj x✝))) ≫ e.hom.app (Λ.F.obj x✝) ≫ Λ.π.app x✝)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : ¬q + 1 = q'
⊢ ¬q + 1 = q'

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : ¬q + 1 = q'
⊢ ¬q + 1 = q'
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
⊢ (fromSingleEquiv h) (fromSingleMk f h) = f

Tactic:
simp [fromSingleEquiv]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
hp : ¬p' + 1 = p
⊢ ¬p' + 1 = p

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
hp : ¬p' + 1 = p
⊢ ¬p' + 1 = p
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
hα : (Cochain.fromSingleMk (f ≫ K.d q q') ⋯).v p q' ⋯ = Cochain.v 0 p q' ⋯
⊢ ↑(fromSingleMk f h q' hq' ⋯) = ↑α

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
hα : (Cochain.fromSingleMk (f ≫ K.d q q') ⋯).v p q' ⋯ = Cochain.v 0 p q' ⋯
⊢ ↑(fromSingleMk f h q' hq' ⋯) = ↑α
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ ↑(toSingleMk f h p' hp' ⋯) = ↑α

Tactic:
;

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ ↑(toSingleMk f h p' hp' ⋯) = ↑α
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ n + 1 + 1 = n + 2

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ n + 1 + 1 = n + 2
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n✝ : ℕ
⊢ Epi 0

Tactic:
;

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n✝ : ℕ
⊢ Epi 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ } ⟶
  { X₁ := kernel f, X₂ := X, X₃ := Y, f := kernel.ι f, g := f, zero := ⋯ } :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ }.X₂,
    τ₃ := 𝟙 { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ }.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := kernel f, X₂ := X, X₃ := Y, f := kernel.ι f, g := f, zero := ⋯ }.Exact

Tactic:
apply ShortComplex.exact_of_f_is_kernel

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ } ⟶
  { X₁ := kernel f, X₂ := X, X₃ := Y, f := kernel.ι f, g := f, zero := ⋯ } := ⋯
⊢ IsLimit (KernelFork.ofι { X₁ := kernel f, X₂ := X, X₃ := Y, f := kernel.ι f, g := f, zero := ⋯ }.f ⋯)
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ : F ⟶ G
X : Karoubi C
⊢ {
          app := fun P ↦
            F.map P.decompId_i ≫
              (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map τ).app P.X ≫ G.map P.decompId_p,
          naturality := ⋯ }.app
      X =
    τ.app X

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ : F ⟶ G
X : Karoubi C
⊢ {
          app := fun P ↦
            F.map P.decompId_i ≫
              (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map τ).app P.X ≫ G.map P.decompId_p,
          naturality := ⋯ }.app
      X =
    τ.app X
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: case e'_3
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
D₁ D₂ : ComposableArrows ι' 2
f : D₁ ⟶ D₂
this :
  X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫ homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯) ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₂) =
    X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₁) ≫
        (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))
⊢ (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv ≫
      (F.mapComposableArrows 1).map (homMk₁ (f.app 0) (f.app 1) ⋯) ≫
        (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom =
    homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯

Tactic:
;

Goal state after:
case e'_3
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
D₁ D₂ : ComposableArrows ι' 2
f : D₁ ⟶ D₂
this :
  X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫ homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯) ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₂) =
    X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₁) ≫
        (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))
⊢ (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv ≫
      (F.mapComposableArrows 1).map (homMk₁ (f.app 0) (f.app 1) ⋯) ≫
        (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom =
    homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Epi (Projective.π Z)

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Epi (Projective.π Z)
Module: Mathlib.Algebra.Homology.LocalCohomology

Goal state before:
pp: case h.inl
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : unop j1.left ≤ unop j2.left
⊢ Nonempty (j2 ⟶ j1)

Tactic:
;

Goal state after:
case h.inl
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : unop j1.left ≤ unop j2.left
⊢ Nonempty (j2 ⟶ j1)
Module: Mathlib.Algebra.Homology.LocalCohomology

Goal state before:
pp: case h.inr
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : unop j2.left ≤ unop j1.left
⊢ Nonempty (j1 ⟶ j2)

Tactic:
;

Goal state after:
case h.inr
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : unop j2.left ≤ unop j1.left
⊢ Nonempty (j1 ⟶ j2)