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

Goal state before:
pp: case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hrn : ∃ y ∈ I • (R ∙ i), ∃ z ∈ I • span R s, y + z = ((LinearMap.lsmul R M) r) n
hn : n ∈ N
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)

Tactic:
rcases hrn with ⟨y, hy, z, hz, hyz⟩

Goal state after:
case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
y : M
hy : y ∈ I • (R ∙ i)
z : M
hz : z ∈ I • span R s
hyz : y + z = ((LinearMap.lsmul R M) r) n
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)

Tactic:
simp only [mem_comap, LinearMap.lsmul_apply]

Goal state after:
case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ (c * r) • n ∈ I • span R s
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 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ I • sInf (N '' S) i ≤ sInf (N '' S) (i + 1)

Tactic:
rw [sInf_eq_iInf', iInf_apply, iInf_apply]
        refine smul_iInf_le.trans ?_
        apply iInf_mono _
        rintro ⟨_, F, hF, rfl⟩
        exact F.smul_le i

Goal state after:
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
  | zero => simp
  | succ _ ih => rw [← add_assoc, ← hn, ih, add_comm, pow_add, mul_smul, pow_one]; lia

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

Tactic:
tsub_add_cancel_of_le hn

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
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
⊢ n = n
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
R : Type u
inst✝⁴ : CommRing R
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
h : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(QuotientAddGroup.lift (I • ⊤).toAddSubgroup f.toAddMonoidHom ⋯)

Tactic:
exact QuotientAddGroup.lift_surjective_of_surjective _ _ h _

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
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I J : Ideal R
hIJ : I = J
x y : ↥I
⊢ (J.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I J hIJ)) (x * y) = 0

Tactic:
simp [toCotangent_eq_zero, ← hIJ, sq, mul_mem_mul]

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
h : I ≠ ⊤
⊢ ⨅ i, I ^ i = ⊥

Tactic:
convert! I.iInf_pow_smul_eq_bot_of_isLocalRing (M := R) h

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
h : I ≠ ⊤
x✝ : ℕ
⊢ I ^ x✝ = I ^ x✝ • ⊤
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤

Tactic:
by_cases I = ⊤

Goal state after:
case pos
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : I = ⊤
⊢ I = ⊥ ∨ I = ⊤

case neg
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ I = ⊥ ∨ I = ⊤
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: case mk.mk
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 φ
desc✝¹ : {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} → M'.Derivation φ → (M ⟶ M')
fac✝¹ : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), d.postcomp (desc✝¹ d') = d'
postcomp_injective✝¹ :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (φ_1 φ' : M ⟶ M'),
    d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
desc✝ : {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} → M'.Derivation φ → (M ⟶ M')
fac✝ : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), d.postcomp (desc✝ d') = d'
postcomp_injective✝ :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (φ_1 φ' : M ⟶ M'),
    d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
this :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ),
    { desc := desc✝¹, fac := fac✝¹, postcomp_injective := postcomp_injective✝¹ }.desc d' =
      { desc := desc✝, fac := fac✝, postcomp_injective := postcomp_injective✝ }.desc d'
⊢ desc✝¹ = desc✝

Tactic:
ext : 2

Goal state after:
case mk.mk
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 φ
desc✝¹ : {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} → M'.Derivation φ → (M ⟶ M')
fac✝¹ : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), d.postcomp (desc✝¹ d') = d'
postcomp_injective✝¹ :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (φ_1 φ' : M ⟶ M'),
    d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
desc✝ : {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} → M'.Derivation φ → (M ⟶ M')
fac✝ : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), d.postcomp (desc✝ d') = d'
postcomp_injective✝ :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (φ_1 φ' : M ⟶ M'),
    d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
this :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ),
    { desc := desc✝¹, fac := fac✝¹, postcomp_injective := postcomp_injective✝¹ }.desc d' =
      { desc := desc✝, fac := fac✝, postcomp_injective := postcomp_injective✝ }.desc d'
x✝¹ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : x✝¹.Derivation φ
⊢ desc✝¹ x✝ = desc✝ x✝
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
⊢ C.d i j ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
⊢ 0 = 0
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 ι
K : HomologicalComplex V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
i k : ι
hik : c.Rel i k
⊢ (if hi : i = j then (K.XIsoOfEq hi).hom ≫ φ ≫ (singleObjXIsoOfEq c j A i hi).inv else 0) ≫ 0 =
    K.d i k ≫ if hi : k = j then (K.XIsoOfEq hi).hom ≫ φ ≫ (singleObjXIsoOfEq c j A k hi).inv else 0

Tactic:
comp_zero

Goal state after:
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
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
i k : ι
hik : c.Rel i k
⊢ 0 = K.d i k ≫ if hi : k = j then (K.XIsoOfEq hi).hom ≫ φ ≫ (singleObjXIsoOfEq c j A k hi).inv else 0
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
φ : C ⟶ (single₀ V).obj X
⊢ φ.f 1 ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
φ : C ⟶ (single₀ V).obj X
⊢ 0 = 0
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).symm.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

Tactic:
Iso.symm_hom,

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 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
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ 0 = colimit.ι (F ⋙ eval C c n) j ≫ 0

Tactic:
comp_zero

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝ : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ 0 = 0
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
m₁ m₂ m₃ : A
X : C
h :
  (shiftFunctorAdd D (m₁ + m₂) m₃).hom.app (F.obj X) ≫
      (shiftFunctor D m₃).map ((shiftFunctorAdd D m₁ m₂).hom.app (F.obj X)) =
    (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
      (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X))
⊢ (eqToHom ⋯ ≫ (i (m₁ + (m₂ + m₃))).hom.app X ≫ eqToHom ⋯) ≫
      (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯).hom.app (F.obj X) ≫
        (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X)) ≫
          (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X) ≫ (i m₂).inv.app ((s m₁).obj X)) =
    F.map (eqToHom ⋯) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        (shiftFunctorAdd D m₁ (m₂ + m₃)).hom.app (F.obj X) ≫
          (shiftFunctorAdd D m₂ m₃).hom.app ((shiftFunctor D m₁).obj (F.obj X)) ≫
            (shiftFunctor D m₃).map ((shiftFunctor D m₂).map ((i m₁).inv.app X)) ≫
              (shiftFunctor D m₃).map ((i m₂).inv.app ((s m₁).obj X))

Tactic:
simp [shiftFunctorAdd', eqToHom_map]

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

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
hij : ¬c.Rel i j
⊢ K.iCycles i ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
hij : ¬c.Rel i j
⊢ 0 = 0
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
⊢ α ≫ 0 = 0

Tactic:
comp_zero

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
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
⊢ 0 = 0
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 : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
⊢ x ≫ 0 = 0

Tactic:
comp_zero

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
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
⊢ 0 = 0
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 : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ x ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
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 : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ 0 = 0
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 : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx✝ : k = x ≫ K.d i' i
hx : k = x ≫ 0
h : ¬c.Rel i' i
⊢ K.liftCycles k j hj ⋯ = 0

Tactic:
comp_zero

Goal state after:
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 : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx✝ : k = x ≫ K.d i' i
hx : k = 0
h : ¬c.Rel i' i
⊢ K.liftCycles k j hj ⋯ = 0
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
⊢ Epi (K.pOpcycles i)

Tactic:
dsimp only [pOpcycles]

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
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst✝ : K.HasHomology i
⊢ Epi (K.sc i).pOpcycles
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: case neg
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
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
this : K.descOpcycles k j hj ⋯ = 0
⊢ K.homologyι i ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
case neg
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
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
this : K.descOpcycles k j hj ⋯ = 0
⊢ 0 = 0
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
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
⊢ φ.f j ≫ 0 = 0

Tactic:
comp_zero

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
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
⊢ 0 = 0
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:
rw [Submodule.map_sup, ← kerTotal_map R R A B h, Submodule.map_span, ← Set.range_comp]

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 (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔
      Submodule.span A
        (Set.range
          (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x ↦
            single ((algebraMap R A) x) 1)) =
    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 B) x) 1)
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 : ι
⊢ HasColimit (pair K L ⋙ eval C c i)

Tactic:
have e : _ ≅ pair (K.X i) (L.X i) := diagramIsoPair (pair K L ⋙ eval C c i)
  exact hasColimit_of_iso e

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

Goal state before:
pp: case mp
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)
x : B ⊗[A] Ω[A⁄R]
⊢ x ∈ (kerCotangentToTensor R A B).range → x ∈ Submodule.restrictScalars A (mapBaseChange R A B).ker

Tactic:
rintro ⟨x, rfl⟩
    obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
    simp only [kerCotangentToTensor_toCotangent, Submodule.restrictScalars_mem, LinearMap.mem_ker,
      mapBaseChange_tmul, map_D, RingHom.mem_ker.mp x.2, map_zero, smul_zero]

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 (c.prev i) i
⊢ f i (c.prev i) ≫ 0 = 0

Tactic:
comp_zero

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

Tactic:
comp_zero

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
f g : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i j : ι
w : ¬c.Rel j i
⊢ 0 = 0
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 : C ⟶ D
hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)
i j : ι
h✝ : ¬c.Rel j i
⊢ f.f i ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
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 : C ⟶ D
hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)
i j : ι
h✝ : ¬c.Rel j i
⊢ 0 = 0
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.X i ⟶ D.X j
i : ι
⊢ G.map (C.d i (c.next i) ≫ hom (c.next i) i + hom i (c.prev i) ≫ D.d (c.prev i) i) =
    G.map (C.d i (c.next i)) ≫ G.map (hom (c.next i) i) + G.map (hom i (c.prev i)) ≫ G.map (D.d (c.prev i) i)

Tactic:
simp only [G.map_comp, Functor.map_add]

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 ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : ¬c.Rel i j
⊢ inrX φ i ≫ 0 = 0

Tactic:
comp_zero

Goal state after:
case neg
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
⊢ 0 = 0