mathlib-initiative/mathlib-tactics huggingface dataset:
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)
      ((ModuleCat.Hom.hom ((relativeDifferentials' φ').map f)) (CommRingCat.KaehlerDifferential.d b)) =
    (ModuleCat.Hom.hom (M'.map f)) ((ModuleCat.Hom.hom (d'.app X).desc) (CommRingCat.KaehlerDifferential.d b))

Tactic:
ModuleCat.Derivation.desc_d,

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
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)
      ((ModuleCat.Hom.hom ((relativeDifferentials' φ').map f)) (CommRingCat.KaehlerDifferential.d b)) =
    (ModuleCat.Hom.hom (M'.map f)) ((d'.app X).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:
rfl

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

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

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
    ext x
    exact CategoryTheory.congr_fun (φ.naturality f) x

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)
⊢ (ConcreteCategory.hom (n • (toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).map f)) x = (ModuleCat.Hom.hom (n • f.app X)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : Type u_1
x : GradedObject I C
i : I
⊢ eqToHom ⋯ i = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β : Type w
X : β → C
b : β
⊢ eqToHom ⋯ b = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y : GradedObject I C
p : I → J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
φ₁ : X ⟶ Y
⊢ mapMap φ₁ p = mapMap φ₁ p

Tactic:
rfl

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
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : A ⟶ B
⊢ eqToHom ⋯ ≫ f ≫ eqToHom ⋯ = (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv

Tactic:
rfl

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
h_X : C₁.X = C₂.X
h_d : ∀ (i j : ι), c.Rel i j → C₁.d i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ C₂.d i j
⊢ C₁ = C₂

Tactic:
obtain ⟨X₁, d₁, s₁, h₁⟩ := C₁

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₂ : HomologicalComplex V c
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
h_X : { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.X = C₂.X
h_d :
  ∀ (i j : ι), c.Rel i j → { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.d i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ C₂.d i j
⊢ { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ } = C₂
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x✝ y✝ : S ⊗[R] S
x₁ x₂ x y : S
⊢ (x₁ * x) • (x₂ • D y + y • D x₂) = (x₁ * x₂) • x • D y + (x * y) • x₁ • D x₂

Tactic:
simp only [smul_smul, smul_add, mul_comm (x * y) x₁, mul_right_comm x₁ x₂, ← mul_assoc]

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
m₁ m₂ m₃ : A
X : C
⊢ 𝟙 ((h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X)) = 𝟙 ((h.F m₂ ⋙ h.F m₃).obj ((h.F m₁).obj X))

Tactic:
rfl

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₁ : HomologicalComplex V c
n : ι
⊢ (eqToHom ⋯).f n = eqToHom ⋯

Tactic:
rfl

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
ι : 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
⊢ φ ≫ (singleObjXIsoOfEq c j A j ⋯).inv = φ ≫ (singleObjXSelf c j A).inv

Tactic:
rfl

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ eqToHom ⋯ ≫ (shiftFunctorAdd C 0 a).hom.app X =
    eqToHom ⋯ ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) (MonoidalCategoryStruct.tensorUnit (Discrete A)) { as := a }).app X

Tactic:
rfl

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ eqToHom ⋯ ≫ (shiftFunctorAdd C a 0).hom.app x✝ =
    eqToHom ⋯ ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a } (MonoidalCategoryStruct.tensorUnit (Discrete A))).app x✝

Tactic:
rfl

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ eqToHom ⋯ ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ }
              (MonoidalCategoryStruct.tensorObj { as := a₂ } { as := a₃ })).app
          X ≫
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
          (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X) =
    eqToHom ⋯ ≫
      (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ + a₃ }).app X ≫
        (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₂ } { as := a₃ }).app
          (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)

Tactic:
rfl

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
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
⊢ (singleObjXIsoOfEq c j A j ⋯).hom ≫ φ = (singleObjXSelf c j A).hom ≫ φ

Tactic:
rfl

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : C.X 0 ⟶ X
n : ℕ
⊢ ((C.toSingle₀Equiv X).symm f).f (n + 1) = 0

Tactic:
rfl

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

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx✝ : x✝ ∈ ideal R S
hx : x✝ ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
x : S
⊢ (fromIdeal R S) ⟨(fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x, ⋯⟩ ∈ Set.range ⇑(D R S)

Tactic:
exact ⟨x, KaehlerDifferential.DLinearMap_apply R S x⟩

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

Goal state before:
pp: case e'_2.e'_6.e'_8.e'_7.e'_5
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
X✝ : C
e_1✝ :
  ((shiftFunctor C i).obj X✝ ⟶ (shiftFunctor C i).obj X✝) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
              ⋯).functor.obj
        X✝ ⟶
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
              ⋯).functor.obj
        X✝)
e_3✝ :
  (shiftFunctor C i).obj X✝ =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
            ⋯).functor.obj
      X✝
e_4✝¹ :
  (shiftFunctor C i).obj ((shiftFunctor C j).obj ((shiftFunctor C i).obj X✝)) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
            ⋯).functor.obj
      ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso ⋯) ⋯).inverse.obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso ⋯) ⋯).functor.obj
          X✝))
e_7✝ :
  (shiftFunctor C j).obj ((shiftFunctor C i).obj X✝) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
            ⋯).inverse.obj
      ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso ⋯) ⋯).functor.obj
        X✝)
e_6✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).inverse
e_4✝ :
  shiftFunctor C i ⋙ shiftFunctor C j =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).functor ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).inverse
X : C
⊢ (shiftFunctorZero C A).inv.app X ≫ (eqToHom ⋯).app X ≫ (shiftFunctorAdd C i j).hom.app X =
    (LaxMonoidal.ε (shiftMonoidalFunctor C A)).app X ≫
      (eqToHom ⋯).app X ≫ (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := i } { as := j }).app X

Tactic:
rfl

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 : C₁ ⟶ C₂
inst✝ : IsIso f
j : ι
⊢ (inv f).f j = inv (f.f j)

Tactic:
apply IsIso.eq_inv_of_inv_hom_id
  simp [← comp_f]

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

Goal state before:
pp: case e'_2.e'_7.e'_7.e'_5
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
X✝ : C
e_1✝ :
  ((shiftFunctor C i).obj X✝ ⟶ (shiftFunctor C i).obj X✝) =
    ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
              ⋯).functor.obj
        X✝ ⟶
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
              ⋯).functor.obj
        X✝)
e_4✝ :
  (shiftFunctor C i).obj ((shiftFunctor C j).obj ((shiftFunctor C i).obj X✝)) =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
            ⋯).functor.obj
      ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
              (Discrete.eqToIso ⋯) ⋯).inverse.obj
        ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h)
                (Discrete.eqToIso ⋯) ⋯).functor.obj
          X✝))
e_5✝¹ :
  (shiftFunctor C i).obj X✝ =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
            ⋯).functor.obj
      X✝
e_5✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).functor
e_3✝ :
  shiftFunctor C j ⋙ shiftFunctor C i =
    (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).inverse ⋙
      (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯)
          ⋯).functor
X : C
⊢ (shiftFunctorAdd C j i).inv.app X ≫ (eqToHom ⋯).app X ≫ (shiftFunctorZero C A).hom.app X =
    (LaxMonoidal.μ (shiftMonoidalFunctor C A) { as := j } { as := i }).app X ≫
      (eqToHom ⋯).app X ≫ (OplaxMonoidal.η (shiftMonoidalFunctor C A)).app X

Tactic:
rfl

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
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S : ShortComplex V
⊢ (succ S).fst = (succ S).fst

Tactic:
rfl

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
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S : ShortComplex V
⊢ S.X₁ = S.X₁

Tactic:
rfl

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✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ 𝟙 ((shiftFunctor C n).obj ((𝟭 C).obj X)) = 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X))

Tactic:
rfl

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
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) = (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).fst

Tactic:
rfl

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

Goal state before:
pp: case neg
ι : 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
⊢ 0 ≫ 0 = 𝟙 (((single W₂ c j).obj (F.obj X)).X i)

Tactic:
apply (isZero_single_obj_X c j _ _ h).eq_of_src

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
eq :
  (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst =
    eqToHom ⋯ ≫
      (succ
            { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
              X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
              g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).snd.fst
⊢ n + 3 = n + 2 + 1

Tactic:
rfl

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
eq :
  (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst =
    eqToHom ⋯ ≫
      (succ
            { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
              X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
              g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).snd.fst
⊢ (mkAux X₀ X₁ X₂ d₀ d₁ s succ (n + 2)).g = (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst

Tactic:
rfl

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

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

Tactic:
← shiftFunctorAdd'_add_zero_hom_app,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map ((shiftFunctorAdd' C n' 0 n' ⋯).hom.app X ≫ (shiftFunctorAdd' C n' 0 n' ⋯).inv.app X) ≫
        (shiftFunctorAdd' C n' n 0 ⋯).inv.app X
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
i j : A
⊢ shiftFunctorComm C i j = (shiftFunctorAdd C i j).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯

Tactic:
rfl

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✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ ((shiftFunctorAdd' C i j (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯).inv =
    ((shiftFunctorAdd' C j i (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C i j (i + j) ⋯).hom

Tactic:
rfl

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
x : ↥(ideal R S)
⊢ LinearMap.id ((ideal R S).toCotangent x) = (ideal R S).toCotangent x

Tactic:
rfl

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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : S
⊢ (AlgHom.id R S) x = x

Tactic:
rfl

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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
this : Function.RightInverse ⇑TensorProduct.includeLeft ⇑↑(TensorProduct.lmul' R)
x✝ : S ⊗[R] S
⊢ x✝ ∈ ideal R S ↔ x✝ ∈ RingHom.ker ↑(TensorProduct.lmul' R)

Tactic:
rfl

Goal state after:
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
⊢ colimMap { app := fun j ↦ (F.obj j).d n m, naturality := ⋯ } = 0

Tactic:
by
        ext j
        rw [ι_colimMap]
        dsimp
        rw [(F.obj j).shape _ _ h, zero_comp, comp_zero]

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
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
y : S ⊗[R] S
⊢ (TensorProduct.lmul' R).kerSquareLift ((Ideal.Quotient.mk (ideal R S ^ 2)) y) =
    (quotientCotangentIdealRingEquiv R S)
      ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) ((Ideal.Quotient.mk (ideal R S ^ 2)) y))

Tactic:
rfl

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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : S →₀ S
this : (derivationQuotKerTotal R S).liftKaehlerDifferential ((linearCombination S ⇑(D R S)) x) = (kerTotal R S).mkQ x
⊢ ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun ((kerTotal R S).mkQ x) =
    (linearCombination S ⇑(D R S)) x

Tactic:
rfl

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

Goal state before:
pp: case e'_4.e'_4
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A (Set.range fun x ↦ single ((algebraMap A B) ((algebraMap R A) x)) 1) ≤
    Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1)

Tactic:
apply Submodule.span_mono

Goal state after:
case e'_4.e'_4
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ (Set.range fun x ↦ single ((algebraMap A B) ((algebraMap R A) x)) 1) ⊆ Set.range fun x ↦ single ((algebraMap S B) x) 1