mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ torsionBySet R M Set.univ ≤ ⊥

Tactic:
← torsionBy_one,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ torsionBySet R M Set.univ ≤ torsionBy R M 1
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type u_3
A : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
a : A
inst✝⁵ : Algebra R A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module A M
inst✝² : Module R M
inst✝¹ : IsScalarTower R A M
inst✝ : FaithfulSMul A M
⊢ annihilator R[X] (AEval R M a) = RingHom.ker (aeval a)

Tactic:
ext p
  simp_rw [mem_annihilator, RingHom.mem_ker]
  change (∀ m : M, aeval a p • m = 0) ↔ _
  exact ⟨fun h ↦ eq_of_smul_eq_smul (α := M) <| by simp [h], fun h ↦ by simp [h]⟩

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

Goal state before:
pp: case succ
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
        ((↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)) (single R j m)) =
    single R (n + (1 + j)) (r • m)

Tactic:
← hn

Goal state after:
case succ
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
        ((↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)) (single R j m)) =
    r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
        (single R (1 + j) m)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ Submodule.map (maximalIdeal R).toCotangent ⊤ = ⊤

Tactic:
simp [Ideal.toCotangent_range]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
h₁ h₂ : d.Universal
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ ∀ (d' : M'.Derivation φ), h₁.desc d' = h₂.desc d'

Tactic:
d'

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
h₁ h₂ : d.Universal
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation φ
⊢ h₁.desc d' = h₂.desc d'
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
⊢ ∀ (a b : M₁ ⟶ M₂), a - b = a + -b

Tactic:
by intros; ext1; simp only [add_app, sub_app, neg_app, sub_eq_add_neg]

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 ι
A B : HomologicalComplex V c
f : A.Hom B
i j : ι
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

Tactic:
by_cases hij : c.Rel i j
  · exact f.comm' i j hij
  · rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]

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
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j k : α
hij : (ComplexShape.down α).Rel i j
hjk : (ComplexShape.down α).Rel j k
⊢ of.d X d i j ≫ of.d X d j k = 0

Tactic:
dsimp [of.d] at hij hjk ⊢
      subst hij hjk
      simp only [eqToHom_refl, id_comp, dite_eq_ite, ite_true, sq]

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
⊢ Submodule.span S (Set.range ⇑(D R S)) = ⊤

Tactic:
by
  rw [_root_.eq_top_iff]
  rintro x -
  obtain ⟨⟨x, hx⟩, rfl⟩ := fromIdeal_surjective R S x
  rw [← Submodule.restrictScalars_mem S, ← KaehlerDifferential.submodule_span_range_eq_ideal] at hx
  suffices ∃ hx,
      fromIdeal R S ⟨x, hx⟩ ∈ Submodule.span S (Set.range <| KaehlerDifferential.D R S) from
    this.snd
  -- TODO: this proof looks like we're reinventing `Submodule.span_le`.
  -- I'm not sure what's the RHS here though.
  refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
  · rintro _ ⟨x, rfl⟩
    refine ⟨KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x, ?_⟩
    apply Submodule.subset_span
    exact ⟨x, KaehlerDifferential.DLinearMap_apply R S x⟩
  · exact ⟨zero_mem _, Submodule.zero_mem _⟩
  · rintro x y - - ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩; exact ⟨add_mem hx₁ hy₁, Submodule.add_mem _ hx₂ hy₂⟩
  · rintro r x - ⟨hx₁, hx₂⟩
    exact ⟨((KaehlerDifferential.ideal R S).restrictScalars S).smul_mem r hx₁,
      Submodule.smul_mem _ r 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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
⊢ f x = f' x

Tactic:
have : x ∈ Submodule.span S (Set.range <| KaehlerDifferential.D R S) := by
    rw [KaehlerDifferential.span_range_derivation]; trivial

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
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ f x = f' x
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case zero
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
⊢ (succ' d₀).fst = (succ' (𝟙 X₁ ≫ d₀)).fst

Tactic:
rw [id_comp]

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

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
e₁ :
  (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S)
      ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)
e : ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x
⊢ ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
    (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x

Tactic:
apply (KaehlerDifferential.quotientCotangentIdealRingEquiv R S).injective

Goal state after:
case mpr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
e₁ :
  (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S)
      ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)
e : ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x
⊢ (quotientCotangentIdealRingEquiv R S) (((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x) =
    (quotientCotangentIdealRingEquiv R S)
      ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)
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
X : C
⊢ F.map ((zero hF s i).hom.app X) = (i 0).hom.app X ≫ (shiftFunctorZero D A).hom.app (F.obj X)

Tactic:
by
  simp [zero]

Goal state after:
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
X : C
⊢ F.map ((zero hF s i).inv.app X) = (shiftFunctorZero D A).inv.app (F.obj X) ≫ (i 0).inv.app X

Tactic:
by
  simp [zero]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
⊢ (mapBaseChange R A B) (x ⊗ₜ[A] y) = x • (map R R A B) y

Tactic:
conv_lhs => rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul', map_smul]

Goal state after:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
⊢ x • (mapBaseChange R A B) (1 ⊗ₜ[A] y) = x • (map R R A B) y
Module: Mathlib.Algebra.Homology.Homotopy

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

Tactic:
rw [nullHomotopicMap', map_nullHomotopicMap]

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

Goal state before:
pp: case e_a.succ
ι : 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)
n✝ : ℕ
⊢ eqToHom ⋯ ≫ (mkInductiveAux₁ e zero one comm_one succ n✝).fst =
    𝟙 (xNext P (n✝ + 1)) ≫ eqToHom ⋯ ≫ (mkInductiveAux₁ e zero one comm_one succ n✝).fst

Tactic:
rw [id_comp]

Goal state after:
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 ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

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

Tactic:
· exact homotopyCofiber.ext_from_X (biprod.lift (𝟙 K) (-𝟙 K)) (c.next i) i hi
      (inlX_nullHomotopy_f _ _ _ _) (inrX_nullHomotopy_f _ hc _)

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

Goal state before:
pp: C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F : HomologicalComplex C c
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✝⁴ : ∀ (i : ι), HasBinaryBiproduct (F.X i) (F.X i)
inst✝³ : HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))
inst✝² :
  ∀ (i : ι), HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i) (((H.mapHomologicalComplex c).obj F).X i)
inst✝¹ :
  HasHomotopyCofiber (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ (H.mapHomologicalComplex c).map (ι₁ F) ≫ (mapHomologicalComplexObjIso F H hc).hom =
    ι₁ ((H.mapHomologicalComplex c).obj F)

Tactic:
dsimp [mapHomologicalComplexObjIso, ι₁, homotopyCofiber.mapArrowHom]
  rw [Functor.map_comp, assoc, homotopyCofiber.inr_mapHomologicalComplexObjIso_hom_assoc,
    homotopyCofiber.inr_desc, ← Category.assoc]
  congr 1
  apply biprod.hom_ext <;> simp [← Functor.map_comp]

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
n₁ n₂ : ℤ
K : CochainComplex C ℤ
x✝² x✝¹ : ℤ
x✝ : (ComplexShape.up ℤ).Rel x✝² x✝¹
⊢ (XIsoOfEq K ⋯).hom ≫ (n₂.negOnePow • n₁.negOnePow • K.d (x✝² + n₂ + n₁) (x✝¹ + n₂ + n₁)) =
    ((n₁ + n₂).negOnePow • K.d (x✝² + (n₁ + n₂)) (x✝¹ + (n₁ + n₂))) ≫ (XIsoOfEq K ⋯).hom

Tactic:
simp only [add_comm n₁ n₂, Int.negOnePow_add, Linear.units_smul_comp,
        Linear.comp_units_smul, d_comp_XIsoOfEq_hom, smul_smul, XIsoOfEq_hom_comp_d]

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

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

Tactic:
Induced.zero_inv_app_obj,

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
n : A
X : C
⊢ eqToHom ⋯ ≫
      (i n).hom.app X ≫
        eqToHom ⋯ ≫ F.map ((shiftFunctorAdd C n 0).hom.app X) ≫ (i 0).inv.app ((shiftFunctor C n).obj X) =
    (eqToHom ⋯).app (F.obj X) ≫
      (𝟭 D).map ((i n).hom.app X) ≫
        F.map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n).obj X)) ≫ (i 0).inv.app ((shiftFunctor C n).obj X)
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 : A
hτ : CommShiftCore τ a
X : C
⊢ τ.app ((shiftFunctor C a).obj X) =
    (Functor.commShiftIso F₁ a).hom.app X ≫ (shiftFunctor D a).map (τ.app X) ≫ (Functor.commShiftIso F₂ a).inv.app X

Tactic:
by
  simp [hτ.shift_app_comm_assoc τ X]

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

Goal state before:
pp: case h₀
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 : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := ⋯
⊢ (T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom) ≫ biprod.fst = biprod.inl ≫ biprod.fst

pp: case h₁
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 : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := ⋯
⊢ (T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom) ≫ biprod.snd = biprod.inl ≫ biprod.snd

Tactic:
· simpa [d] using d.bicone.inl_fst

Goal state after:
case h₁
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 : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := ⋯
⊢ (T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom) ≫ biprod.snd = biprod.inl ≫ biprod.snd
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
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr φ₁) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map b ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr φ₂)

Tactic:
simp only [← Functor.map_comp, triangleMapOfHomotopy_comm₂]

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
⊢ δ 0 1 (-(inl φ).leftShift 1 0 ⋯) + (↑(-(Cocycle.ofHom φ).leftShift 1 1 ⋯)).comp (Cochain.ofHom (inr φ)) ⋯ = 0

Tactic:
simp only [Int.reduceNeg, δ_neg,
        Cochain.δ_leftShift _ 1 0 1 (neg_add_cancel 1) 0 (zero_add 1),
        Int.negOnePow_one, δ_inl, Cochain.ofHom_comp, Cochain.leftShift_comp_zero_cochain,
        Units.neg_smul, one_smul, neg_neg, Cocycle.coe_neg, Cocycle.leftShift_coe,
        Cocycle.ofHom_coe, Cochain.neg_comp, add_neg_cancel]

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
⊢ lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 ⋯) (-(inl φ).leftShift 1 0 ⋯) ⋯ ≫ desc (inr φ) 0 (triangle φ).mor₃ ⋯ =
    𝟙 ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).obj K)

Tactic:
by
    ext n
    -- the following list of lemmas has been obtained by doing
    -- simp? [lift_desc_f _ _ _ _ _ _ _ _ _ rfl,
    --   (inl φ).leftShift_v 1 0 _ _ n _ (n + 1) (by simp only [add_neg_cancel_right])]
    simp only [shiftFunctor_obj_X', Int.reduceNeg, HomologicalComplex.comp_f,
      lift_desc_f _ _ _ _ _ _ _ _ _ rfl, Cocycle.coe_neg, Cocycle.leftShift_coe,
      Cocycle.ofHom_coe, Cochain.neg_v, Cochain.zero_v,
      comp_zero, (inl φ).leftShift_v 1 0 _ _ n _ (n + 1) (by simp only [add_neg_cancel_right]),
      shiftFunctor_obj_X, mul_zero, sub_self, Int.zero_ediv, add_zero, Int.negOnePow_zero,
      shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, id_comp, one_smul,
      Preadditive.neg_comp, inl_v_triangle_mor₃_f, Iso.refl_inv, neg_neg, zero_add,
      HomologicalComplex.id_f]

Goal state after:
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
G : C ⥤ D
inst✝ : G.Additive
⊢ (G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ ≫ 𝟙 ((G.mapHomologicalComplex (ComplexShape.up ℤ)).obj L) =
    𝟙 ((G.mapHomologicalComplex (ComplexShape.up ℤ)).obj K) ≫ (G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ

Tactic:
simp only [comp_id, id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
⊢ homOfDegreewiseSplit S σ ≫ 𝟙 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj S.X₁) =
    𝟙 S.X₃ ≫ homOfDegreewiseSplit S σ

Tactic:
simp only [comp_id, id_comp]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Category.{v_3, u_3} A
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
G : Type u_5
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ (shiftFunctor C m).obj Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ mn + a = a''

Tactic:
by rw [← ha'', ← ha', ← hnm, add_assoc]

Goal state after: