mathlib-initiative/mathlib-tactics huggingface dataset:
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
i j k : A
h : i + j = k
⊢ shiftFunctorComm C i j = (shiftFunctorAdd' C i j k h).symm ≪≫ shiftFunctorAdd' C j i k ⋯

Tactic:
subst h
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd]
  rfl

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

Goal state before:
pp: case mp
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 : S.ShortExact
i : ι
⊢ (S.map (eval C c i)).ShortExact

Tactic:
have := hS.mono_f

Goal state after:
case mp
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 : S.ShortExact
i : ι
this : Mono S.f
⊢ (S.map (eval C c i)).ShortExact
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x : S
this : ∀ x ∈ adjoin R ↑(EssFiniteType.finset R S), (D R S) x ∈ Submodule.span S ↑s
t : S
ht : t ∈ adjoin R ↑(EssFiniteType.finset R S)
ht' : IsUnit t
hxt : x * t ∈ adjoin R ↑(EssFiniteType.finset R S)
⊢ ht'.unit⁻¹ • ((D R S) (x * t) - x • (D R S) t) ∈ ↑(Submodule.span S ↑s)

Tactic:
exact Submodule.smul_mem _ _ (sub_mem (this _ hxt) (Submodule.smul_mem _ _ (this _ ht)))

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

Goal state before:
pp: case a.inl.inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S
⊢ (fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) (x, y) ∈ ↑(linearCombination S ⇑(D R S)).ker

pp: case a.inl.inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S
⊢ (fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) (x, y) ∈ ↑(linearCombination S ⇑(D R S)).ker

pp: case a.inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
⊢ (fun x ↦ single ((algebraMap R S) x) 1) x ∈ ↑(linearCombination S ⇑(D R S)).ker

Tactic:
<;>

Goal state after:
case a.inl.inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S
⊢ (fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) (x, y) ∈ ↑(linearCombination S ⇑(D R S)).ker

case a.inl.inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S
⊢ (fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) (x, y) ∈ ↑(linearCombination S ⇑(D R S)).ker

case a.inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
⊢ (fun x ↦ single ((algebraMap R S) x) 1) x ∈ ↑(linearCombination S ⇑(D R S)).ker
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: case neg
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 ⋯ ≫ K.homologyπ i = 0

Tactic:
have : liftCycles K k j hj (by rw [hx, assoc, K.d_comp_d, comp_zero]) = 0 := by
      rw [K.shape _ _ h, comp_zero] at hx
      rw [← cancel_mono (K.iCycles i), zero_comp, liftCycles_i, hx]
    rw [this, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F₁ F₂ : W.FunctorsInverting D
h : F₁.obj = F₂.obj
⊢ F₁ = F₂

Tactic:
cases F₁
  cases F₂
  subst h
  rfl

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

Goal state before:
pp: case succ.e_4.e_a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1

pp: case succ.e_6.e_8
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1

pp: case succ.e_7.e_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1

Tactic:
<;>

Goal state after:
case succ.e_4.e_a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1

case succ.e_6.e_8
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1

case succ.e_7.e_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case succ.e_4.e_a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1

pp: case succ.e_6.e_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1

pp: case succ.e_7.e_7
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1

Tactic:
<;>

Goal state after:
case succ.e_4.e_a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1

case succ.e_6.e_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1

case succ.e_7.e_7
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos
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 : ι
hi : c.Rel i (c.next i)
⊢ (biprod.inr ≫ (XIsoBiprod φ i (c.next i) hi).inv) ≫ (XIsoBiprod φ i (c.next i) hi).hom ≫ biprod.snd = 𝟙 (G.X i)

pp: case neg
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 : ι
hi : ¬c.Rel i (c.next i)
⊢ (XIso φ i hi).inv ≫ (XIso φ i hi).hom = 𝟙 (G.X i)

Tactic:
<;>

Goal state after:
case pos
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 : ι
hi : c.Rel i (c.next i)
⊢ (biprod.inr ≫ (XIsoBiprod φ i (c.next i) hi).inv) ≫ (XIsoBiprod φ i (c.next i) hi).hom ≫ biprod.snd = 𝟙 (G.X i)

case neg
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 : ι
hi : ¬c.Rel i (c.next i)
⊢ (XIso φ i hi).inv ≫ (XIso φ i hi).hom = 𝟙 (G.X i)
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✝ : ι
f g : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i : ι
⊢ e.f i ≫ ((dNext i) h.hom + (prevD i) h.hom + g.f i) =
    e.f i ≫ (dNext i) h.hom + e.f i ≫ (prevD i) h.hom + e.f i ≫ g.f i

Tactic:
Preadditive.comp_add,

Goal state after:
ι : 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✝ : ι
f g : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i : ι
⊢ e.f i ≫ ((dNext i) h.hom + (prevD i) h.hom) + e.f i ≫ g.f i =
    e.f i ≫ (dNext i) h.hom + e.f i ≫ (prevD i) h.hom + e.f i ≫ g.f i
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✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 : (prevD i) hom ≫ D.d i j = 0
eq2 : C.d i j ≫ (dNext j) hom = 0
⊢ (C.d i j ≫ hom j i + (prevD i) hom) ≫ D.d i j = C.d i j ≫ ((dNext j) hom + hom j i ≫ D.d i j)

Tactic:
Preadditive.comp_add,

Goal state after:
ι : 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✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 : (prevD i) hom ≫ D.d i j = 0
eq2 : C.d i j ≫ (dNext j) hom = 0
⊢ (C.d i j ≫ hom j i + (prevD i) hom) ≫ D.d i j = C.d i j ≫ (dNext j) hom + C.d i j ≫ hom j i ≫ D.d i j
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos
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 i j
hij : c.Rel j (c.next j)
⊢ (-fstX φ i j hij✝ ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hij + fstX φ i j hij✝ ≫ φ.f j ≫ inrX φ j +
        sndX φ i ≫ G.d i j ≫ inrX φ j) ≫
      sndX φ j =
    fstX φ i j hij✝ ≫ φ.f j + sndX φ i ≫ G.d i j

pp: case neg
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 i j
hij : ¬c.Rel j (c.next j)
⊢ (0 + fstX φ i j hij✝ ≫ φ.f j ≫ inrX φ j + sndX φ i ≫ G.d i j ≫ inrX φ j) ≫ sndX φ j =
    fstX φ i j hij✝ ≫ φ.f j + sndX φ i ≫ G.d i j

Tactic:
<;>

Goal state after:
case pos
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 i j
hij : c.Rel j (c.next j)
⊢ (-fstX φ i j hij✝ ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hij + fstX φ i j hij✝ ≫ φ.f j ≫ inrX φ j +
        sndX φ i ≫ G.d i j ≫ inrX φ j) ≫
      sndX φ j =
    fstX φ i j hij✝ ≫ φ.f j + sndX φ i ≫ G.d i j

case neg
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 i j
hij : ¬c.Rel j (c.next j)
⊢ (0 + fstX φ i j hij✝ ≫ φ.f j ≫ inrX φ j + sndX φ i ≫ G.d i j ≫ inrX φ j) ≫ sndX φ j =
    fstX φ i j hij✝ ≫ φ.f j + sndX φ i ≫ G.d i j
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 φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ (inl φ).comp ((↑(fst φ)).comp γ he) ⋯ = γ

Tactic:
rw [← Cochain.comp_assoc _ _ _ (neg_add_cancel 1) (by lia) (by lia), inl_fst,
    Cochain.id_comp]

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

Goal state before:
pp: case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₀) k₀

pp: case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)

Tactic:
<;>

Goal state after:
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₀) k₀

case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

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

pp: case h₂
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
⊢ f ≫ (snd φ).v i i ⋯ =
    ((f ≫ (↑(fst φ)).v i j hij) ≫ (inl φ).v j i ⋯ + (f ≫ (snd φ).v i i ⋯) ≫ (inr φ).f i) ≫ (snd φ).v i i ⋯

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
⊢ f ≫ (↑(fst φ)).v i j hij =
    ((f ≫ (↑(fst φ)).v i j hij) ≫ (inl φ).v j i ⋯ + (f ≫ (snd φ).v i i ⋯) ≫ (inr φ).f i) ≫ (↑(fst φ)).v i j hij

case h₂
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
⊢ f ≫ (snd φ).v i i ⋯ =
    ((f ≫ (↑(fst φ)).v i j hij) ≫ (inl φ).v j i ⋯ + (f ≫ (snd φ).v i i ⋯) ≫ (inr φ).f i) ≫ (snd φ).v i i ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

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

pp: case h₂
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
j : ℤ
A : C
f : (mappingCone φ).X j ⟶ A
i : ℤ
hij : j + 1 = i
⊢ (inr φ).f j ≫ f = (inr φ).f j ≫ ((↑(fst φ)).v j i hij ≫ (inl φ).v i j ⋯ ≫ f + (snd φ).v j j ⋯ ≫ (inr φ).f j ≫ f)

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
j : ℤ
A : C
f : (mappingCone φ).X j ⟶ A
i : ℤ
hij : j + 1 = i
⊢ (inl φ).v i j ⋯ ≫ f =
    (inl φ).v i j ⋯ ≫ ((↑(fst φ)).v j i hij ≫ (inl φ).v i j ⋯ ≫ f + (snd φ).v j j ⋯ ≫ (inr φ).f j ≫ f)

case h₂
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
j : ℤ
A : C
f : (mappingCone φ).X j ⟶ A
i : ℤ
hij : j + 1 = i
⊢ (inr φ).f j ≫ f = (inr φ).f j ≫ ((↑(fst φ)).v j i hij ≫ (inl φ).v i j ⋯ ≫ f + (snd φ).v j j ⋯ ≫ (inr φ).f j ≫ f)
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i : ι
h✝ : c.Rel i (c.next i)
⊢ inrX φ i ≫ (fstX φ i (c.next i) h✝ ≫ hα.hom (c.next i) i + sndX φ i ≫ α.f i) = α.f i

pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i : ι
h✝ : ¬c.Rel i (c.next i)
⊢ inrX φ i ≫ sndX φ i ≫ α.f i = α.f i

Tactic:
<;>

Goal state after:
case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i : ι
h✝ : c.Rel i (c.next i)
⊢ inrX φ i ≫ (fstX φ i (c.next i) h✝ ≫ hα.hom (c.next i) i + sndX φ i ≫ α.f i) = α.f i

case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i : ι
h✝ : ¬c.Rel i (c.next i)
⊢ inrX φ i ≫ sndX φ i ≫ α.f i = α.f i
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : ¬n + 1 = m
⊢ δ n m ↑z = 0

Tactic:
· exact δ_shape n m h _

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: case e'_3
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f✝ : X ⟶ Y
f g : X.as ⟶ Y.as
hfg : r f g
⊢ -g = f + (-f - g)

pp: case e'_4
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f✝ : X ⟶ Y
f g : X.as ⟶ Y.as
hfg : r f g
⊢ -f = g + (-f - g)

Tactic:
<;>

Goal state after:
case e'_3
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f✝ : X ⟶ Y
f g : X.as ⟶ Y.as
hfg : r f g
⊢ -g = f + (-f - g)

case e'_4
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f✝ : X ⟶ Y
f g : X.as ⟶ Y.as
hfg : r f g
⊢ -f = g + (-f - g)
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 ι
W : Type u_3
inst✝⁴ : Category.{v_1, u_3} W
inst✝³ : Preadditive W
F : V ⥤ W
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : F.Additive
⊢ ∀ {X Y : HomotopyCategory V c}, Function.Surjective (F.mapHomotopyCategory c).map

Tactic:
rintro ⟨K⟩ ⟨L⟩ ⟨f⟩

Goal state after:
case mk
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
W : Type u_3
inst✝⁴ : Category.{v_1, u_3} W
inst✝³ : Preadditive W
F : V ⥤ W
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : F.Additive
K L : HomologicalComplex V c
b✝ : (F.mapHomotopyCategory c).obj { as := K } ⟶ (F.mapHomotopyCategory c).obj { as := L }
f : ((F.mapHomotopyCategory c).obj { as := K }).as ⟶ ((F.mapHomotopyCategory c).obj { as := L }).as
⊢ ∃ a, (F.mapHomotopyCategory c).map a = Quot.mk (HomRel.CompClosure (homotopic W c)) f
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type u_3
D : Type u_1
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_2
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
X : C
h :
  F.whiskerLeft (zero F s i).hom =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom
⊢ (zero F s i).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Tactic:
exact (NatTrans.congr_app h X).trans (by simp)

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
X : C
h :
  F.whiskerLeft (zero F s i).inv =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv
⊢ (zero F s i).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Tactic:
exact (NatTrans.congr_app h X).trans (by simp)

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

Goal state before:
pp: C : Type u_3
D : Type u_1
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_2
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).hom =
    (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)).hom
⊢ (add F s i a b).hom.app (F.obj X) =
    (i (a + b)).hom.app X ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X)

Tactic:
exact (NatTrans.congr_app h X).trans (by simp)

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
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

Tactic:
exact (NatTrans.congr_app h X).trans (by simp)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
⊢ (-γ).shift a = -γ.shift a

Tactic:
change shiftAddHom K L n a (-γ) = _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
⊢ (shiftAddHom K L n a) (-γ) = -γ.shift a