mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Ideal R
__spread✝⁻⁰ : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯
x : ↥I
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I I ⋯)) ⋯) (I.toCotangent x)) =
    I.toCotangent x

Tactic:
simp

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
k : ℕ
⊢ I ^ k • ⊤ = (I.stableFiltration ⊤).N k

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Submodule.span R (⇑(maximalIdeal R).toCotangent '' s) = Submodule.restrictScalars R ⊤ ↔
    Submodule.map (maximalIdeal R).toCotangent (Submodule.span R s) = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr.zero
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : ↑r • x = x
⊢ x ∈ I ^ 0 • ⊤

Tactic:
simp

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✝ : IsDomain R
h : I ≠ ⊤
x✝ : ℕ
⊢ I ^ x✝ = I ^ x✝ • ⊤

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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ᵒᵖ
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:
simp

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✝
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:
simp

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 (d'.app Y).desc) (CommRingCat.KaehlerDifferential.d ((ConcreteCategory.hom (R.map f)) b)) =
    (ModuleCat.Hom.hom (M'.map f)) (d'.d b)

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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ᵒᵖ
x : ↑(M₁.obj X)
⊢ (ModuleCat.Hom.hom ((n • f).app X)) x = (ModuleCat.Hom.hom (n • f.app X)) x

Tactic:
change (toPresheaf R ⋙ (evaluation _ _).obj X).map (n • f) x = _

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : ↑(M₁.obj X)
⊢ (ConcreteCategory.hom ((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).map (n • f))) x =
    (ModuleCat.Hom.hom (n • f.app X)) 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
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:
simp

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
⊢ (ConcreteCategory.hom (R.map f)) 1 • s.eval Y = (ConcreteCategory.hom (M.map f)) (1 • s.eval X)

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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.map (𝟙 n)).app ((F.obj m).obj X) ≫ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X

Tactic:
simp

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.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map (𝟙 m)).app X) ≫ (μ F m n').app X

Tactic:
simp

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
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((η F).app X ≫ (ε F).app X) =
    ((μ F (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X) ≫ (F.obj n).map ((ε F).app X)

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

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₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) =
    (F.obj m₃).map ((μ F m₁ m₂).app X) ≫
      (μ F (m₁ ⊗ m₂) m₃).app X ≫
        (F.map (α_ m₁ m₂ m₃).hom).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (δ F (m₁ ⊗ m₂) m₃).app X

Tactic:
simp

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₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (m₂ ⊗ m₃)).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (δ F (m₁ ⊗ m₂) m₃).app X

Tactic:
rw [← associativity_app_assoc]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
s : Cofan (X.mapObjFun r k)
x✝ : ↑(r ⁻¹' {k})
i : I
hi : r i = k
⊢ (Cofan.inj (X.cofanMapObjComp p q r hpqr k c c') ⟨i, hi⟩ ≫
      Cofan.IsColimit.desc hc' fun x ↦
        match x with
        | ⟨j, hj⟩ =>
          Cofan.IsColimit.desc (hc j hj) fun x ↦
            match x with
            | ⟨i, hi⟩ => s.inj ⟨i, ⋯⟩) =
    s.inj ⟨i, hi⟩

Tactic:
simp

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 : M
X Y : C
f : X ⟶ (F.obj m).obj Y
inst✝ : F.Monoidal
⊢ ((ε F).app X ≫ (F.obj (𝟙_ M)).map f ≫ (μ F m (𝟙_ M)).app Y) ≫ (δ F m (𝟙_ M)).app Y =
    ((ε F).app X ≫ (η F).app X ≫ f ≫ (F.map (ρ_ m).inv).app Y) ≫ (δ F m (𝟙_ M)).app Y

Tactic:
simp

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₁ m₂ : M
X : C
inst✝ : F.Monoidal
⊢ (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (δ F (m₁ ⊗ 𝟙_ M) m₂).app X =
    (F.obj m₂).map ((η F).app ((F.obj m₁).obj X) ≫ (F.map (ρ_ m₁).inv).app X)

Tactic:
simp

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

Goal state before:
pp: case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
A : V
i✝ : ι
⊢ eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ = 𝟙 (if i✝ = i✝ then A else 0)

Tactic:
simp

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

Goal state before:
pp: case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
X✝ Y✝ Z✝ : V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : ι
⊢ eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ = (eqToHom ⋯ ≫ f ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ g ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
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 ι
j : ι
X✝ Y✝ Z✝ : V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : ι
h : ¬i✝ = j
⊢ 0 = 0 ≫ 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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
h : ShiftMkCore C A
X X' : A
x✝ : C
⊢ (MonoidalCategoryStruct.whiskerRight ((Discrete.functor h.F).map { down := { down := ⋯ } })
            ((Discrete.functor h.F).obj { as := X' }) ≫
          (h.add { as := X }.as { as := X' }.as).symm.hom).app
      x✝ =
    ((h.add { as := X }.as { as := X' }.as).symm.hom ≫
          (Discrete.functor h.F).map (MonoidalCategoryStruct.whiskerRight { down := { down := ⋯ } } { as := X' })).app
      x✝

Tactic:
simp

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

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

Tactic:
simp

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
h : ShiftMkCore C A
X X' : A
x✝ : C
⊢ (MonoidalCategoryStruct.whiskerLeft ((Discrete.functor h.F).obj { as := X' })
            ((Discrete.functor h.F).map { down := { down := ⋯ } }) ≫
          (h.add { as := X' }.as { as := X }.as).symm.hom).app
      x✝ =
    ((h.add { as := X' }.as { as := X }.as).symm.hom ≫
          (Discrete.functor h.F).map (MonoidalCategoryStruct.whiskerLeft { as := X' } { down := { down := ⋯ } })).app
      x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n : ι
⊢ φ.f n ≫ (L.XIsoOfEq ⋯).hom = (K.XIsoOfEq ⋯).hom ≫ φ.f n

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n : ι
⊢ φ.f n ≫ (L.XIsoOfEq ⋯).inv = (K.XIsoOfEq ⋯).inv ≫ φ.f n

Tactic:
simp

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 : ChainComplex V ℕ
X : V
f : { f // C.d 1 0 ≫ f = 0 }
⊢ (fun φ ↦ ⟨φ.f 0, ⋯⟩) ((fun f ↦ HomologicalComplex.mkHomToSingle ↑f ⋯) f) = f

Tactic:
simp

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
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftAdd X i j).inv ≫ (shiftFunctor C (i + j)).map f ≫ (shiftAdd Y i j).hom

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i j : ι
hij : c.Rel i j
⊢ (f i).inv ≫ C₁.d i j = (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i j : ι
hij : c.Rel i j
⊢ (f i).inv ≫ ((f i).hom ≫ C₂.d i j) ≫ (f j).inv = C₂.d i j ≫ (f j).inv

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ (isoApp (isoOfComponents f hf) i).hom = (f i).hom

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
x : R
⊢ (D R S) ((algebraMap R S) x) ∈ ↑⊥

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁵ : Category.{v_2, u_3} W₁
inst✝⁴ : Category.{v_3, u_4} W₂
inst✝³ : HasZeroMorphisms W₁
inst✝² : HasZeroMorphisms W₂
c : ComplexShape ι
F G : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : G.PreservesZeroMorphisms
α : F ⟶ G
C D : HomologicalComplex W₁ c
f : C ⟶ D
⊢ (F.mapHomologicalComplex c).map f ≫ (mapHomologicalComplex α c).app D =
    (mapHomologicalComplex α c).app C ≫ (G.mapHomologicalComplex c).map f

Tactic:
simp

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

Goal state before:
pp: W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ ((F.mapHomologicalComplex (ComplexShape.down α)).obj (of X d sq)).d (j + 1) j ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (of (fun n ↦ F.obj (X n)) (fun n ↦ F.map (d n)) ⋯).d (j + 1) j

Tactic:
simp

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S : ShortComplex V
⊢ (succ S).snd.fst = eqToHom ⋯ ≫ (succ S).snd.fst ≫ eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: case pos
ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
h : i = j
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = 𝟙 (F.obj (((single W₁ c j).obj X).X i))

Tactic:
simp

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

Goal state before:
pp: case pos
ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i✝ : ι
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
i : ι
h : i = j
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = 𝟙 (((single W₂ c j).obj (F.obj X)).X i)

Tactic:
simp

Goal state after: