mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ ↑⟨a, ha⟩ • ↑(μ i) • x = 0

Tactic:
rw [smul_smul]

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
⊢ (↑⟨a, ha⟩ * ↑(μ i)) • x = 0
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
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = torsionBySet R M ↑(⨅ a ∈ S, Ideal.span {q a})

Tactic:
←
    iSup_torsionBySet_ideal_eq_torsionBySet_iInf

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = ⨆ i ∈ S, torsionBySet R M ↑(Ideal.span {q i})

R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ (↑S).Pairwise fun i j ↦ Ideal.span {q i} ⊔ Ideal.span {q j} = ⊤
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h
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₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
k : ℕ
⊢ F.N (n₀ + k) = I ^ k • F.N n₀

Tactic:
induction k with

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ I • ⊤ ≤ Submodule.comap (Submodule.subtype I) (I ^ 2)

Tactic:
rw [← Submodule.map_le_iff_le_comap, Submodule.map_smul'', Submodule.map_top,
        Submodule.range_subtype, smul_eq_mul, pow_two]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : I.Cotangent
⊢ I.cotangentToQuotientSquare x ∈ Submodule.restrictScalars R I.cotangentIdeal

Tactic:
← range_cotangentToQuotientSquare

Goal state after:
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : I.Cotangent
⊢ I.cotangentToQuotientSquare x ∈ I.cotangentToQuotientSquare.range
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr
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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
⊢ (Submodule.span (↥(reesAlgebra I)) (single R ↑⟨i, hi⟩ '' ↑(F.N ↑⟨i, hi⟩))).FG

Tactic:
have : Submodule.span (reesAlgebra I) (s.image (lsingle R i) : Set (PolynomialModule R M)) =
        Submodule.span _ (single R i '' (F.N i : Set M)) := by
      rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs]; rfl

Goal state after:
case mpr
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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
this :
  Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))
⊢ (Submodule.span (↥(reesAlgebra I)) (single R ↑⟨i, hi⟩ '' ↑(F.N ↑⟨i, hi⟩))).FG
Module: Mathlib.RingTheory.Ideal.Cotangent

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

Tactic:
refine (Submodule.map_le_map_iff_of_injective (Submodule.injective_subtype _) _ _).mp ?_

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (maximalIdeal R).toCotangent M = ⊤
⊢ Submodule.map (Submodule.subtype (maximalIdeal R)) ⊤ ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) M
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (𝟙 X j) = 𝟙 (F.obj (X j))

Tactic:
GradedObject.categoryOfGradedObjects_id,

Goal state after:
C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (𝟙 (X j)) = 𝟙 (F.obj (X j))
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (𝟙 Y j) = 𝟙 (F.obj (Y j))

Tactic:
GradedObject.categoryOfGradedObjects_id,

Goal state after:
C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (𝟙 (Y j)) = 𝟙 (F.obj (Y j))
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
⊢ ∀ (X : Discrete A),
    (MonoidalCategoryStruct.rightUnitor ((Discrete.functor h.F).obj X)).hom =
      MonoidalCategoryStruct.whiskerLeft ((Discrete.functor h.F).obj X) h.zero.symm.hom ≫
        (h.add X.as (MonoidalCategoryStruct.tensorUnit (Discrete A)).as).symm.hom ≫
          (Discrete.functor h.F).map (MonoidalCategoryStruct.rightUnitor X).hom

Tactic:
rintro ⟨n⟩
        ext X
        simp [h.add_zero_inv_app]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X) =
    (eqToHom ⋯ ≫ (shiftFunctorAdd C a₁ (a₂ + a₃)).hom.app X) ≫
      (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)

Tactic:
dsimp [shiftFunctorAdd, shiftFunctor]

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ + a₂ } { as := a₃ }).app X ≫
      ((shiftMonoidalFunctor C A).obj { as := a₃ }).map
        ((OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ }).app X) =
    (eqToHom ⋯ ≫ (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).app X) ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
        (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
i k : ι
hik : c.Rel i k
hi : ¬i = j
⊢ 0 ≫ K.d i k = 0

Tactic:
· apply (isZero_single_obj_X c j A i hi).eq_of_src

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
i : ι
hi : c.Rel i j
⊢ False

Tactic:
have : c.prev j = i := c.prev_eq' 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
this : c.prev j = i
⊢ False
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
f : { f // C.d 1 0 ≫ f = 0 }
i : ℕ
hi : (ComplexShape.down ℕ).Rel i 0
⊢ C.d i 0 ≫ ↑f = 0

Tactic:
by
    obtain rfl : i = 1 := by simpa using hi.symm
    exact f.2

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
C : CochainComplex V ℕ
X : V
f : { f // f ≫ C.d 0 1 = 0 }
i : ℕ
hi : (ComplexShape.up ℕ).Rel 0 i
⊢ ↑f ≫ C.d 0 i = 0

Tactic:
by
    obtain rfl : i = 1 := by simpa using hi.symm
    exact f.2

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

Goal state before:
pp: 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
j : α
⊢ of.d X d (j + 1) j = d j

Tactic:
dsimp [of.d]

Goal state after:
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
j : α
⊢ (if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ (shiftFunctorAdd' C p' p 0 hp).hom.app X =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
            (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)

Tactic:
rw [← NatTrans.naturality]

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ (shiftFunctorAdd' C p' p 0 hp).hom.app X =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C m ⋙ shiftFunctor C n).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X) ≫
            (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C p').obj X)
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 ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
⊢ (ComplexShape.up α).Rel i j → (ComplexShape.up α).Rel j k → of.d X d i j ≫ of.d X d j k = 0

Tactic:
dsimp [of.d]

Goal state after:
ι : 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 ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
⊢ i + 1 = j →
    j + 1 = k → ((if h : i + 1 = j then d i ≫ eqToHom ⋯ else 0) ≫ if h : j + 1 = k then d j ≫ eqToHom ⋯ else 0) = 0
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: 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 ⟶ X (n + 1)
j : α
⊢ of.d X d j (j + 1) = d j

Tactic:
dsimp [of.d]

Goal state after:
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 ⟶ X (n + 1)
j : α
⊢ (if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j
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 i j).hom ≫ (shiftFunctor C i).map ((shiftFunctor C j).map f) =
    (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫ (shiftComm Y i j).hom

Tactic:
shiftComm',

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
⊢ (shiftComm X i j).hom ≫
      (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
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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
      (kerTotal R A ⊔ Submodule.span A (Set.range fun x ↦ single ((algebraMap R A) x) 1)) =
    Submodule.restrictScalars A (kerTotal R B)

Tactic:
by
  rw [Submodule.map_sup, ← kerTotal_map R R A B h, Submodule.map_span, ← Set.range_comp]
  congr
  ext; simp [IsScalarTower.algebraMap_eq R A B]

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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.map (linearCombination A ⇑(D R A)) (kerTotal R A) ⊔
        Submodule.map (linearCombination A ⇑(D R A))
          (Submodule.span A (Set.range fun x ↦ single ((algebraMap R A) x) 1)) ⊔
      Submodule.map (linearCombination A ⇑(D R A))
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker

Tactic:
← kerTotal_eq,

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
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.map (linearCombination A ⇑(D R A)) (linearCombination A ⇑(D R A)).ker ⊔
        Submodule.map (linearCombination A ⇑(D R A))
          (Submodule.span A (Set.range fun x ↦ single ((algebraMap R A) x) 1)) ⊔
      Submodule.map (linearCombination A ⇑(D R A))
        (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod

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
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ (biprod.inl ≫ biprod.fst).f i = 𝟙 (K.X i)

Tactic:
biprod.inl_fst,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ (𝟙 K).f i = 𝟙 (K.X i)
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
F : C ⥤ D
⊢ (isomorphisms C).IsInvertedBy F

Tactic:
by
  intro _ _ _ hf
  simp only [isomorphisms.iff] at hf
  infer_instance

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
⊢ inrX φ j ≫ (XIsoBiprod φ j i hij).hom = biprod.inr

Tactic:
obtain rfl := c.next_eq' hij
  have := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
  simp [inrX, XIsoBiprod, dif_pos hij]

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✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i j : ι
w : ¬c.Rel j i
⊢ h.hom i j ≫ g.f j = 0

Tactic:
rw [h.zero i j w, zero_comp]

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 φ
i : ℤ
⊢ IsZero ((mappingCone φ).X i) ↔ IsZero (F.X (i + 1)) ∧ IsZero (G.X i)

Tactic:
by
  have := HasHomotopyCofiber.hasBinaryBiproduct φ i (i + 1) rfl
  rw [← biprod_isZero_iff]
  exact (homotopyCofiber.XIsoBiprod φ i (i + 1) rfl).isZero_iff

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

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
F G K L : CochainComplex C ℤ
n m : ℤ
x✝² x✝¹ : R
x✝ : Cocycle F G n
p✝ q✝ : ℤ
hpq✝ : p✝ + n = q✝
⊢ (x✝² * x✝¹) • (↑x✝).v p✝ q✝ hpq✝ = x✝² • x✝¹ • (↑x✝).v p✝ q✝ hpq✝

Tactic:
rw [smul_smul]

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

Goal state before:
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
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ¬∃ k, c.Rel j k
⊢ inrX K j ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inrX K j ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
simp only [not_exists] at hj
    simp only [assoc, Homotopy.nullHomotopicMap'_f_of_not_rel_left hij hj,
      homotopyCofiber_d, homotopyCofiber.inlX_d' _ _ _ _ (hj _), homotopyCofiber.inrX_sndX_assoc,
      comp_sub, inrX_π_assoc, comp_id, ι₀, comp_f, homotopyCofiber.inr_f]
    rw [← cancel_epi (biprodXIso K K j).inv]
    ext
    · simp
    · simp [this]

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 : Quotient r) (f : X ⟶ Y) (r_1 : R) (g : Y ⟶ Z), f ≫ (r_1 • g) = r_1 • f ≫ g

Tactic:
rintro ⟨X⟩ ⟨Y⟩ ⟨Z⟩ f a g

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
f : { as := X } ⟶ { as := Y }
a : R
g : { as := Y } ⟶ { as := Z }
⊢ f ≫ (a • g) = a • f ≫ g
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₂
X : C
⊢ (LiftCommShift.iso F r hF 0).hom.app ((functor r).obj X) =
    (Functor.CommShift.isoZero (lift r F hF) A).hom.app ((functor r).obj X)

Tactic:
rw [LiftCommShift.iso_hom_app, (functor r).commShiftIso_zero,
      Functor.CommShift.isoZero_hom_app, Functor.CommShift.isoZero_inv_app,
      Functor.map_comp, assoc, F.commShiftIso_zero, Functor.CommShift.isoZero_hom_app,
      lift_map_functor_map, ← F.map_comp_assoc, Iso.inv_hom_id_app]

Goal state after:
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₂
X : C
⊢ (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      F.map (𝟙 ((𝟭 C).obj X)) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app ((lift r F hF).obj ((functor r).obj X))
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p' + n' = q
⊢ (γ.leftUnshift n hn).v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p' p ⋯).inv ≫ γ.v p' q ⋯

Tactic:
by
  obtain rfl : p' = p - a := by lia
  rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
m m' : ℤ
hm' : m + a = m'
⊢ δ n m (γ.leftUnshift n hn) = a.negOnePow • (δ n' m' γ).leftUnshift m hm'

Tactic:
obtain ⟨γ', rfl⟩ := (leftShiftAddEquiv K L n a n' hn).surjective γ
  dsimp
  simp only [leftUnshift_leftShift, γ'.δ_leftShift a n' m' hn m hm', leftUnshift_units_smul,
    smul_smul, Int.units_mul_self, one_smul]

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
n p q : ℤ
hpq : p + 1 = q
⊢ (δ 0 1 ((snd φ).shift n)).v p q hpq +
      ((n.negOnePow • (↑(fst φ)).shift n).comp
            (Cochain.ofHom ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)) ⋯).v
        p q hpq =
    0

Tactic:
simp only [Cochain.δ_shift, δ_snd, Cochain.shift_neg, smul_neg, Cochain.neg_v,
      shiftFunctor_obj_X', Cochain.units_smul_v, Cochain.shift_v', Cochain.comp_zero_cochain_v,
      Cochain.ofHom_v, Cochain.units_smul_comp, shiftFunctor_map_f', neg_add_cancel]

Goal state after: