mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝³ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst✝¹ : Fibration f
inst✝ : WeakEquivalence w
h : RetractArrow f w
hw : (trivialCofibrations C).MapFactorizationData (fibrations C) w
this✝ : (trivialFibrations C).IsStableUnderRetracts
sq : CommSq (Arrow.Hom.left h.r) hw.i f (hw.p ≫ Arrow.Hom.right h.r)
hf : fibrations C f
this : HasLiftingProperty hw.i f
⊢ WeakEquivalence f

Tactic:
have : RetractArrow f hw.p :=
    { i := Arrow.homMk (h.i.left ≫ hw.i) h.i.right
      r := Arrow.homMk sq.lift h.r.right }

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝³ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst✝¹ : Fibration f
inst✝ : WeakEquivalence w
h : RetractArrow f w
hw : (trivialCofibrations C).MapFactorizationData (fibrations C) w
this✝¹ : (trivialFibrations C).IsStableUnderRetracts
sq : CommSq (Arrow.Hom.left h.r) hw.i f (hw.p ≫ Arrow.Hom.right h.r)
hf : fibrations C f
this✝ : HasLiftingProperty hw.i f
this : RetractArrow f hw.p
⊢ WeakEquivalence f
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²³ : Category.{v_1, u_1} C₁
inst✝²² : Category.{v_2, u_2} C₂
inst✝²¹ : Category.{v_3, u_5} C₃
inst✝²⁰ : Category.{v_4, u_6} C₄
inst✝¹⁹ : Category.{v_6, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := ⋯
h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
h₂ : ¬c₁.π c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
⊢ 0 + 0 = d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' + d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Tactic:
· congr 1
        · by_cases h₃ : c₂.Rel i₂ (c₂.next i₂)
          · rw [d₂_eq _ _ _ _ _ _ _ _ _ h₃, ιOrZero_eq_zero, comp_zero, smul_zero]
            intro h₄
            apply h₂
            rw [← h₄]
            dsimp [ComplexShape.r]
            rw [ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄, ComplexShape.next_π₁ c₃ c₂₃ h₃ i₃]
          · rw [d₂_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₃]
        · by_cases h₃ : c₃.Rel i₃ (c₃.next i₃)
          · rw [d₃_eq _ _ _ _ _ _ _ _ _ _ h₃, ιOrZero_eq_zero, comp_zero, smul_zero]
            intro h₄
            apply h₂
            rw [← h₄]
            dsimp [ComplexShape.r]
            rw [ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄, ComplexShape.next_π₂ c₂ c₂₃ i₂ h₃]
          · rw [d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₃]

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this✝¹ : Epi π
this✝ : Mono ι
n : ℤ
this :
  (↑(cocycle₁' sq hsq)).v n (n + 1) ⋯ ≫ X.d (n + 1) (n + 2) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq)).v (n + 1) (n + 2) ⋯ =
    0
⊢ π.f n ≫
      ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2) +
        Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)

Tactic:
Preadditive.comp_add,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this✝¹ : Epi π
this✝ : Mono ι
n : ℤ
this :
  (↑(cocycle₁' sq hsq)).v n (n + 1) ⋯ ≫ X.d (n + 1) (n + 2) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq)).v (n + 1) (n + 2) ⋯ =
    0
⊢ π.f n ≫ (cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2) +
      π.f n ≫ Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ ≫ ι.f (n + 2) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma

Goal state before:
pp: case left
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : CofibrantBrownFactorization f
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (coprod.desc f (𝟙 Y))
⊢ Fibration h.p

pp: case right
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : CofibrantBrownFactorization f
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (coprod.desc f (𝟙 Y))
⊢ WeakEquivalence h.p

Tactic:
<;>

Goal state after:
case left
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : CofibrantBrownFactorization f
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (coprod.desc f (𝟙 Y))
⊢ Fibration h.p

case right
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : CofibrantBrownFactorization f
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (coprod.desc f (𝟙 Y))
⊢ WeakEquivalence h.p
Module: Mathlib.AlgebraicTopology.ModelCategory.BrownLemma

Goal state before:
pp: case left
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : FibrantBrownFactorization f
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (prod.lift f (𝟙 X))
⊢ Cofibration h.i

pp: case right
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : FibrantBrownFactorization f
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (prod.lift f (𝟙 X))
⊢ WeakEquivalence h.i

Tactic:
<;>

Goal state after:
case left
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : FibrantBrownFactorization f
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (prod.lift f (𝟙 X))
⊢ Cofibration h.i

case right
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
X Y : C
f : X ⟶ Y
h✝ : FibrantBrownFactorization f
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (prod.lift f (𝟙 X))
⊢ WeakEquivalence h.i
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : C
inst✝ : IsFibrant Y
f g : resolutionObj X ⟶ Y
h : RightHomotopyRel (iResolutionObj X ≫ f) (iResolutionObj X ≫ g)
⊢ toHoCat.map (homMk f) = toHoCat.map (homMk g)

Tactic:
apply toHoCat_map_eq
  rw [homRel_iff_leftHomotopyRel]
  apply RightHomotopyRel.leftHomotopyRel
  rw [← RightHomotopyClass.mk_eq_mk_iff] at h ⊢
  exact (RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence
    (f := iResolutionObj X) (Z := Y)).1 h

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: case mpr
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
hF : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
X₂ : C₂
R : Φ.RightResolution X₂
⊢ F.HasPointwiseRightDerivedFunctorAt W₂ X₂

Tactic:
simpa only [hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure,
      ← F.hasPointwiseRightDerivedFunctorAt_iff_of_mem W₂ R.w R.hw] using hF R.X₁

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
eT : C₂ ≌ C₃
eB : D₂ ≌ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
⊢ (w ≫ₕ w'.hom).GuitartExact ↔ w.GuitartExact

Tactic:
let w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
  have : (w ≫ₕ w'.hom).op = (w.op ≫ᵥ w''.hom) := by ext; simp [w'']
  rw [← guitartExact_op_iff, ← guitartExact_op_iff w,
    ← vComp_iff_of_equivalences _ _ _ w'', this]
  rfl

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
K : Plus (InjectiveObject C)
⊢ fibrantObjects (Plus C) ((InjectiveObject.ι C).mapCochainComplexPlus.obj K)

Tactic:
by
    dsimp [fibrantObjects]
    rw [modelCategoryQuillen.isFibrant_iff]
    intro n
    dsimp
    infer_instance

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

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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ (K.stupidTrunc e).IsStrictlySupported e

Tactic:
dsimp [stupidTrunc]
  infer_instance

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

Goal state before:
pp: case pos.inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel k i₁
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f k = φ'.f k
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ.f k = φ'.f k

pp: case pos.inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel i₀ k
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f k = φ'.f k
⊢ φ.f k = φ'.f k

Tactic:
<;>

Goal state after:
case pos.inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel k i₁
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f k = φ'.f k
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ.f k = φ'.f k

case pos.inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel i₀ k
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f k = φ'.f k
⊢ φ.f k = φ'.f k
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: case pos.inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel k i₁
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f k = φ'.f k
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ.f k = φ'.f k

pp: case pos.inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel i₀ k
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f k = φ'.f k
⊢ φ.f k = φ'.f k

Tactic:
<;>

Goal state after:
case pos.inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel k i₁
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f k = φ'.f k
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ.f k = φ'.f k

case pos.inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ : ι
K : HomologicalComplex C c
k : ι
hi₀₁ : c.Rel i₀ k
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f k = φ'.f k
⊢ φ.f k = φ'.f k
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case 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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = ↑0
inst✝ : HasHomology L 0
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0
⊢ (ComplexShape.up ℕ).prev 0 = 0 - 1

pp: case succ
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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = ↑(n✝ + 1)
inst✝ : HasHomology L (n✝ + 1)
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n✝ + 1)
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1

Tactic:
<;>

Goal state after:
case 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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = ↑0
inst✝ : HasHomology L 0
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0
⊢ (ComplexShape.up ℕ).prev 0 = 0 - 1

case succ
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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = ↑(n✝ + 1)
inst✝ : HasHomology L (n✝ + 1)
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n✝ + 1)
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: case neg.inl
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
h✝ : ∃ k, c.Rel j k ∧ j ≠ k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1

pp: case neg.inr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
h✝ : ∀ (k : ι), ¬c.Rel j k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1

Tactic:
<;>

Goal state after:
case neg.inl
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
h✝ : ∃ k, c.Rel j k ∧ j ≠ k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1

case neg.inr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
h✝ : ∀ (k : ι), ¬c.Rel j k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case 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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = ↑0
inst✝ : HasHomology L 0
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0
this : 0 ≠ 0
⊢ (ComplexShape.embeddingUpIntGE 0).f (0 - 1) = m - 1

pp: case succ
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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = ↑(n✝ + 1)
inst✝ : HasHomology L (n✝ + 1)
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n✝ + 1)
this : n✝ + 1 ≠ 0
⊢ (ComplexShape.embeddingUpIntGE 0).f (n✝ + 1 - 1) = m - 1

Tactic:
<;>

Goal state after:
case 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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = ↑0
inst✝ : HasHomology L 0
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0
this : 0 ≠ 0
⊢ (ComplexShape.embeddingUpIntGE 0).f (0 - 1) = m - 1

case succ
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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = ↑(n✝ + 1)
inst✝ : HasHomology L (n✝ + 1)
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n✝ + 1)
this : n✝ + 1 ≠ 0
⊢ (ComplexShape.embeddingUpIntGE 0).f (n✝ + 1 - 1) = m - 1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case 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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = ↑0
inst✝ : HasHomology L 0
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0
this : 0 ≠ 0
⊢ 0 = m - 1

pp: case succ
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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = ↑(n✝ + 1)
inst✝ : HasHomology L (n✝ + 1)
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n✝ + 1)
this : n✝ + 1 ≠ 0
⊢ ↑n✝ = m - 1

Tactic:
<;>

Goal state after:
case 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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = ↑0
inst✝ : HasHomology L 0
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0
this : 0 ≠ 0
⊢ 0 = m - 1

case succ
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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = ↑(n✝ + 1)
inst✝ : HasHomology L (n✝ + 1)
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n✝ + 1)
this : n✝ + 1 ≠ 0
⊢ ↑n✝ = m - 1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case 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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = -↑(0 + 1)
inst✝ : HasHomology K 0
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0
⊢ (ComplexShape.down ℕ).next 0 = 0 - 1

pp: case succ
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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = -↑(n✝ + 1 + 1)
inst✝ : HasHomology K (n✝ + 1)
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology (n✝ + 1)
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1

Tactic:
<;>

Goal state after:
case 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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = -↑(0 + 1)
inst✝ : HasHomology K 0
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0
⊢ (ComplexShape.down ℕ).next 0 = 0 - 1

case succ
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''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = -↑(n✝ + 1 + 1)
inst✝ : HasHomology K (n✝ + 1)
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology (n✝ + 1)
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1