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

Goal state before:
pp: case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
i : ℕ
⊢ (F'.N i).FG

Tactic:
;

Goal state after:
case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
i : ℕ
⊢ (F'.N i).FG
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
i : ℕ
⊢ (F.N i).FG

Tactic:
;

Goal state after:
case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
i : ℕ
⊢ (F.N i).FG
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:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ Submodule.map (maximalIdeal R).toCotangent ⊤ = ⊤
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set ↥(maximalIdeal R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span R s = ⊤
⊢ Submodule.span R (⇑(maximalIdeal R).toCotangent '' s) = ⊤

Tactic:
← Submodule.map_span,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set ↥(maximalIdeal R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span R s = ⊤
⊢ Submodule.map (maximalIdeal R).toCotangent (Submodule.span R s) = ⊤
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: 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 = ⊤

pp: 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 = ⊤

Tactic:
;

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.Homology.ComplexShape

Goal state before:
pp: α : Type u_1
inst✝¹ : AddRightCancelSemigroup α
inst✝ : DecidableEq α
a x✝¹ x✝ : α
⊢ Decidable (x✝¹ + a = x✝)

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : AddRightCancelSemigroup α
inst✝ : DecidableEq α
a x✝¹ x✝ : α
⊢ Decidable (x✝¹ + a = x✝)
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: α : Type u_1
inst✝² : AddRightCancelSemigroup α
inst✝¹ : DecidableEq α
inst✝ : One α
⊢ DecidableRel (up' 1).Rel

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : AddRightCancelSemigroup α
inst✝¹ : DecidableEq α
inst✝ : One α
⊢ DecidableRel (up' 1).Rel
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
x✝ : Dᵒᵖ
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x✝))) ⋯
        (CommRingCat.KaehlerDifferential (φ'.app x✝))).inv

Tactic:
;

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
x✝ : Dᵒᵖ
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x✝))) ⋯
        (CommRingCat.KaehlerDifferential (φ'.app x✝))).inv
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
x✝ : Dᵒᵖ
b✝ : ↑(R.obj x✝)
⊢ (ConcreteCategory.hom (CommRingCat.KaehlerDifferential.map ⋯)) (CommRingCat.KaehlerDifferential.d b✝) =
    (ConcreteCategory.hom
        (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x✝))) ⋯
            (CommRingCat.KaehlerDifferential (φ'.app x✝))).inv)
      (CommRingCat.KaehlerDifferential.d b✝)

Tactic:
;

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
x✝ : Dᵒᵖ
b✝ : ↑(R.obj x✝)
⊢ (ConcreteCategory.hom (CommRingCat.KaehlerDifferential.map ⋯)) (CommRingCat.KaehlerDifferential.d b✝) =
    (ConcreteCategory.hom
        (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 x✝))) ⋯
            (CommRingCat.KaehlerDifferential (φ'.app x✝))).inv)
      (CommRingCat.KaehlerDifferential.d b✝)
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
X✝ Y✝ Z✝ : Dᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    CommRingCat.KaehlerDifferential.map ⋯ ≫
      (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map x✝¹))).map (CommRingCat.KaehlerDifferential.map ⋯) ≫
        (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (R.map x✝¹)) (CommRingCat.Hom.hom (R.map x✝))
            (CommRingCat.Hom.hom (R.map (x✝¹ ≫ x✝))) ⋯ (CommRingCat.KaehlerDifferential (φ'.app Z✝))).inv

Tactic:
;

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
X✝ Y✝ Z✝ : Dᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    CommRingCat.KaehlerDifferential.map ⋯ ≫
      (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map x✝¹))).map (CommRingCat.KaehlerDifferential.map ⋯) ≫
        (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (R.map x✝¹)) (CommRingCat.Hom.hom (R.map x✝))
            (CommRingCat.Hom.hom (R.map (x✝¹ ≫ x✝))) ⋯ (CommRingCat.KaehlerDifferential (φ'.app Z✝))).inv
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
X✝ Y✝ Z✝ : Dᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
b✝ : ↑(R.obj X✝)
⊢ (ConcreteCategory.hom (CommRingCat.KaehlerDifferential.map ⋯)) (CommRingCat.KaehlerDifferential.d b✝) =
    (ConcreteCategory.hom
        (CommRingCat.KaehlerDifferential.map ⋯ ≫
          (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map x✝¹))).map (CommRingCat.KaehlerDifferential.map ⋯) ≫
            (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (R.map x✝¹)) (CommRingCat.Hom.hom (R.map x✝))
                (CommRingCat.Hom.hom (R.map (x✝¹ ≫ x✝))) ⋯ (CommRingCat.KaehlerDifferential (φ'.app Z✝))).inv))
      (CommRingCat.KaehlerDifferential.d b✝)

Tactic:
;

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
X✝ Y✝ Z✝ : Dᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
b✝ : ↑(R.obj X✝)
⊢ (ConcreteCategory.hom (CommRingCat.KaehlerDifferential.map ⋯)) (CommRingCat.KaehlerDifferential.d b✝) =
    (ConcreteCategory.hom
        (CommRingCat.KaehlerDifferential.map ⋯ ≫
          (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map x✝¹))).map (CommRingCat.KaehlerDifferential.map ⋯) ≫
            (ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (R.map x✝¹)) (CommRingCat.Hom.hom (R.map x✝))
                (CommRingCat.Hom.hom (R.map (x✝¹ ≫ x✝))) ⋯ (CommRingCat.KaehlerDifferential (φ'.app Z✝))).inv))
      (CommRingCat.KaehlerDifferential.d b✝)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
U V W : Cᵒᵖ
i : U ⟶ V
j : V ⟶ W
x : ↑(M.obj U)
⊢ (ConcreteCategory.hom
        (M.map i ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map i))).map (M.map j) ≫
            (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map i)) (RingCat.Hom.hom (R.map j))
                    (RingCat.Hom.hom (R.map (i ≫ j))) ⋯).inv.app
              (M.obj W)))
      x =
    (ConcreteCategory.hom (M.map j)) ((ConcreteCategory.hom (M.map i)) x)

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
U V W : Cᵒᵖ
i : U ⟶ V
j : V ⟶ W
x : ↑(M.obj U)
⊢ (ConcreteCategory.hom
        (M.map i ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map i))).map (M.map j) ≫
            (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map i)) (RingCat.Hom.hom (R.map j))
                    (RingCat.Hom.hom (R.map (i ≫ j))) ⋯).inv.app
              (M.obj W)))
      x =
    (ConcreteCategory.hom (M.map j)) ((ConcreteCategory.hom (M.map i)) x)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f g : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), f.app X = g.app X
x✝ : Cᵒᵖ
⊢ f.app x✝ = g.app x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f g : M₁ ⟶ M₂
h : ∀ (X : Cᵒᵖ), f.app X = g.app X
x✝ : Cᵒᵖ
⊢ f.app x✝ = g.app x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ X✝ Y✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
X Y : Cᵒᵖ
g : X ⟶ Y
x : ↑(X✝.presheaf.obj X)
⊢ (AddCommGrpCat.Hom.hom
        (X✝.presheaf.map g ≫ AddCommGrpCat.ofHom (AddMonoidHom.mk' ⇑(ConcreteCategory.hom (f.app Y)) ⋯)))
      x =
    (AddCommGrpCat.Hom.hom
        (AddCommGrpCat.ofHom (AddMonoidHom.mk' ⇑(ConcreteCategory.hom (f.app X)) ⋯) ≫ Y✝.presheaf.map g))
      x

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ X✝ Y✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
X Y : Cᵒᵖ
g : X ⟶ Y
x : ↑(X✝.presheaf.obj X)
⊢ (AddCommGrpCat.Hom.hom
        (X✝.presheaf.map g ≫ AddCommGrpCat.ofHom (AddMonoidHom.mk' ⇑(ConcreteCategory.hom (f.app Y)) ⋯)))
      x =
    (AddCommGrpCat.Hom.hom
        (AddCommGrpCat.ofHom (AddMonoidHom.mk' ⇑(ConcreteCategory.hom (f.app X)) ⋯) ≫ Y✝.presheaf.map g))
      x
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✝ c✝ : M₁ ⟶ M₂
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ b✝ c✝ : M₁ ⟶ M₂
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
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✝ c✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ (a✝ + b✝ + c✝).app X✝ = (a✝ + (b✝ + c✝)).app X✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ b✝ c✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ (a✝ + b✝ + c✝).app X✝ = (a✝ + (b✝ + c✝)).app X✝
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✝ : M₁ ⟶ M₂
⊢ 0 + a✝ = a✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ : M₁ ⟶ M₂
⊢ 0 + a✝ = a✝
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✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ (0 + a✝).app X✝ = a✝.app X✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ (0 + a✝).app X✝ = a✝.app X✝
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✝ : M₁ ⟶ M₂
⊢ a✝ + 0 = a✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ : M₁ ⟶ M₂
⊢ a✝ + 0 = a✝
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✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ (a✝ + 0).app X✝ = a✝.app X✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ (a✝ + 0).app X✝ = a✝.app X✝
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:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ b✝ : M₁ ⟶ M₂
⊢ a✝ - b✝ = a✝ + -b✝
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₂
X✝ : Cᵒᵖ
⊢ (a✝ - b✝).app X✝ = (a✝ + -b✝).app X✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ b✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ (a✝ - b✝).app X✝ = (a✝ + -b✝).app X✝
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✝ : M₁ ⟶ M₂
⊢ -a✝ + a✝ = 0

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ : M₁ ⟶ M₂
⊢ -a✝ + a✝ = 0
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✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ (-a✝ + a✝).app X✝ = Hom.app 0 X✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ (-a✝ + a✝).app X✝ = Hom.app 0 X✝
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✝ = b✝ + a✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ b✝ : M₁ ⟶ M₂
⊢ a✝ + b✝ = b✝ + a✝
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₂
X✝ : Cᵒᵖ
⊢ (a✝ + b✝).app X✝ = (b✝ + a✝).app X✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ b✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ (a✝ + b✝).app X✝ = (b✝ + a✝).app X✝
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₂
X✝ : Cᵒᵖ
⊢ a✝.app X✝ + b✝.app X✝ = b✝.app X✝ + a✝.app X✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ b✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ a✝.app X✝ + b✝.app X✝ = b✝.app X✝ + a✝.app X✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
s t : M.sections
h : ∀ (X : Cᵒᵖ), ↑s X = ↑t X
x✝ : Cᵒᵖ
⊢ ↑s x✝ = ↑t x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
s t : M.sections
h : ∀ (X : Cᵒᵖ), ↑s X = ↑t X
x✝ : Cᵒᵖ
⊢ ↑s x✝ = ↑t x✝
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✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (M.map f✝)) ((ConcreteCategory.hom (f.app X✝)) 1) = (ConcreteCategory.hom (f.app Y✝)) 1

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
f : unit R ⟶ M
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (M.map f✝)) ((ConcreteCategory.hom (f.app X✝)) 1) = (ConcreteCategory.hom (f.app Y✝)) 1
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (f b) = X (g b)

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (f b) = X (g b)
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (g b) = X (f b)

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
f g : β → γ
h : f = g
X : GradedObject γ C
b : β
⊢ X (g b) = X (f b)
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x✝ : β
⊢ x✝ = (⇑e.symm ∘ ⇑e) x✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x✝ : β
⊢ x✝ = (⇑e.symm ∘ ⇑e) x✝
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x✝ : γ
⊢ (⇑e ∘ ⇑e.symm) x✝ = x✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
x✝ : γ
⊢ (⇑e ∘ ⇑e.symm) x✝ = x✝
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (m + n) • s = ((fun b ↦ b + m • s) ∘ fun b ↦ b + n • s) x✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (m + n) • s = ((fun b ↦ b + m • s) ∘ fun b ↦ b + n • s) x✝
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (m + n) • s = x✝ + n • s + m • s

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
inst✝ : AddCommGroup β
s : β
m n : ℤ
x✝ : β
⊢ x✝ + (m + n) • s = x✝ + n • s + m • s
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 : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ (if i = j then X✝ else 0) = X✝

Tactic:
;

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 : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ (if i = j then X✝ else 0) = X✝
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 : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ Y✝ = if i = j then Y✝ else 0

Tactic:
;

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 : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ Y✝ = if i = j then Y✝ else 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
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    (add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
n : A
X : C
⊢ (F (0 + n)).obj X = (F n).obj X

Tactic:
;

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    (add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
n : A
X : C
⊢ (F (0 + n)).obj X = (F n).obj X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    (add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
zero_add_hom_app : ∀ (n : A) (X : C), (add 0 n).hom.app X = eqToHom ⋯ ≫ (F n).map (zero.inv.app X)
n : A
X : C
⊢ (F (n + 0)).obj X = (F n).obj X

Tactic:
;

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    (add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
zero_add_hom_app : ∀ (n : A) (X : C), (add 0 n).hom.app X = eqToHom ⋯ ≫ (F n).map (zero.inv.app X)
n : A
X : C
⊢ (F (n + 0)).obj X = (F n).obj X
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 ι
A : V
i : ι
⊢ ((single V c i).obj A).X i = A

Tactic:
;

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
A : V
i : ι
⊢ ((single V c i).obj A).X i = A
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.F n).obj X = (h.F (0 + n)).obj X

Tactic:
;

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.F n).obj X = (h.F (0 + n)).obj X
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.F n).obj X = (h.F (n + 0)).obj X

Tactic:
;

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.F n).obj X = (h.F (n + 0)).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
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₃ : ι
⊢ (K.XIsoOfEq ⋯).hom ≫ K.d p₁ p₃ = K.d p₁ p₃

Tactic:
;

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₃ : ι
⊢ (K.XIsoOfEq ⋯).hom ≫ K.d p₁ p₃ = K.d p₁ p₃