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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ : ι
h : p₁ = p₂
p₃ : ι
⊢ (K.XIsoOfEq h).hom ≫ K.d p₂ p₃ = K.d p₁ p₃

Tactic:
by subst h; simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₁ : ι
h : p₂ = p₁
p₃ : ι
⊢ (K.XIsoOfEq h).inv ≫ K.d p₂ p₃ = K.d p₁ p₃

Tactic:
by subst h; simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
h : p₂ = p₃
p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq h).hom = K.d p₁ p₃

Tactic:
by subst h; simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
h : p₃ = p₂
p₁ : ι
⊢ K.d p₁ p₂ ≫ (K.XIsoOfEq h).inv = K.d p₁ p₃

Tactic:
by subst h; simp

Goal state after:
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
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)

Tactic:
simp_rw [smul_sub, TensorProduct.smul_tmul', smul_eq_mul, mul_one]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n n' : ι
h : n = n'
⊢ φ.f n ≫ (L.XIsoOfEq h).hom = (K.XIsoOfEq h).hom ≫ φ.f n'

Tactic:
by subst h; simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n n' : ι
h : n = n'
⊢ φ.f n' ≫ (L.XIsoOfEq h).inv = (K.XIsoOfEq h).inv ≫ φ.f n

Tactic:
by subst h; simp

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

Goal state before:
pp: case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ ∀ (j_1 : ι), ¬c.Rel j_1 j

Tactic:
intro i hi

Goal state after:
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬c.Rel (c.prev j) j
i : ι
hi : c.Rel i j
⊢ False
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.Exact
i : ι
⊢ (S.map (eval C c i)).Exact

Tactic:
exact hS.map (eval C c i)

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 : ι
this✝ : Mono S.f
this : Epi S.g
⊢ (S.map (eval C c i)).ShortExact

Tactic:
exact hS.map (eval C c i)

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

Goal state before:
pp: case refine_4
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✝ x : S
hx : x ∈ adjoin R ↑(EssFiniteType.finset R S)
⊢ ∀ (x y : S),
    x ∈ adjoin R ↑(EssFiniteType.finset R S) →
      y ∈ adjoin R ↑(EssFiniteType.finset R S) →
        (D R S) x ∈ Submodule.span S ↑s → (D R S) y ∈ Submodule.span S ↑s → (D R S) (x * y) ∈ Submodule.span S ↑s

Tactic:
· intro x y _ _ hx hy
      simp only [Derivation.leibniz]
      exact add_mem (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hx)

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

Tactic:
← (KaehlerDifferential.kerTotal R S).ker_mkQ

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
| (kerTotal R S).mkQ.ker
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case succ
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✝ : ℕ
⊢ C.d (n✝ + 1) ((ComplexShape.down ℕ).next (n✝ + 1)) ≫ f ((ComplexShape.down ℕ).next (n✝ + 1)) (n✝ + 1) =
    C.d (n✝ + 1) (n✝ + 1 - 1) ≫ f (n✝ + 1 - 1) (n✝ + 1)

Tactic:
congr <;> simp

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

Goal state before:
pp: case succ
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✝ : ℕ
⊢ f (n✝ + 1) ((ComplexShape.up ℕ).prev (n✝ + 1)) ≫ D.d ((ComplexShape.up ℕ).prev (n✝ + 1)) (n✝ + 1) =
    f (n✝ + 1) (n✝ + 1 - 1) ≫ D.d (n✝ + 1 - 1) (n✝ + 1)

Tactic:
congr <;> simp

Goal state after:
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 : ι
hij : c.Rel j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
this : HasBinaryBiproduct (F.X i) (G.X j)
⊢ biprod.inl ≫ (XIsoBiprod φ j i hij).inv ≫ f = biprod.inl ≫ (XIsoBiprod φ j i hij).inv ≫ g

Tactic:
simpa

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v, u_1} C
inst✝³ : Category.{v', u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ 1 + m = m + 1

Tactic:
add_comm

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v, u_1} C
inst✝³ : Category.{v', u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ m + 1 = m + 1
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 ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
⊢ Cochain.ofHom (desc φ α β eq) = descCochain φ α (Cochain.ofHom β) ⋯

Tactic:
by
  simp [desc]

Goal state after:
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 ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
p q : ℤ
h : p + -1 = q
⊢ (inl φ).v p q h ≫ (desc φ α β eq).f q = α.v p q h

Tactic:
by
  simp [desc]

Goal state after:
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 ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
p : ℤ
⊢ (inr φ).f p ≫ (desc φ α β eq).f p = β.f p

Tactic:
by
  simp [desc]

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 E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ e.f i =
    (dFrom P i ≫
        (fromNext i) fun i j ↦
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0) +
      ((toPrev i) fun i j ↦
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0) ≫
        dTo Q i

Tactic:
add_comm

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✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ e.f i =
    ((toPrev i) fun i j ↦
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0) ≫
        dTo Q i +
      dFrom P i ≫
        (fromNext i) fun i j ↦
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
h : q = q'' - 1
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
subst h
        obtain rfl : q' = q'' := by lia
        simp only [single_v]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n m : ℤ
hnm : n + 1 = m
⊢ mapHomologicalComplexXIso φ H n = mapHomologicalComplexXIso' φ H n m hnm

Tactic:
by
  subst hnm
  rfl

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

Goal state before:
pp: case pos.h₀
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
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inl ≫ (K.biprodXIso K j).inv ≫ ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K j)

pp: case h₁
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
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inr ≫ (K.biprodXIso K j).inv ≫ ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K j)

Tactic:
· simp [ι₀]

Goal state after:
case h₁
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
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inr ≫ (K.biprodXIso K j).inv ≫ ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K 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 : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
f : X✝ ⟶ Y✝
g : HomotopyEquiv Y✝ Z✝
e : HomotopyEquiv X✝ Z✝
he : e.hom = f ≫ g.hom
⊢ Homotopy (f ≫ g.hom ≫ g.inv) f

Tactic:
exact g.homotopyHomInvId.compLeftId f

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
a b e : C
f : a ⟶ b
X Y c d : C
h₁ h₂ : c ⟶ d
h : r h₁ h₂
g : b ⟶ c
i : d ⟶ e
⊢ CompClosure r (f ≫ g ≫ h₁ ≫ i) (f ≫ g ≫ h₂ ≫ i)

Tactic:
simpa using CompClosure.intro _ _ (f ≫ g) _ _ i h

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: case h_map
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
x✝ : X✝.as ⟶ Y✝.as
⊢ Φ.map (Quot.mk (HomRel.CompClosure r) x✝) ≍
    (Quot.mk (HomRel.CompClosure r) x✝).liftOn (fun f ↦ Φ.map ((functor r).map f)) ⋯

Tactic:
simp only [heq_eq_eq]

Goal state after:
case h_map
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
x✝ : X✝.as ⟶ Y✝.as
⊢ Φ.map (Quot.mk (HomRel.CompClosure r) x✝) =
    (Quot.mk (HomRel.CompClosure r) x✝).liftOn (fun f ↦ Φ.map ((functor r).map f)) ⋯
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.Full
X Y : C
f : X ⟶ Y
⊢ ∃ a, (Quotient.lift L.homRel L ⋯).map a = L.map f

Tactic:
exact ⟨(Quotient.functor _).map f, rfl⟩

Goal state after:
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 ι
⊢ ∀ ⦃X Y : HomologicalComplex V c⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y),
    homotopic V c f₁ f₂ → homotopic V c g₁ g₂ → homotopic V c (f₁ + g₁) (f₂ + g₂)

Tactic:
by
    rintro _ _ _ _ _ _ ⟨h⟩ ⟨h'⟩
    exact ⟨Homotopy.add h h'⟩

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
n : ℤ
X Y : HomologicalComplex C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
h₁ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ)).map f ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map f
⊢ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map (r • (quotient C (ComplexShape.up ℤ)).map f) =
    r • (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map f)

Tactic:
have h₂ := NatIso.naturality_1 ((HomotopyCategory.quotient _ _).commShiftIso n) (r • f)

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
n : ℤ
X Y : HomologicalComplex C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
h₁ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ)).map f ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map f
h₂ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ)).map (r • f) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map (r • f)
⊢ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map (r • (quotient C (ComplexShape.up ℤ)).map f) =
    r • (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map f)
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 A.obj₃

Tactic:
by rw [← comp_hom₃, e.hom_inv_id, id_hom₃]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Rotate

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
X : C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
⊢ (invRotate C).IsEquivalence

Tactic:
change (triangleRotation C).inverse.IsEquivalence
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
⊢ ∃ Y f g, Triangle.mk f g h ∈ distinguishedTriangles

Tactic:
let T' := (Triangle.mk h f' g').invRotate.invRotate

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
Z X : C
h : Z ⟶ (shiftFunctor C 1).obj X
Y' : C
f' : (shiftFunctor C 1).obj X ⟶ Y'
g' : Y' ⟶ (shiftFunctor C 1).obj Z
mem : Triangle.mk h f' g' ∈ distinguishedTriangles
T' : Triangle C := (Triangle.mk h f' g').invRotate.invRotate
⊢ ∃ Y f g, Triangle.mk f g h ∈ distinguishedTriangles
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₁ ≫
      (n.negOnePow • Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₂).hom =
    (Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₁).hom ≫
      (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₁

pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₂ ≫ (shiftIso φ n).hom =
    (n.negOnePow • Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₂).hom ≫
      (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₂

pp: case refine_3
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₃ ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map
        (Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₁).hom =
    (shiftIso φ n).hom ≫ (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₃

Tactic:
· dsimp
    simp only [Linear.comp_units_smul, comp_id, id_comp, smul_smul,
      Int.units_mul_self, one_smul]

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₂ ≫ (shiftIso φ n).hom =
    (n.negOnePow • Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₂).hom ≫
      (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₂

case refine_3
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₃ ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map
        (Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₁).hom =
    (shiftIso φ n).hom ≫ (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₃
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ (G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ) ≅
    triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)

Tactic:
by
  refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (mapHomologicalComplexIso φ G) ?_ ?_ ?_
  · dsimp
    simp only [comp_id, id_comp]
  · dsimp
    rw [map_inr, id_comp]
  · dsimp
    simp only [CategoryTheory.Functor.map_id, comp_id, map_δ]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Functor

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
inst✝⁶ : HasShift C ℤ
inst✝⁵ : HasShift D ℤ
inst✝⁴ : HasShift E ℤ
F : C ⥤ D
inst✝³ : F.CommShift ℤ
G : D ⥤ E
inst✝² : G.CommShift ℤ
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : Triangle C
f : F.mapTriangle.obj X ⟶ F.mapTriangle.obj Y
⊢ F.map (X.mor₃ ≫ (shiftFunctor C 1).map (F.preimage f.hom₁)) = F.map (F.preimage f.hom₃ ≫ Y.mor₃)

Tactic:
rw [← cancel_mono ((F.commShiftIso (1 : ℤ)).hom.app Y.obj₁)]

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
inst✝⁶ : HasShift C ℤ
inst✝⁵ : HasShift D ℤ
inst✝⁴ : HasShift E ℤ
F : C ⥤ D
inst✝³ : F.CommShift ℤ
G : D ⥤ E
inst✝² : G.CommShift ℤ
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : Triangle C
f : F.mapTriangle.obj X ⟶ F.mapTriangle.obj Y
⊢ F.map (X.mor₃ ≫ (shiftFunctor C 1).map (F.preimage f.hom₁)) ≫ (commShiftIso F 1).hom.app Y.obj₁ =
    F.map (F.preimage f.hom₃ ≫ Y.mor₃) ≫ (commShiftIso F 1).hom.app Y.obj₁