mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
P M✝ : ModuleCat R
inst✝ : Small.{v, u} R
M : ModuleCat R
e : Basis (↑M) R (↑M →₀ Shrink.{v, u} R) := { repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) }
⊢ Epi (↟((e.constr ℕ) id))

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ : ι
w : Relation.Comp c₁.Rel c₂.Rel i✝ j✝
w' : Relation.Comp c₁.Rel c₂.Rel i✝ j'✝
⊢ j✝ = j'✝

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ : ι
w : Relation.Comp c₁.Rel c₂.Rel i✝ j✝
w' : Relation.Comp c₁.Rel c₂.Rel i'✝ j✝
⊢ i✝ = i'✝

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
i : ι
⊢ Subsingleton { j // c.Rel i j }

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.next i = j

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
j : ι
hj : ∀ (k : ι), ¬c.Rel j k
⊢ ¬∃ j_1, c.Rel j j_1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
j : ι
hj : ¬c.Rel j (c.next j)
k : ι
hk' : c.Rel j k
⊢ c.Rel j (c.next j)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
R : Dᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
d d' : M.Derivation φ
h : d = d'
X : Dᵒᵖ
b : ↑(R.obj X)
⊢ d.d b = d'.d b

Tactic:
by

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
R : Dᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
d : M.Derivation φ
X : Dᵒᵖ
⊢ d.d 1 = 0

Tactic:
by

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 φ
f : M ⟶ N
X Y : Dᵒᵖ
g : X ⟶ Y
x : ↑(R.obj X)
⊢ ((ModuleCat.Hom.hom (f.app Y)).toAddMonoidHom.comp d.d) ((ConcreteCategory.hom (R.map g)) x) =
    (ConcreteCategory.hom (N.map g)) (((ModuleCat.Hom.hom (f.app X)).toAddMonoidHom.comp d.d) x)

Tactic:
by

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 φ
f : M ⟶ N
X : Cᵒᵖ
a : ↑(S.obj X)
⊢ ((ModuleCat.Hom.hom (f.app (F.op.obj X))).toAddMonoidHom.comp d.d) ((ConcreteCategory.hom (φ.app X)) a) = 0

Tactic:
by

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
this : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), h₁.desc d' = h₂.desc d'
⊢ h₁ = h₂

Tactic:
by

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
⊢ h₁ = h₂

Tactic:
by

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 : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)
d_map :
  ∀ ⦃X Y : Dᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(R.obj X)),
    (d Y).d ((ConcreteCategory.hom (R.map f)) x) = (ConcreteCategory.hom (M.map f)) ((d X).d x)
X : Dᵒᵖ
⊢ ∀ (a b : ↑(R.obj X)), (d X).d (a + b) = (d X).d a + (d X).d b

Tactic:
by

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
x✝ : Dᵒᵖ
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    (ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (𝟙 x✝))) ⋯).inv.app
      (CommRingCat.KaehlerDifferential (φ'.app x✝))

Tactic:
by

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
X✝ Y✝ Z✝ : Dᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ CommRingCat.KaehlerDifferential.map ⋯ =
    CommRingCat.KaehlerDifferential.map ⋯ ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map x✝¹))).map
          (CommRingCat.KaehlerDifferential.map ⋯) ≫
        (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map x✝¹))
                (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map x✝))
                (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (x✝¹ ≫ x✝))) ⋯).inv.app
          (CommRingCat.KaehlerDifferential (φ'.app Z✝))

Tactic:
by

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
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation' φ'
X Y : Dᵒᵖ
f : X ⟶ Y
b : ↑(R.obj X)
⊢ (ConcreteCategory.hom
        ((relativeDifferentials' φ').map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map (d'.app Y).desc))
      (CommRingCat.KaehlerDifferential.d b) =
    (ConcreteCategory.hom ((d'.app X).desc ≫ M'.map f)) (CommRingCat.KaehlerDifferential.d b)

Tactic:
by

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
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation' φ'
⊢ Derivation.postcomp (derivation' φ') { app := fun X ↦ (d'.app X).desc, naturality := ⋯ } = d'

Tactic:
by

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
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
α β : relativeDifferentials' φ' ⟶ M
h : Derivation.postcomp (derivation' φ') α = Derivation.postcomp (derivation' φ') β
⊢ α = β

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
m : ↑(M.obj X)
⊢ (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X Y : Cᵒᵖ
f g : X ⟶ Y
h : f = g
m : ↑(M.obj X)
⊢ (ConcreteCategory.hom (M.map f)) m = (ConcreteCategory.hom (M.map g)) m

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : Cᵒᵖ
⊢ (𝟙 M).app X = 𝟙 (M.obj X)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X
naturality :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    M₁.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).hom = (app X).hom ≫ M₂.map f
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ M₂.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).inv = (app X).inv ≫ M₁.map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ ∀ (a b : ↑((forget₂ (ModuleCat ↑(R.obj X✝)) Ab).1 (M.obj X✝))),
    (ConcreteCategory.hom (M.map f)) (a + b) = (ConcreteCategory.hom (M.map f)) a + (ConcreteCategory.hom (M.map f)) b

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
U V : Cᵒᵖ
f : U ⟶ V
r : ↑(R.obj U)
⊢ (M.obj U).smul r ≫ M.presheaf.map f = M.presheaf.map f ≫ (M.obj V).smul ((ConcreteCategory.hom (R.map f)) r)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ X✝ Y✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
X : Cᵒᵖ
⊢ ∀ (a b : ↑(X✝.obj X)),
    (ConcreteCategory.hom (f.app X)) (a + b) = (ConcreteCategory.hom (f.app X)) a + (ConcreteCategory.hom (f.app X)) b

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : Cᵒᵖ ⥤ Ab
inst✝ : (X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)
map_smul :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (x y : ↑(M.obj X)),
    (ConcreteCategory.hom (M.map f)) (x + y) = (ConcreteCategory.hom (M.map f)) x + (ConcreteCategory.hom (M.map f)) y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
φ : M₁.presheaf ⟶ M₂.presheaf
hφ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(M₁.obj X)),
    (ConcreteCategory.hom (φ.app X)) (r • m) = r • (ConcreteCategory.hom (φ.app X)) m
X : Cᵒᵖ
⊢ ∀ (x y : ↑(M₁.1 X)),
    (ConcreteCategory.hom (φ.app X)) (x + y) = (ConcreteCategory.hom (φ.app X)) x + (ConcreteCategory.hom (φ.app X)) y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
φ : M₁.presheaf ⟶ M₂.presheaf
hφ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(M₁.obj X)),
    (ConcreteCategory.hom (φ.app X)) (r • m) = r • (ConcreteCategory.hom (φ.app X)) m
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ M₁.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
        (ModuleCat.ofHom { toFun := ⇑(ConcreteCategory.hom (φ.app Y✝)), map_add' := ⋯, map_smul' := ⋯ }) =
    ModuleCat.ofHom { toFun := ⇑(ConcreteCategory.hom (φ.app X✝)), map_add' := ⋯, map_smul' := ⋯ } ≫ M₂.map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
⊢ M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (-f.app Y) = (-f.app X) ≫ M₂.map h

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
f g : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
⊢ M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y + g.app Y) =
    (f.app X + g.app X) ≫ M₂.map h

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
f g : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
⊢ M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y - g.app Y) =
    (f.app X - g.app X) ≫ M₂.map h

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a b c : M₁ ⟶ M₂), a + b + c = a + (b + c)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a : M₁ ⟶ M₂), 0 + a = a

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a : M₁ ⟶ M₂), a + 0 = a

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a b : M₁ ⟶ M₂), a - b = a + -b

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a : M₁ ⟶ M₂), -a + a = 0

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
⊢ ∀ (a b : M₁ ⟶ M₂), a + b = b + a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (x y : ↑(R.obj X)),
    (ConcreteCategory.hom (R.map f)) (x + y) = (ConcreteCategory.hom (R.map f)) x + (ConcreteCategory.hom (R.map f)) y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (m x : ↑(R.obj X)),
    (ConcreteCategory.hom (R.map f)) (m • x) = (RingHom.id ↑(R.obj X)) m • (ConcreteCategory.hom (R.map f)) x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ M N : PresheafOfModules R
f : M ⟶ N
s : M.sections
X Y : Cᵒᵖ
g : X ⟶ Y
⊢ (ConcreteCategory.hom (N.map g)) ((ConcreteCategory.hom (f.app X)) (↑s X)) = (ConcreteCategory.hom (f.app Y)) (↑s Y)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
f : unit R ⟶ M
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y),
    (ConcreteCategory.hom (M.map f_1)) ((ConcreteCategory.hom (f.app X)) 1) = (ConcreteCategory.hom (f.app Y)) 1

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (unit R).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
        (ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj Y) ℤ ↑(M.obj Y)).symm (↑s Y))) =
    ModuleCat.ofHom ((ringLmapEquivSelf ↑(R.obj X) ℤ ↑(M.obj X)).symm (↑s X)) ≫ M.map f

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
⊢ ∀ (x y : ↑(forgetToPresheafModuleCatObjObj X hX M Y)),
    (ConcreteCategory.hom (M.map f)) (x + y) = (ConcreteCategory.hom (M.map f)) x + (ConcreteCategory.hom (M.map f)) y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X : Cᵒᵖ
hX : Limits.IsInitial X
M : PresheafOfModules R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : ↑(R.obj X)
x : ↑(forgetToPresheafModuleCatObjObj X hX M Y)
⊢ (ConcreteCategory.hom (M.map f)) (r • x) = (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M.map f)) x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X✝ : Cᵒᵖ
hX✝ : Limits.IsInitial X✝
X : Cᵒᵖ
hX : Limits.IsInitial X
M N : PresheafOfModules R
f : M ⟶ N
Y : Cᵒᵖ
⊢ ∀ (x y : ↑((forgetToPresheafModuleCatObj X hX M).obj Y)),
    (ConcreteCategory.hom (f.app Y)) (x + y) = (ConcreteCategory.hom (f.app Y)) x + (ConcreteCategory.hom (f.app Y)) y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
X✝ : Cᵒᵖ
hX✝ : Limits.IsInitial X✝
X : Cᵒᵖ
hX : Limits.IsInitial X
M N : PresheafOfModules R
f : M ⟶ N
Y Z : Cᵒᵖ
g : Y ⟶ Z
⊢ (forgetToPresheafModuleCatObj X hX M).map g ≫
      ModuleCat.ofHom { toFun := ⇑(ConcreteCategory.hom (f.app Z)), map_add' := ⋯, map_smul' := ⋯ } =
    ModuleCat.ofHom { toFun := ⇑(ConcreteCategory.hom (f.app Y)), map_add' := ⋯, map_smul' := ⋯ } ≫
      (forgetToPresheafModuleCatObj X hX N).map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
X Y : C
f : X ⟶ Y
inst✝ : F.OplaxMonoidal
⊢ (η F).app X ≫ (𝟙_ (C ⥤ C)).map f = (η F).app X ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n : M
X Y : C
f : X ⟶ Y
inst✝ : F.OplaxMonoidal
⊢ (δ F m n).app X ≫ (F.obj n).map ((F.obj m).map f) = (F.obj (m ⊗ n)).map f ≫ (δ F m n).app Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ₘ g)).app X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' : M
f : m ⟶ m'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X = (μ F m n).app X ≫ (F.map (f ▷ n)).app X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n n' : M
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.map g).app ((F.obj m).obj X) ≫ (μ F m n').app X = (μ F m n).app X ≫ (F.map (m ◁ g)).app X

Tactic:
by

Goal state after: