mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
X✝ Y✝ Z✝ : V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { f := fun i ↦ if h : i = j then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ else 0, comm' := ⋯ } =
    { f := fun i ↦ if h : i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0, comm' := ⋯ } ≫
      { f := fun i ↦ if h : i = j then eqToHom ⋯ ≫ g ≫ eqToHom ⋯ else 0, comm' := ⋯ }

Tactic:
ext

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
X✝ Y✝ Z✝ : V
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : ι
⊢ { f := fun i ↦ if h : i = j then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ else 0, comm' := ⋯ }.f i✝ =
    ({ f := fun i ↦ if h : i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0, comm' := ⋯ } ≫
          { f := fun i ↦ if h : i = j then eqToHom ⋯ ≫ g ≫ eqToHom ⋯ else 0, comm' := ⋯ }).f
      i✝
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 : (single V c j).obj A ⟶ (single V c j).obj B
⊢ (single V c j).map ((singleObjXSelf c j A).inv ≫ f.f j ≫ (singleObjXSelf c j B).hom) = f

Tactic:
ext

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : (single V c j).obj A ⟶ (single V c j).obj B
⊢ ((single V c j).map ((singleObjXSelf c j A).inv ≫ f.f j ≫ (singleObjXSelf c j B).hom)).f j = f.f j
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
⊢ 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 =
    (h.add { as := X }.as { as := X' }.as).symm.hom ≫
      (Discrete.functor h.F).map (MonoidalCategoryStruct.whiskerRight { down := { down := ⋯ } } { as := X' })

Tactic:
ext

Goal state after:
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✝
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
⊢ 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 =
    (h.add { as := X' }.as { as := X }.as).symm.hom ≫
      (Discrete.functor h.F).map (MonoidalCategoryStruct.whiskerLeft { as := X' } { down := { down := ⋯ } })

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case refine_1
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
⊢ f = default

Tactic:
ext

Goal state after:
case refine_1
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
i✝ : ι
⊢ f.f i✝ = default.f i✝
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: case refine_2
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
⊢ f = default

Tactic:
ext

Goal state after:
case refine_2
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ f.f i✝ = default.f i✝
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
⊢ shiftFunctorAdd' C a 0 a ⋯ =
    (shiftFunctor C a).rightUnitor.symm ≪≫ (shiftFunctor C a).isoWhiskerLeft (shiftFunctorZero C A).symm

Tactic:
ext

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ (shiftFunctorAdd' C a 0 a ⋯).hom.app x✝ =
    ((shiftFunctor C a).rightUnitor.symm ≪≫ (shiftFunctor C a).isoWhiskerLeft (shiftFunctorZero C A).symm).hom.app x✝
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
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 = f i

Tactic:
ext

Goal state after:
ι : 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
Module: Mathlib.Algebra.Homology.Additive

Goal state before:
pp: ι : 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 : ι
F : V ⥤ W
inst✝¹ : F.Additive
c : ComplexShape ι
inst✝ : F.Faithful
K L : HomologicalComplex V c
f₁ f₂ : K ⟶ L
h : (F.mapHomologicalComplex c).map f₁ = (F.mapHomologicalComplex c).map f₂
⊢ f₁ = f₂

Tactic:
ext

Goal state after:
ι : 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 : ι
F : V ⥤ W
inst✝¹ : F.Additive
c : ComplexShape ι
inst✝ : F.Faithful
K L : HomologicalComplex V c
f₁ f₂ : K ⟶ L
h : (F.mapHomologicalComplex c).map f₁ = (F.mapHomologicalComplex c).map f₂
i✝ : ι
⊢ f₁.f i✝ = f₂.f i✝
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).map ((shiftFunctorCompIsoId C n m h).hom.app X) =
    (shiftFunctorCompIsoId C m n ⋯).hom.app ((shiftFunctor C n).obj X)

Tactic:
by
  dsimp [shiftFunctorCompIsoId]
  simpa only [Functor.map_comp, ← shiftFunctorAdd'_zero_add_inv_app n X,
    ← shiftFunctorAdd'_add_zero_inv_app n X]
    using shiftFunctorAdd'_assoc_inv_app n m n 0 0 n h
      (by rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]) (by rw [h, zero_add]) X

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

Goal state before:
pp: ι : 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₂
W : Type u_5
inst✝³ : Category.{v_4, u_5} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
inst✝ : DecidableEq ι
j : ι
x✝¹ x✝ : W
f g : x✝¹ ⟶ x✝
⊢ (single W c j).map (f + g) = (single W c j).map f + (single W c j).map g

Tactic:
ext

Goal state after:
ι : 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₂
W : Type u_5
inst✝³ : Category.{v_4, u_5} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
inst✝ : DecidableEq ι
j : ι
x✝¹ x✝ : W
f g : x✝¹ ⟶ x✝
⊢ ((single W c j).map (f + g)).f j = ((single W c j).map f + (single W c j).map g).f j
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 : A
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorCompIsoId C n (-n) ⋯).inv.app X) =
    (shiftFunctorCompIsoId C (-n) n ⋯).inv.app ((shiftFunctor C n).obj X)

Tactic:
apply shift_shiftFunctorCompIsoId_inv_app

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 : A
X : C
⊢ (shiftFunctor C (-n)).map ((shiftFunctorCompIsoId C (-n) n ⋯).inv.app X) =
    (shiftFunctorCompIsoId C n (-n) ⋯).inv.app ((shiftFunctor C (-n)).obj X)

Tactic:
apply shift_shiftFunctorCompIsoId_inv_app

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
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
i i' : ι
x✝ : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (hs k).lift ((eval C c k).mapCone t) ≫ (s.π.app j).f k = (t.π.app j).f k
⊢ (hs i).lift ((eval C c i).mapCone t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' = t.pt.d i i' ≫ (t.π.app j).f i'

Tactic:
← Hom.comm,

Goal state after:
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
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
i i' : ι
x✝ : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (hs k).lift ((eval C c k).mapCone t) ≫ (s.π.app j).f k = (t.π.app j).f k
⊢ (hs i).lift ((eval C c i).mapCone t) ≫ (s.π.app j).f i ≫ (F.obj j).d i i' = t.pt.d i i' ≫ (t.π.app j).f i'
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
i j : A
⊢ (shiftComm X i j).symm = shiftComm X j i

Tactic:
ext

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
i j : A
⊢ (shiftComm X i j).symm.hom = (shiftComm X j i).hom
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)
⊢ ideal R S = RingHom.ker ↑(TensorProduct.lmul' R)

Tactic:
ext

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

Tactic:
constructor

Goal state after:
case mp
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
e₁ :
  (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S)
      ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)
⊢ ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
      (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x →
    ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x

case mpr
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
e₁ :
  (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S)
      ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)
⊢ ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x →
    ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
      (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x
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.Exact ↔ ∀ (i : ι), (S.map (eval C c i)).Exact

Tactic:
constructor

Goal state after:
case mp
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.Exact → ∀ (i : ι), (S.map (eval C c i)).Exact

case mpr
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ (∀ (i : ι), (S.map (eval C c i)).Exact) → S.Exact
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:
constructor

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

case mpr
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ (∀ (i : ι), (S.map (eval C c i)).ShortExact) → S.ShortExact
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: case neg
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 : ι
h : ¬j = i
⊢ PreservesColimitsOfShape J (single C c i ⋙ eval C c j)

Tactic:
· exact Functor.preservesColimitsOfShape_of_isZero _ (isZero_single_comp_eval C c _ _ h) _

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

Goal state after:
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
i✝ : ι
⊢ ((x✝² * x✝¹) • x✝).f i✝ = (x✝² • x✝¹ • x✝).f i✝
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:
ext

Goal state after:
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
i✝ : ι
⊢ ((x✝² + x✝¹) • x✝).f i✝ = (x✝² • x✝ + x✝¹ • x✝).f i✝
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case e_a
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ (⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x ↦
      single ((algebraMap R A) x) 1) =
    fun x ↦ single ((algebraMap R B) x) 1

Tactic:
ext

Goal state after:
case e_a
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x✝ : R
a✝ : B
⊢ ((⇑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)) ∘ fun x ↦
          single ((algebraMap R A) x) 1)
        x✝)
      a✝ =
    (single ((algebraMap R B) x✝) 1) a✝
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K : ChainComplex C ℕ
X : C
φ : K.X 0 ⟶ X
inst✝ : HomologicalComplex.HasHomology K 0
hφ : K.d 1 0 ≫ φ = 0
⊢ IsIso (HomologicalComplex.descOpcycles K φ 1 isIso_descOpcycles_iff._proof_1 hφ) ↔
    { X₁ := K.X 1, X₂ := K.X 0, X₃ := X, f := K.d 1 0, g := φ, zero := hφ }.Exact ∧ Epi φ

Tactic:
suffices ∀ (i : ℕ) (hx : (ComplexShape.down ℕ).prev 0 = i)
    (hφ : K.d i 0 ≫ φ = 0), IsIso (K.descOpcycles φ i hx hφ) ↔
      (ShortComplex.mk _ _ hφ).Exact ∧ Epi φ from this 1 (by simp) hφ
  rintro _ rfl hφ
  let α : K.sc 0 ⟶ ShortComplex.mk (0 : X ⟶ X) (0 : X ⟶ X) (by simp) :=
    { τ₁ := 0
      τ₂ := φ
      τ₃ := 0 }
  exact (ShortComplex.quasiIso_iff_isIso_descOpcycles α (by simp) rfl rfl).symm.trans
    (ShortComplex.quasiIso_iff_of_zeros' α (by simp) rfl rfl)

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ (biprod.inr ≫ biprod.snd).f i = 𝟙 (L.X i)

Tactic:
biprod.inr_snd,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ (𝟙 L).f i = 𝟙 (L.X i)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case e'_2.e'_12
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
⊢ mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B ⇑(algebraMap B B) = LinearMap.id

Tactic:
ext

Goal state after:
case e'_2.e'_12
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
a✝¹ a✝ : B
⊢ (((mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B ⇑(algebraMap B B)) ∘ₗ lsingle a✝¹) 1) a✝ =
    ((LinearMap.id ∘ₗ lsingle a✝¹) 1) a✝
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.isoClosure.IsInvertedBy F → W.IsInvertedBy F

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.IsInvertedBy F → W.isoClosure.IsInvertedBy F
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy (F ⋙ G) ↔ W.IsInvertedBy F

Tactic:
constructor

Goal state after:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy (F ⋙ G) → W.IsInvertedBy F

case mpr
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
inst✝ : G.ReflectsIsomorphisms
⊢ W.IsInvertedBy F → W.IsInvertedBy (F ⋙ G)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : B ⊗[A] Ω[A⁄R]
⊢ x ∈ (kerCotangentToTensor R A B).range ↔ x ∈ Submodule.restrictScalars A (mapBaseChange R A B).ker

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : B ⊗[A] Ω[A⁄R]
⊢ x ∈ (kerCotangentToTensor R A B).range → x ∈ Submodule.restrictScalars A (mapBaseChange R A B).ker

case mpr
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
x : B ⊗[A] Ω[A⁄R]
⊢ x ∈ Submodule.restrictScalars A (mapBaseChange R A B).ker → x ∈ (kerCotangentToTensor R A B).range