mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case a
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ p ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
p.as_sum_support

Goal state after:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ ∑ i ∈ p.support, (monomial i) (p.coeff i) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ ∀ x ∈ p.support, (monomial x) (p.coeff x) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
rintro i -

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
i : ℕ
⊢ (monomial i) (p.coeff i) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
⊢ Disjoint (torsionBySet R M ↑P) (torsionBySet R M ↑Q)

Tactic:
let map : Fin 2 → Ideal R | 0 => P | 1 => Q
  have heq := Submodule.supIndep_torsionBySet_ideal (p := map) (M := M) (S := ⊤) ?_
  · simpa [Finset.top_eq_univ, Fin.isValue, map] using heq
  · aesop (add norm [Fin.univ_succ, Set.pairwise_pair, map, sup_comm])

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : a • (mk (R ∙ a * b)) x = 0
⊢ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x

Tactic:
← mk_eq_mk,

Goal state after:
case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : a • Submodule.Quotient.mk x = 0
⊢ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case h
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c * b = x
⊢ c • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) (c * b)

Tactic:
← mk_eq_mk,

Goal state after:
case h
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c * b = x
⊢ c • Submodule.Quotient.mk b = (mk (R ∙ a * b)) (c * b)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case mpr
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
⊢ c • a • (mk (R ∙ a * b)) b = 0

Tactic:
← mk_eq_mk,

Goal state after:
case mpr
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
⊢ c • a • Submodule.Quotient.mk b = 0
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
⊢ F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

Tactic:
← submodule_span_single,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
⊢ Submodule.span (↥(reesAlgebra I)) (⋃ i, single R i '' ↑(F.N i)) =
      Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Submodule.map (Submodule.subtype I) I.toCotangent.ker = I ^ 2

Tactic:
rw [Ideal.toCotangent, Submodule.ker_mkQ, pow_two, Submodule.map_smul'' I ⊤ (Submodule.subtype I),
    smul_eq_mul, Submodule.map_subtype_top]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddRightCancelSemigroup α
inst✝ : DecidableEq α
a x✝¹ x✝ : α
⊢ Decidable ((up' a).Rel x✝¹ x✝)

Tactic:
by dsimp; infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
f : unit R ⟶ M
X : Cᵒᵖ
⊢ ModuleCat.Hom.hom
      (((fun s ↦
              { app := fun X ↦ ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj X) ℤ ↑(M.obj X)).symm (↑s X)),
                naturality := ⋯ })
            ((fun f ↦ sectionsMk (fun X ↦ (ConcreteCategory.hom (f.app X)) 1) ⋯) f)).app
        X) =
    ModuleCat.Hom.hom (f.app X)

Tactic:
exact (LinearMap.ringLmapEquivSelf (R.obj X) ℤ (M.obj X)).symm_apply_apply (f.app X).hom

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

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i ≠ j
⊢ IsZero (if i = j then A else 0)

Tactic:
if_neg hi

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i ≠ j
⊢ IsZero 0
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.add n 0).inv.app X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯

Tactic:
← cancel_epi ((h.add n 0).hom.app X),

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.add n 0).hom.app X ≫ (h.add n 0).inv.app X = (h.add n 0).hom.app X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorCompIsoId C n m h).inv.app X) =
    (shiftFunctorCompIsoId C m n ⋯).inv.app ((shiftFunctor C n).obj X)

Tactic:
rw [← cancel_mono (((shiftFunctorCompIsoId C n m h).hom.app X)⟦n⟧'),
    ← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id,
    shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_id_app]
  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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : S
⊢ ((TensorProduct.lmul' R).comp TensorProduct.includeLeft) x = x

Tactic:
TensorProduct.lmul'_comp_includeLeft

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
x : S
⊢ (AlgHom.id R S) x = x
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 Y : C
f : X ⟶ Y
i j : A
⊢ (shiftComm X j i).inv ≫
      (shiftComm X j i).hom ≫ (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫ (shiftComm Y i j).hom =
    (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫ (shiftComm Y i j).hom

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫ (shiftComm Y i j).hom =
    (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫ (shiftComm Y i j).hom
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
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ (α ≫ k) ≫ K.d i j = 0

Tactic:
rw [assoc, hk, comp_zero]

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 i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ (f ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.fst = (g ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.fst

Tactic:
simpa using! h₁

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 ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
⊢ (inrX φ i ≫ d φ i j) ≫ fstX φ j (c.next j) hj = (G.d i j ≫ inrX φ j) ≫ fstX φ j (c.next j) hj

Tactic:
simp [d_fstX φ _ _ _ hij]

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 K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
hc : ∀ (j : ι), ∃ i, c.Rel i j
i j : ι
⊢ (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j

Tactic:
by_cases hij : c.Rel j i
  · dsimp
    simp only [inrCompHomotopy_hom φ hc i j hij, desc_f φ α hα _ _ hij,
      comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]
  · simp only [Homotopy.zero _ _ _ hij, zero_comp]

Goal state after:
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''

pp: case neg
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:
case neg
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''
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 (c.prev i) i
⊢ (f.f (c.prev i) - g.f (c.prev i) - K.d (c.prev i) i ≫ ho.hom i (c.prev i)) ≫ ((shortComplexFunctor C c i).obj L).f = 0

Tactic:
· dsimp
      rw [L.shape _ _ h, comp_zero]

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

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (functor r).map ((a • f) ≫ g) = (functor r).map (a • f ≫ g)

Tactic:
Linear.smul_comp

Goal state after:
R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (functor r).map (a • f ≫ g) = (functor r).map (a • f ≫ g)
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
x✝ : Nonempty (Homotopy f 0)
h : Homotopy f 0
⊢ (quotient V c).map f = 0

Tactic:
simpa using eq_of_homotopy _ _ h

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ (iso F r hF a).hom.app ((functor r).obj X) =
    (lift r F hF).map ((Functor.commShiftIso (functor r) a).inv.app X) ≫ (Functor.commShiftIso F a).hom.app X

Tactic:
simp [iso, lift_obj_functor_obj]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ (iso F r hF a).inv.app ((functor r).obj X) =
    (Functor.commShiftIso F a).inv.app X ≫ (lift r F hF).map ((Functor.commShiftIso (functor r) a).hom.app X)

Tactic:
simp [iso, lift_obj_functor_obj]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
n : ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₂)
          (n.negOnePow •
            (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁)).mor₂ ≫
      (CategoryTheory.shiftFunctor C n).map f.hom₃ =
    (CategoryTheory.shiftFunctor C n).map f.hom₂ ≫
      (mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₂)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj₁)).mor₂

Tactic:
by
        dsimp
        simp only [Linear.units_smul_comp, Linear.comp_units_smul, ← Functor.map_comp, f.comm₂]

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

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T.obj₁ ≫
      (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    (eqToHom ⋯).hom₁ ≫
      (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + (b + c)) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁)

Tactic:
dsimp only [CategoryTheory.shiftFunctorAdd']

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₁ ≫
      (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₁) =
    (eqToHom ⋯).hom₁ ≫
      (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₁)
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T.obj₂ ≫
      (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂) =
    (eqToHom ⋯).hom₂ ≫
      (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + (b + c)) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂)

Tactic:
dsimp only [CategoryTheory.shiftFunctorAdd']

Goal state after:
case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₂ ≫
      (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₂) =
    (eqToHom ⋯).hom₂ ≫
      (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₂)
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: case h₃
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T.obj₃ ≫
      (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃) =
    (eqToHom ⋯).hom₃ ≫
      (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + (b + c)) ⋯).hom.app T.obj₃ ≫
        (CategoryTheory.shiftFunctor C c).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃)

Tactic:
dsimp only [CategoryTheory.shiftFunctorAdd']

Goal state after:
case h₃
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₃ ≫
      (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₃) =
    (eqToHom ⋯).hom₃ ≫
      (eqToIso ⋯ ≪≫ shiftFunctorAdd C (a + b) c).hom.app T.obj₃ ≫
        (CategoryTheory.shiftFunctor C c).map ((eqToIso ⋯ ≪≫ shiftFunctorAdd C a b).hom.app T.obj₃)
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
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₂ : IsIso φ.hom₂
⊢ IsIso ((rotate C).map φ).hom₃

Tactic:
by dsimp; 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
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
⊢ IsIso ((invRotate C).map φ).hom₁

Tactic:
by dsimp; 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
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
⊢ IsIso ((invRotate C).map φ).hom₃

Tactic:
by dsimp; infer_instance

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
⊢ δ (-1) 0 0 = Cochain.ofHom (inr φ ≫ (triangle φ).mor₃)

Tactic:
simp only [δ_zero, inr_triangleδ, Cochain.ofHom_zero]

Goal state after:
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
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ ∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C

Tactic:
obtain ⟨f, rfl⟩ := (quotient _ _).map_surjective f
  exact ⟨_, _, _, ⟨_, _, f, ⟨Iso.refl _⟩⟩⟩

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
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
ha'' : ∀ (j : J), ∃ g, (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun j ↦ (T j).obj₃) j = g ≫ (T j).mor₂
b : (j : J) → A ⟶ (T j).obj₂ := fun j ↦ ⋯.choose
hb : ∀ (j : J), (a - a' ≫ φ'.hom₃) ≫ Pi.π (fun j ↦ (T j).obj₃) j = b j ≫ (T j).mor₂
hb' : a - a' ≫ φ'.hom₃ = Pi.lift b ≫ (productTriangle T).mor₂
⊢ A ⟶ T'.obj₂

Tactic:
exact Pi.lift b

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K✝ : HomologicalComplex C c
i j : ι
hij : c.Rel i j
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
φ : K ⟶ L
⊢ (composableArrows₃ K i j).map' 1 2 _proof_246✝ _proof_299✝ ≫ cyclesMap φ j =
    opcyclesMap φ i ≫ (composableArrows₃ L i j).map' 1 2 _proof_246✝ _proof_299✝

Tactic:
simp [-Fin.reduceFinMk]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K✝ : HomologicalComplex C c
i j : ι
hij : c.Rel i j
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
φ : K ⟶ L
⊢ (composableArrows₃ K i j).map' 2 3 _proof_299✝ _proof_300✝ ≫ homologyMap φ j =
    cyclesMap φ j ≫ (composableArrows₃ L i j).map' 2 3 _proof_299✝ _proof_300✝

Tactic:
simp [-Fin.reduceFinMk]

Goal state after: