mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ Submodule.span S (Set.range ⇑(D R S)) ≤ Submodule.span S ↑s

Tactic:
Submodule.span_le

Goal state after:
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)
⊢ Set.range ⇑(D R S) ⊆ ↑(Submodule.span S ↑s)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this : (i (0 + n)).hom.app X = eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯
⊢ F.map ((add hF s i 0 n).hom.app X) = F.map (eqToHom ⋯ ≫ (s n).map ((zero hF s i).inv.app X))

Tactic:
← cancel_mono ((i n).hom.app ((s 0).obj X))

Goal state after:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this : (i (0 + n)).hom.app X = eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯
⊢ F.map ((add hF s i 0 n).hom.app X) ≫ (i n).hom.app ((s 0).obj X) =
    F.map (eqToHom ⋯ ≫ (s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.span S
      (((Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
          Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
        Set.range fun x ↦ single ((algebraMap R S) x) 1) ≤
    (linearCombination S ⇑(D R S)).ker

Tactic:
Submodule.span_le

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (((Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
        Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
      Set.range fun x ↦ single ((algebraMap R S) x) 1) ⊆
    ↑(linearCombination S ⇑(D R S)).ker
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
⊢ Function.Surjective ⇑(linearCombination S ⇑(D R S))

Tactic:
rw [← LinearMap.range_eq_top, range_linearCombination, span_range_derivation]

Goal state after:
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
hk : K.d j i ≫ k = 0
⊢ K.pOpcycles i ≫ K.descOpcycles k j hj hk = k

Tactic:
by
  dsimp [descOpcycles, pOpcycles]
  simp

Goal state after:
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 L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map φ ≫ (shortComplexFunctor C c i).map ψ) =
    ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map ψ)

Tactic:
ShortComplex.opcyclesMap_comp

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map ψ) =
    ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map ψ)
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

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
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap (φ + ψ) i = homologyMap φ i + homologyMap ψ i

Tactic:
dsimp [homologyMap]
  rw [← ShortComplex.homologyMap_add]
  rfl

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
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A (Set.range ⇑(D S B)) ≤ (map R S A B).range

Tactic:
Submodule.span_le

Goal state after:
R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Set.range ⇑(D S B) ⊆ ↑(map R S A B).range
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.convert_2
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.span B
      (((Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
          Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
        Set.range fun x ↦ single ((algebraMap A B) x) 1) ≤
    Submodule.comap (linearCombination B ⇑(D R B)) (mapBaseChange R A B).range

Tactic:
Submodule.span_le

Goal state after:
case a.convert_2
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
⊢ (((Set.range fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∪
        Set.range fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∪
      Set.range fun x ↦ single ((algebraMap A B) x) 1) ⊆
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (mapBaseChange R A B).range)
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
L : C ⥤ D
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
⊢ IsIso (L.op.map f)

Tactic:
have := h f.unop hf
  dsimp
  infer_instance

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
L : C ⥤ Dᵒᵖ
h : W.IsInvertedBy L
X Y : Cᵒᵖ
f : X ⟶ Y
hf : W.op f
⊢ IsIso (L.leftOp.map f)

Tactic:
have := h f.unop hf
  dsimp
  infer_instance

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
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ C.d i (c.next i) ≫ f (c.next i) i = 0

Tactic:
rw [shape _ _ _ hi, zero_comp]

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
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
⊢ f = g

Tactic:
by
  have := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
  rw [← cancel_epi (XIsoBiprod φ j i hij).inv]
  apply biprod.hom_ext'
  · simpa
  · obtain rfl := c.next_eq' hij
    simpa [-inr_XIsoBiprod_inv, -inr_XIsoBiprod_inv_assoc, inrX, dif_pos hij] using h₂

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 : C ⟶ D
hom : (i j : ι) → D.X i ⟶ E.X j
⊢ f ≫ nullHomotopicMap hom = nullHomotopicMap fun i j ↦ f.f i ≫ hom i j

Tactic:
by
  ext n
  dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]
  simp only [Preadditive.comp_add, assoc, f.comm_assoc]

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 : ι
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ Homotopy (nullHomotopicMap' h) 0

Tactic:
by
  apply nullHomotopy fun i j => dite (c.Rel j i) (h i j) fun _ => 0
  grind

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

Goal state before:
pp: case e_a.e_a
ι : 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 : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (toPrev i) fun i j ↦
      if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom else 0

Tactic:
dsimp [toPrev]
      rw [dif_pos (by simp only [ChainComplex.prev])]
      simp [xPrevIso, comp_id]

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
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
⊢ (H.mapHomologicalComplex c).map (inr φ) ≫ (mapHomologicalComplexObjIso φ H).hom =
    inr ((H.mapHomologicalComplex c).map φ)

Tactic:
ext
  simp [mapHomologicalComplexObjIso]

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
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ ∀ {X Y Z : Quotient r} (f : X ⟶ Y) (g : Y ⟶ Z),
    Quot.liftOn (f ≫ g) (fun f ↦ F.map f) ⋯ = Quot.liftOn f (fun f ↦ F.map f) ⋯ ≫ Quot.liftOn g (fun f ↦ F.map f) ⋯

Tactic:
by
    rintro a b c ⟨f⟩ ⟨g⟩
    exact F.map_comp f g

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
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
Φ : Quotient r ⥤ D
hΦ : functor r ⋙ Φ = F
⊢ Φ = lift r F H

Tactic:
by
  subst_vars
  fapply Functor.hext
  · rintro X
    dsimp [lift, Functor]
    congr
  · rintro _ _ f
    dsimp [lift, Functor]
    refine Quot.inductionOn f fun _ ↦ ?_
    simp only [heq_eq_eq]
    congr

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

Goal state before:
pp: 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₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
⊢ ∀ (a : P ⟶ Q), 0 + a = a

Tactic:
rintro ⟨_⟩

Goal state after:
case mk
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₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝¹ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ 0 + Quot.mk (HomRel.CompClosure r) a✝ = Quot.mk (HomRel.CompClosure r) a✝
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: 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₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
⊢ ∀ (a : P ⟶ Q), a + 0 = a

Tactic:
rintro ⟨_⟩

Goal state after:
case mk
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₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝¹ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ Quot.mk (HomRel.CompClosure r) a✝ + 0 = Quot.mk (HomRel.CompClosure r) a✝
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: 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₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
⊢ ∀ (a : P ⟶ Q), -a + a = 0

Tactic:
rintro ⟨_⟩

Goal state after:
case mk
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₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
a✝¹ : P ⟶ Q
a✝ : P.as ⟶ Q.as
⊢ -Quot.mk (HomRel.CompClosure r) a✝ + Quot.mk (HomRel.CompClosure r) a✝ = 0
Module: Mathlib.CategoryTheory.Shift.CommShift

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
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
X : C
this :
  (shiftFunctor C c ⋙ F).map ((shiftFunctorAdd' C a b ab hab).app X).hom ≫
      ec.hom.app ((shiftFunctor C a ⋙ shiftFunctor C b).obj X) ≫
        (F ⋙ shiftFunctor D c).map ((shiftFunctorAdd' C a b ab hab).app X).inv =
    ec.hom.app ((shiftFunctor C ab).obj X)
⊢ (isoAdd' ⋯ (isoAdd' hab ea eb) ec).hom.app X = (isoAdd' ⋯ ea (isoAdd' hbc eb ec)).hom.app X

Tactic:
dsimp at this ⊢

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
X : C
this :
  F.map ((shiftFunctor C c).map ((shiftFunctorAdd' C a b ab hab).hom.app X)) ≫
      ec.hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        (shiftFunctor D c).map (F.map ((shiftFunctorAdd' C a b ab hab).inv.app X)) =
    ec.hom.app ((shiftFunctor C ab).obj X)
⊢ (isoAdd' ⋯ (isoAdd' hab ea eb) ec).hom.app X = (isoAdd' ⋯ ea (isoAdd' hbc eb ec)).hom.app X
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

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
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : R
⊢ (x • γ).shift a = x • γ.shift a

Tactic:
by
  ext p q hpq
  dsimp
  simp only [shift_v', smul_v]

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

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
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : F₁.CommShift A
inst✝ : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
X : C
this :
  (shiftFunctor D a ⋙ shiftFunctor D b).map (τ.app X) ≫ (shiftFunctorAdd D a b).inv.app (F₂.obj X) =
    (shiftFunctorAdd D a b).inv.app (F₁.obj X) ≫ (shiftFunctor D (a + b)).map (τ.app X)
⊢ ((Functor.commShiftIso F₁ (a + b)).hom ≫ Functor.whiskerRight τ (shiftFunctor D (a + b))).app X =
    ((shiftFunctor C (a + b)).whiskerLeft τ ≫ (Functor.commShiftIso F₂ (a + b)).hom).app X

Tactic:
dsimp at this ⊢

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : F₁.CommShift A
inst✝ : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
X : C
this :
  (shiftFunctor D b).map ((shiftFunctor D a).map (τ.app X)) ≫ (shiftFunctorAdd D a b).inv.app (F₂.obj X) =
    (shiftFunctorAdd D a b).inv.app (F₁.obj X) ≫ (shiftFunctor D (a + b)).map (τ.app X)
⊢ (Functor.commShiftIso F₁ (a + b)).hom.app X ≫ (shiftFunctor D (a + b)).map (τ.app X) =
    τ.app ((shiftFunctor C (a + b)).obj X) ≫ (Functor.commShiftIso F₂ (a + b)).hom.app X
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (rotateHomotopyEquiv φ).hom ≫ (triangle (inr φ)).mor₃ = -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ

Tactic:
by
  ext p
  dsimp [rotateHomotopyEquiv]
  -- the following list of lemmas has been obtained by doing
  -- simp? [lift_f _ _ _ _ _ (p + 1) rfl,
  --   (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by lia)]
  simp only [Int.reduceNeg, lift_f _ _ _ _ _ (p + 1) rfl, shiftFunctor_obj_X', Cocycle.coe_neg,
    Cocycle.leftShift_coe, Cocycle.ofHom_coe, Cochain.neg_v,
    (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by lia), mul_one,
      sub_self, mul_zero, Int.zero_ediv, add_zero, Int.negOnePow_one,
    shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, Cochain.ofHom_v, id_comp,
    Units.neg_smul, one_smul, neg_neg, Preadditive.neg_comp, Preadditive.add_comp, assoc,
    inl_v_triangle_mor₃_f, Iso.refl_inv, Preadditive.comp_neg, comp_id, inr_f_triangle_mor₃_f,
    comp_zero, neg_zero]

Goal state after:
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
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
G : C ⥤ D
inst✝ : G.Additive
⊢ ∀ T ∈ distinguishedTriangles, (G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.obj T ∈ distinguishedTriangles

Tactic:
by
    rintro T ⟨K, L, f, ⟨e⟩⟩
    exact ⟨_, _, _, ⟨(G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.mapIso e ≪≫
      CochainComplex.mappingCone.mapTrianglehIso f G⟩⟩

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
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = e₃.hom ≫ T₂.mor₃
this :
  (shiftFunctor C 1 ⋙ shiftFunctor C (-1)).map e₁.hom ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₂.obj₁ =
    (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₁.obj₁ ≫ (𝟭 C).map e₁.hom
⊢ ((shiftFunctor C (-1)).mapIso e₃).hom ≫ (Arrow.mk T₂.invRotate.mor₁).hom = (Arrow.mk T₁.invRotate.mor₁).hom ≫ e₁.hom

Tactic:
dsimp at this ⊢

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
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = e₃.hom ≫ T₂.mor₃
this :
  (shiftFunctor C (-1)).map ((shiftFunctor C 1).map e₁.hom) ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₂.obj₁ =
    (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₁.obj₁ ≫ e₁.hom
⊢ (shiftFunctor C (-1)).map e₃.hom ≫
      (-(shiftFunctor C (-1)).map T₂.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₂.obj₁) =
    (-(shiftFunctor C (-1)).map T₁.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₁.obj₁) ≫ e₁.hom
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} A
F : C ⥤ A
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso mn a a'' ⋯).hom.app X =
    (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).hom.app X) ≫
      (F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X

Tactic:
by
  simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} A
F : C ⥤ A
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso mn a a'' ⋯).inv.app X =
    (F.shiftIso m a' a'' ha'').inv.app X ≫
      (F.shiftIso n a a' ha').inv.app ((shiftFunctor C m).obj X) ≫
        (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).inv.app X)

Tactic:
by
  simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']

Goal state after: