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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f✝ : C ⟶ D
i : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X✝ Y✝ : W₁
f : X✝ ⟶ Y✝
⊢ (single W₁ c j ⋙ F.mapHomologicalComplex c).map f ≫
      { hom := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
          inv := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom =
    { hom := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
          inv := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      (F ⋙ single W₂ c j).map f

Tactic:
ext i

Goal state after:
ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f✝ : C ⟶ D
i✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X✝ Y✝ : W₁
f : X✝ ⟶ Y✝
i : ι
⊢ ((single W₁ c j ⋙ F.mapHomologicalComplex c).map f ≫
          { hom := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
              inv := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.hom).f
      i =
    ({ hom := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
              inv := { f := fun i ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
              inv_hom_id := ⋯ }.hom ≫
          (F ⋙ single W₂ c j).map f).f
      i
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
j : J
⊢ { f := fun i ↦ (hs i).lift ((eval C c i).mapCone t), comm' := ⋯ } ≫ s.π.app j = t.π.app j

Tactic:
ext i

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
j : J
i : ι
⊢ ({ f := fun i ↦ (hs i).lift ((eval C c i).mapCone t), comm' := ⋯ } ≫ s.π.app j).f i = (t.π.app j).f i
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), m ≫ s.π.app j = t.π.app j
⊢ m = { f := fun i ↦ (hs i).lift ((eval C c i).mapCone t), comm' := ⋯ }

Tactic:
ext i

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), m ≫ s.π.app j = t.π.app j
i : ι
⊢ m.f i = { f := fun i ↦ (hs i).lift ((eval C c i).mapCone t), comm' := ⋯ }.f i
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cocone F
hs : (i : ι) → IsColimit ((eval C c i).mapCocone s)
t : Cocone F
j : J
⊢ s.ι.app j ≫ { f := fun i ↦ (hs i).desc ((eval C c i).mapCocone t), comm' := ⋯ } = t.ι.app j

Tactic:
ext i

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cocone F
hs : (i : ι) → IsColimit ((eval C c i).mapCocone s)
t : Cocone F
j : J
i : ι
⊢ (s.ι.app j ≫ { f := fun i ↦ (hs i).desc ((eval C c i).mapCocone t), comm' := ⋯ }).f i = (t.ι.app j).f i
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cocone F
hs : (i : ι) → IsColimit ((eval C c i).mapCocone s)
t : Cocone F
m : s.pt ⟶ t.pt
hm : ∀ (j : J), s.ι.app j ≫ m = t.ι.app j
⊢ m = { f := fun i ↦ (hs i).desc ((eval C c i).mapCocone t), comm' := ⋯ }

Tactic:
ext i

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cocone F
hs : (i : ι) → IsColimit ((eval C c i).mapCocone s)
t : Cocone F
m : s.pt ⟶ t.pt
hm : ∀ (j : J), s.ι.app j ≫ m = t.ι.app j
i : ι
⊢ m.f i = { f := fun i ↦ (hs i).desc ((eval C c i).mapCocone t), comm' := ⋯ }.f i
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X)) =
    (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app X) ≫
      (shiftFunctorComm C n 0).inv.app X ≫ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X)

Tactic:
shiftFunctorZero_hom_app_shift,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X)) =
    (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app X) ≫
      (shiftFunctorComm C n 0).inv.app X ≫
        (shiftFunctorComm C n 0).hom.app X ≫ (shiftFunctor C n).map ((shiftFunctorZero C A).hom.app X)
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology
⊢ 𝟙 S.homology = 0

Tactic:
ext i

Goal state after:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology
i : ι
⊢ (𝟙 S.homology).f i = Hom.f 0 i
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ K.liftCycles k j hj ⋯ = 0

Tactic:
K.shape _ _ h,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx✝ : k = x ≫ K.d i' i
hx : k = x ≫ 0
h : ¬c.Rel i' i
⊢ K.liftCycles k j hj ⋯ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ K.descOpcycles k j hj ⋯ = 0

Tactic:
K.shape _ _ h,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx✝ : k = K.d i i' ≫ x
hx : k = 0 ≫ x
h : ¬c.Rel i i'
⊢ K.descOpcycles k j hj ⋯ = 0
Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.inl ≫ (K.biprodXIso L i).inv = biprod.inl.f i

Tactic:
by
  simp [biprodXIso]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.inr ≫ (K.biprodXIso L i).inv = biprod.inr.f i

Tactic:
by
  simp [biprodXIso]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ (K.biprodXIso L i).hom ≫ biprod.fst = biprod.fst.f i

Tactic:
by
  simp [biprodXIso]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ (K.biprodXIso L i).hom ≫ biprod.snd = biprod.snd.f i

Tactic:
by
  simp [biprodXIso]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B ⊗[A] Ω[A⁄R]
⊢ (mapBaseChange R A B) x ∈ (map R A B B).ker

Tactic:
induction x with

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case e'_3
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
⊢ (map R A B B).ker = Submodule.map (linearCombination B ⇑(D R B)) (kerTotal A B)

Tactic:
rw [KaehlerDifferential.ker_map]

Goal state after:
case e'_3
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
⊢ Submodule.map (linearCombination B ⇑(D R B))
      (Submodule.comap (mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B ⇑(algebraMap B B))
        (Submodule.restrictScalars B (kerTotal A B))) =
    Submodule.map (linearCombination B ⇑(D R B)) (kerTotal A B)
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E₁ : Type u_3
E₂ : Type u_4
inst✝¹ : Category.{v_3, u_3} E₁
inst✝ : Category.{v_4, u_4} E₂
F₁ : C₁ ⥤ E₁
F₂ : C₂ ⥤ E₂
h₁ : W₁.IsInvertedBy F₁
h₂ : W₂.IsInvertedBy F₂
x✝¹ x✝ : C₁ × C₂
f : x✝¹ ⟶ x✝
hf : W₁.prod W₂ f
⊢ IsIso ((F₁.prod F₂).map f)

Tactic:
rw [isIso_prod_iff]
  exact ⟨h₁ _ hf.1, h₂ _ hf.2⟩

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
⊢ inrX φ i ≫ sndX φ i = 𝟙 (G.X i)

Tactic:
by
  dsimp [sndX, inrX]
  split_ifs with hi <;> simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ inlX φ i j hij ≫ sndX φ j = 0

Tactic:
obtain rfl := c.next_eq' hij
  simp [inlX, sndX, dif_pos hij]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
⊢ p₁ + n₁₂ = p₃

Tactic:
by rw [← h₂, ← h₁, ← h, add_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
⊢ (z₁.comp z₂ ⋯).v p (p + n₁ + n₂) ⋯ ≫ z₃.v (p + n₁ + n₂) q ⋯ = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq

Tactic:
comp_v z₁ z₂ rfl p (p + n₁) (p + n₁ + n₂) (by lia) (by lia),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₂ n₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
p q : ℤ
hpq : p + (n₁ + n₂ + n₃) = q
⊢ (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ z₃.v (p + n₁ + n₂) q ⋯ = (z₁.comp (z₂.comp z₃ ⋯) ⋯).v p q hpq
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case h₁
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ (inlX φ j i hij ≫ d φ i j) ≫ fstX φ j k hjk = (-F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j) ≫ fstX φ j k hjk

Tactic:
simp [d_fstX φ _ _ _ hij hjk]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{v_1, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (G.mapHomologicalComplex c).map (nullHomotopicMap hom) = nullHomotopicMap fun i j ↦ G.map (hom i j)

Tactic:
ext i

Goal state after:
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{v_1, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
i : ι
⊢ ((G.mapHomologicalComplex c).map (nullHomotopicMap hom)).f i = (nullHomotopicMap fun i j ↦ G.map (hom i j)).f i
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
⊢ (mappingCone φ).d i j ≫ (snd φ).v j j ⋯ = (↑(fst φ)).v i j hij ≫ φ.f j + (snd φ).v i i ⋯ ≫ G.d i j

Tactic:
dsimp [mappingCone, snd, fst]

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
⊢ homotopyCofiber.d φ i j ≫ (Cochain.ofHoms (homotopyCofiber.sndX φ)).v j j ⋯ =
    (↑(Cocycle.mk (Cochain.mk fun p q hpq ↦ homotopyCofiber.fstX φ p q hpq) 2 fst._proof_2 ⋯)).v i j hij ≫ φ.f j +
      (Cochain.ofHoms (homotopyCofiber.sndX φ)).v i i ⋯ ≫ G.d i j
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
i : ℕ
⊢ i + 1 = (ComplexShape.down ℕ).prev i

Tactic:
by simp only [ChainComplex.prev]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
H : ∀ (j : ι), ∃ i, c.Rel i j
⊢ mapArrowHom φ φ H (𝟙 (Arrow.mk φ)) = 𝟙 (homotopyCofiber φ)

Tactic:
ext i

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
H : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
⊢ (mapArrowHom φ φ H (𝟙 (Arrow.mk φ))).f i = (𝟙 (homotopyCofiber φ)).f i
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
⊢ ⟨(ConcreteCategory.hom s.ι) 0, ⋯⟩ = 0

Tactic:
by
          #adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
          this was just `cat_disch`. -/
          simp +instances only [HomComplex_X, map_zero]
          rfl

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
F' F'' G' G'' : HomologicalComplex C c
φ' : F' ⟶ G'
φ'' : F'' ⟶ G''
inst✝¹ : HasHomotopyCofiber φ'
inst✝ : HasHomotopyCofiber φ''
H : ∀ (j : ι), ∃ i, c.Rel i j
α : Arrow.mk φ ⟶ Arrow.mk φ'
β : Arrow.mk φ' ⟶ Arrow.mk φ''
⊢ mapArrowHom φ φ'' H (α ≫ β) = mapArrowHom φ φ' H α ≫ mapArrowHom φ' φ'' H β

Tactic:
ext i

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
F' F'' G' G'' : HomologicalComplex C c
φ' : F' ⟶ G'
φ'' : F'' ⟶ G''
inst✝¹ : HasHomotopyCofiber φ'
inst✝ : HasHomotopyCofiber φ''
H : ∀ (j : ι), ∃ i, c.Rel i j
α : Arrow.mk φ ⟶ Arrow.mk φ'
β : Arrow.mk φ' ⟶ Arrow.mk φ''
i : ι
⊢ (mapArrowHom φ φ'' H (α ≫ β)).f i = (mapArrowHom φ φ' H α ≫ mapArrowHom φ' φ'' H β).f i
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ nullHomotopicMap K = π K ≫ ι₀ K - 𝟙 K.cylinder

Tactic:
ext i

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case neg
ι✝ : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel i (c.next i)
⊢ K.d i (c.next i) ≫ (f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i)) = 0

Tactic:
K.shape _ _ h,

Goal state after:
case neg
ι✝ : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel i (c.next i)
⊢ 0 ≫ (f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i)) = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.inv ≫ (quotient V c).map f.hom = 𝟙 ((quotient V c).obj D)

Tactic:
by
    rw [← (quotient V c).map_comp, ← (quotient V c).map_id]
    exact eq_of_homotopy _ _ f.homotopyInvHomId

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

Goal state before:
pp: C : Type u_2
D : Type u_1
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
a b : A
X : C
⊢ (add F s i a b).inv.app (F.obj X) =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X

Tactic:
have h : whiskerLeft F (add F s i a b).inv = _ :=
    ((whiskeringLeft C D D).obj F).map_preimage _

Goal state after:
C : Type u_2
D : Type u_1
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
a b : A
X : C
h :
  F.whiskerLeft (add F s i a b).inv =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
            (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
              ((shiftFunctor C a).associator F (s b)).symm ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv
⊢ (add F s i a b).inv.app (F.obj X) =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
n : A
⊢ ∀ (X : D), (Induced.add F s i 0 n).hom.app X = eqToHom ⋯ ≫ (s n).map ((Induced.zero F s i).inv.app X)

Tactic:
suffices (Induced.add F s i 0 n).hom =
          eqToHom (by rw [zero_add]; rfl) ≫ whiskerRight (Induced.zero F s i).inv (s n) by
          intro X
          simpa using NatTrans.congr_app this X
        apply ((whiskeringLeft C D D).obj F).map_injective
        ext X
        have eq := dcongr_arg (fun a => (i a).hom.app X) (zero_add n)
        dsimp
        simp only [Induced.add_hom_app_obj, eq, shiftFunctorAdd_zero_add_hom_app,
          Functor.map_comp, eqToHom_map, Category.assoc, eqToHom_trans_assoc,
          eqToHom_refl, Category.id_comp, eqToHom_app, Induced.zero_inv_app_obj]
        erw [← NatTrans.naturality_assoc, Iso.hom_inv_id_app_assoc]
        rfl

Goal state after: