mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
a : A
⊢ (shiftFunctorComm C a 0).hom.app X =
    (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor C a).map ((shiftFunctorZero C A).inv.app X)

Tactic:
by

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
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i j : ι
⊢ PreservesColimitsOfShape J (single C c i ⋙ eval C c j)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ S.ShortExact ↔ ∀ (i : ι), (S.map (eval C c i)).ShortExact

Tactic:
by

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
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i : ι
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesLimitsOfShape J (single C c i)

Tactic:
by

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
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i : ι
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesColimitsOfShape J (single C c i)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
i j : ι
I : C
inst✝ : Injective I
⊢ Injective (((single C c i).obj I).X j)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
inst✝¹ : Linear R C
inst✝ : Linear R D
ι : Type u_4
c : ComplexShape ι
X✝ Y✝ X Y : HomologicalComplex C c
x✝² x✝¹ : R
x✝ : X ⟶ Y
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
inst✝¹ : Linear R C
inst✝ : Linear R D
ι : Type u_4
c : ComplexShape ι
X✝ Y✝ X Y : HomologicalComplex C c
a : X ⟶ Y
⊢ 1 • a = a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
inst✝¹ : Linear R C
inst✝ : Linear R D
ι : Type u_4
c : ComplexShape ι
X✝ Y✝ X Y : HomologicalComplex C c
⊢ ∀ (a : R), a • 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
inst✝¹ : Linear R C
inst✝ : Linear R D
ι : Type u_4
c : ComplexShape ι
X✝ Y✝ X Y : HomologicalComplex C c
⊢ ∀ (a : R) (x y : X ⟶ Y), a • (x + y) = a • x + a • y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
inst✝¹ : Linear R C
inst✝ : Linear R D
ι : Type u_4
c : ComplexShape ι
X✝ Y✝ X Y : HomologicalComplex C c
x✝² x✝¹ : R
x✝ : X ⟶ Y
⊢ (x✝² + x✝¹) • x✝ = x✝² • x✝ + x✝¹ • x✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
inst✝¹ : Linear R C
inst✝ : Linear R D
ι : Type u_4
c : ComplexShape ι
X✝ Y✝ X Y : HomologicalComplex C c
⊢ ∀ (x : X ⟶ Y), 0 • x = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
i j : ι
P : C
inst✝ : Projective P
⊢ Projective (((single C c i).obj P).X j)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝² : HasFiniteLimits C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits F
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesLimitsOfShape J (F.mapHomologicalComplex c)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝² : HasFiniteColimits C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesFiniteColimits F
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesColimitsOfShape J (F.mapHomologicalComplex c)

Tactic:
by

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
m₁ m₂ m₃ : A
X : C
⊢ m₂ + m₁ + m₃ = m₁ + (m₂ + m₃)

Tactic:
by

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
m₁ m₂ m₃ : A
X : C
⊢ (shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫ (shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X) =
    (shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X) ≫
      (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X) ≫
        (shiftFunctorComm C m₁ m₃).hom.app ((shiftFunctor C m₂).obj X)

Tactic:
by

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
X✝ Y : C
f : X✝ ⟶ Y
m n : A
hmn : m + n = 0
X : C
⊢ n + m = 0

Tactic:
by

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
m n : A
hmn : m + n = 0
X : C
⊢ (shiftFunctorComm C m n).hom.app X =
    (shiftFunctorCompIsoId C m n hmn).hom.app X ≫ (shiftFunctorCompIsoId C n m ⋯).inv.app X

Tactic:
by

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
m n : A
hmn : m + n = 0
X : C
⊢ (shiftFunctorComm C m n).inv.app X =
    (shiftFunctorCompIsoId C n m ⋯).hom.app X ≫ (shiftFunctorCompIsoId C m n hmn).inv.app X

Tactic:
by

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
X : C
⊢ F.map ((zero hF s i).hom.app X) = (i 0).hom.app X ≫ (shiftFunctorZero D A).hom.app (F.obj X)

Tactic:
by

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
⊢ (Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f =
      IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) ↔
    (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S

Tactic:
by

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
X : C
⊢ F.map ((zero hF s i).inv.app X) = (shiftFunctorZero D A).inv.app (F.obj X) ≫ (i 0).inv.app X

Tactic:
by

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map ((add hF s i a b).hom.app X) =
    (i (a + b)).hom.app X ≫
      (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ (shiftFunctor D b).map ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map ((add hF s i a b).inv.app X) =
    (i b).hom.app ((s a).obj X) ≫
      (shiftFunctor D b).map ((i a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X

Tactic:
by

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
inst✝ : EssFiniteType R S
x : S
I : Ideal (S ⊗[R] S) := Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))
⊢ (IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeRight =
    (IsScalarTower.toAlgHom R (S ⊗[R] S) (S ⊗[R] S ⧸ I)).comp TensorProduct.includeLeft

Tactic:
by

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
inst✝ : EssFiniteType R S
⊢ (ideal R S).FG

Tactic:
by

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
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x : S
⊢ ∀ x ∈ adjoin R ↑(EssFiniteType.finset R S), (D R S) x ∈ Submodule.span S ↑s

Tactic:
by

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
⊢ F.map ((add hF s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯ ≫ (add hF s i m₁ (m₂ + m₃)).hom.app X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X))

Tactic:
by

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
inst✝ : EssFiniteType R S
⊢ Module.Finite S Ω[S⁄R]

Tactic:
by

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 y z : S
⊢ (z𝖣x + y) = (z𝖣x) + z𝖣y

Tactic:
by

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
⊢ F.map ((add hF s i 0 n).hom.app X) = F.map (eqToHom ⋯ ≫ (s n).map ((zero hF s i).inv.app X))

Tactic:
by

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
⊢ F.map ((add hF s i n 0).hom.app X) = F.map (eqToHom ⋯ ≫ (zero hF s i).inv.app ((s n).obj X))

Tactic:
by

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 y z : S
⊢ (z𝖣x * y) = ((z * x)𝖣y) + (z * y)𝖣x

Tactic:
by

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 : R
y : S
⊢ (y𝖣(algebraMap R S) x) = 0

Tactic:
by

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 : S
⊢ (x𝖣1) = 0

Tactic:
by

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
r : R
x y : S
⊢ (y𝖣r • x) = r • y𝖣x

Tactic:
by

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
a b : S
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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
⊢ (derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S) = (kerTotal R S).mkQ

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : c.prev j = i
hk : c.next j = k
K : HomologicalComplex C c
⊢ (K.XIsoOfEq hi).hom ≫ ((shortComplexFunctor' C c i j k).obj K).f =
    ((shortComplexFunctor C c j).obj K).f ≫ (Iso.refl ((shortComplexFunctor C c j).obj K).X₂).hom

Tactic:
by

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
⊢ (linearCombination S ⇑(D R S)).ker = kerTotal R S

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : c.prev j = i
hk : c.next j = k
K : HomologicalComplex C c
⊢ (Iso.refl ((shortComplexFunctor C c j).obj K).X₂).hom ≫ ((shortComplexFunctor' C c i j k).obj K).g =
    ((shortComplexFunctor C c j).obj K).g ≫ (K.XIsoOfEq hk).hom

Tactic:
by

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
⊢ Function.Surjective ⇑(linearCombination S ⇑(D R S))

Tactic:
by

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
⊢ Function.LeftInverse (⇑(derivationQuotKerTotal R S).liftKaehlerDifferential)
    ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y),
    (shortComplexFunctor C c j).map f ≫
        (ShortComplex.isoMk (Y.XIsoOfEq hi) (Iso.refl ((shortComplexFunctor C c j).obj Y).X₂) (Y.XIsoOfEq hk) ⋯ ⋯).hom =
      (ShortComplex.isoMk (X.XIsoOfEq hi) (Iso.refl ((shortComplexFunctor C c j).obj X).X₂) (X.XIsoOfEq hk) ⋯ ⋯).hom ≫
        (shortComplexFunctor' C c i j k).map f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
⊢ k ≫ (K.sc i).g = 0

Tactic:
by

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
⊢ Function.RightInverse (⇑(derivationQuotKerTotal R S).liftKaehlerDifferential)
    ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
⊢ K.liftCycles k j hj hk ≫ K.iCycles i = k

Tactic:
by

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
⊢ (↑(quotKerTotalEquiv R S).symm).compDer (D R S) = derivationQuotKerTotal R S

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst✝ : K.HasHomology i
hj : c.next i = j
⊢ IsLimit (KernelFork.ofι (K.iCycles i) ⋯)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst✝ : K.HasHomology i
⊢ Mono (K.iCycles i)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst✝ : K.HasHomology i
⊢ Epi (K.homologyπ i)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
inst✝ : K.HasHomology k
⊢ K.d i j ≫ K.toCycles j k = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ (α ≫ k) ≫ K.d i j = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A' A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
α : A' ⟶ A
⊢ α ≫ K.liftCycles k j hj hk = K.liftCycles (α ≫ k) j hj ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
⊢ k ≫ K.d i j = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ k ≫ K.d i j = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ K.liftCycles k j hj ⋯ = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
⊢ K.liftCycles k j hj ⋯ ≫ K.homologyπ i = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology j
⊢ K.d i j = 𝟙 (K.X i) ≫ K.d i j

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
hi : c.prev j = i
inst✝ : K.HasHomology j
⊢ IsColimit (CokernelCofork.ofπ (K.homologyπ j) ⋯)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
⊢ (K.sc i).f ≫ k = 0

Tactic:
by

Goal state after: