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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ (fun i ↦ i) = ⇑e.symm ∘ ⇑e

Tactic:
ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β γ : Type w
e : β ≃ γ
⊢ ⇑e ∘ ⇑e.symm = fun i ↦ i

Tactic:
ext; 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
ι : 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:
by
    ext
    dsimp
    split_ifs with h
    · subst h
      simp
    · simp

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.restrictScalars S (ideal R S) ≤ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
rintro x (hx : _ = _)

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
⊢ x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
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
⊢ (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ + a₂ } { as := a₃ }).app X ≫
      ((shiftMonoidalFunctor C A).obj { as := a₃ }).map
        ((OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ } { as := a₂ }).app 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:
simp only [obj_μ_inv_app, Discrete.addMonoidal_associator, eqToIso.hom, eqToHom_map,
    eqToHom_app]

Goal state after:
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
⊢ (OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a₁ + a₂ } { as := a₃ }).app X ≫
      (LaxMonoidal.μ (shiftMonoidalFunctor C A) (MonoidalCategoryStruct.tensorObj { as := a₁ } { as := a₂ })
              { as := a₃ }).app
          X ≫
        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)
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
⊢ n + m + n = n

Tactic:
by rw [h, zero_add]

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

Tactic:
erw [← shiftComm_symm Y i j, ← ((shiftFunctorComm C i j).hom.naturality_assoc f)]

Goal state after:
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
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftFunctor C i ⋙ shiftFunctor C j).map f ≫ (shiftFunctorComm C i j).hom.app Y ≫ (shiftComm Y i j).symm.hom
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: 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

Tactic:
intro hS i

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)
hS : S.Exact
i : ι
⊢ (S.map (eval C c i)).Exact
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: 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

Tactic:
intro hS i

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)
hS : S.ShortExact
i : ι
⊢ (S.map (eval C c i)).ShortExact
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: 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

Tactic:
intro e

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)
e :
  ((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
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: 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

Tactic:
intro e

Goal state after:
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)
e : ((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.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:
intro x
      obtain ⟨x, rfl⟩ := KaehlerDifferential.linearCombination_surjective R S x
      have := LinearMap.congr_fun
        (KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination R S) x
      rw [LinearMap.comp_apply] at this
      rw [this]
      rfl

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
  dsimp only [iCycles]
  infer_instance

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

Goal state before:
pp: case a.tmul
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
r : B
x : A →₀ A
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) x)) = 0

Tactic:
induction x using Finsupp.induction_linear

Goal state after:
case a.tmul.zero
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
r : B
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) 0)) = 0

case a.tmul.add
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
r : B
f✝ g✝ : A →₀ A
a✝¹ : r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) f✝)) = 0
a✝ : r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) g✝)) = 0
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) (f✝ + g✝))) = 0

case a.tmul.single
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
r : B
a✝ b✝ : A
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) (single a✝ b✝))) = 0
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; 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
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
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
x y : ↥(RingHom.ker (algebraMap A B))
⊢ 1 ⊗ₜ[A] (D R A) ↑(x + y) = 1 ⊗ₜ[A] (D R A) ↑x + 1 ⊗ₜ[A] (D R A) ↑y

Tactic:
by simp only [Submodule.coe_add, map_add, TensorProduct.tmul_add]

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 : 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
⊢ RingHom.ker (algebraMap A B) • ⊤ ≤ (kerToTensor R A B).ker

Tactic:
by
    rw [Submodule.smul_eq_map₂]
    apply iSup_le_iff.mpr
    simp only [Submodule.map_le_iff_le_comap, Subtype.forall]
    rintro x hx y -
    simp only [Submodule.mem_comap, LinearMap.lsmul_apply, LinearMap.mem_ker, map_smul,
      kerToTensor_apply, TensorProduct.smul_tmul', ← algebraMap_eq_smul_one,
      RingHom.mem_ker.mp hx, TensorProduct.zero_tmul]

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

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : ChainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ C.d (n✝ + 1) ((ComplexShape.down ℕ).next (n✝ + 1)) ≫ f ((ComplexShape.down ℕ).next (n✝ + 1)) (n✝ + 1) =
    C.d (n✝ + 1) (n✝ + 1 - 1) ≫ f (n✝ + 1 - 1) (n✝ + 1)

Tactic:
· congr <;> simp

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

Goal state before:
pp: 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 : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
⊢ ∃ y, (kerCotangentToTensor R A B) y = 1 ⊗ₜ[A] ∑ x_1 ∈ x.support with (algebraMap A B) x_1 = c, x x_1 • (D R A) x_1

Tactic:
use ∑ i ∈ {i ∈ x.support | algebraMap A B i = c}.attach, x i • Ideal.toCotangent _ ⟨i - a, ?_⟩

Goal state after:
case h
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 : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
⊢ (kerCotangentToTensor R A B)
      (∑ i ∈ {i ∈ x.support | (algebraMap A B) i = c}.attach,
        x ↑i • (RingHom.ker (algebraMap A B)).toCotangent ⟨↑i - a, ⋯⟩) =
    1 ⊗ₜ[A] ∑ x_1 ∈ x.support with (algebraMap A B) x_1 = c, x x_1 • (D R A) x_1

case w
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 : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
i : ↥({i ∈ x.support | (algebraMap A B) i = c})
⊢ ↑i - a ∈ RingHom.ker (algebraMap A B)
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n✝ : ℕ
⊢ f (n✝ + 1) ((ComplexShape.up ℕ).prev (n✝ + 1)) ≫ D.d ((ComplexShape.up ℕ).prev (n✝ + 1)) (n✝ + 1) =
    f (n✝ + 1) (n✝ + 1 - 1) ≫ D.d (n✝ + 1 - 1) (n✝ + 1)

Tactic:
· congr <;> simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Linear R V
h : Homotopy f g
a : R
i j : ι
hij : ¬c.Rel j i
⊢ a • h.hom i j = 0

Tactic:
rw [h.zero i j hij, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₂ : Cochain F G n
⊢ (ofHom (𝟙 F)).comp z₂ ⋯ = z₂

Tactic:
by
  ext p q hpq
  simp only [zero_cochain_comp_v, ofHom_v, HomologicalComplex.id_f, id_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
e f : ℤ
hf : -1 + e = f
γ : Cochain G K e
he : 0 + e = e
⊢ (inl φ).comp ((snd φ).comp γ he) hf = 0

Tactic:
rw [← Cochain.comp_assoc_of_second_is_zero_cochain, inl_snd, Cochain.zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
p : ℤ
eq : φ₁.f p = (dNext p) h.hom + (prevD p) h.hom + φ₂.f p
⊢ (δ (-1) 0 (Cochain.ofHomotopy h)).v p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯

Tactic:
rw [dNext_eq h.hom (show (ComplexShape.up ℤ).Rel p (p + 1) by simp),
    prevD_eq h.hom (show (ComplexShape.up ℤ).Rel (p - 1) p by simp)] at eq

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
p : ℤ
eq : φ₁.f p = F.d p (p + 1) ≫ h.hom (p + 1) p + h.hom p (p - 1) ≫ G.d (p - 1) p + φ₂.f p
⊢ (δ (-1) 0 (Cochain.ofHomotopy h)).v p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case neg
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫ (mapHomologicalComplexObjXIso φ H i).inv ≫ H.map (d φ i j) =
    inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫
      d ((H.mapHomologicalComplex c).map φ) i j ≫ (mapHomologicalComplexObjXIso φ H j).inv

Tactic:
simp [← Functor.map_comp, inlX_d' _ _ _ _ hj, inlX_d'_assoc _ _ _ _ hj]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ (lift r F hF).map ((Functor.commShiftIso (functor r) (a + b)).inv.app X) ≫
      (Functor.commShiftIso F (a + b)).hom.app X =
    (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)).hom.app ((functor r).obj X)

Tactic:
(functor r).commShiftIso_add,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ (lift r F hF).map
        ((Functor.CommShift.isoAdd (Functor.commShiftIso (functor r) a) (Functor.commShiftIso (functor r) b)).inv.app
          X) ≫
      (Functor.commShiftIso F (a + b)).hom.app X =
    (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)).hom.app ((functor r).obj X)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
h : n = 0
X✝ Y✝ : CochainComplex C ℤ
x✝ : X✝ ⟶ Y✝
⊢ (shiftFunctor C n).map x✝ ≫ (Hom.isoOfComponents (fun i ↦ Y✝.shiftFunctorObjXIso n i i ⋯) ⋯).hom =
    (Hom.isoOfComponents (fun i ↦ X✝.shiftFunctorObjXIso n i i ⋯) ⋯).hom ≫ (𝟭 (CochainComplex C ℤ)).map x✝

Tactic:
ext; simp

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
⊢ LiftCommShift.iso F r hF (a + b) = Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)

Tactic:
by
    ext1
    apply natTrans_ext
    ext X
    dsimp
    rw [LiftCommShift.iso_hom_app, (functor r).commShiftIso_add, F.commShiftIso_add,
      Functor.CommShift.isoAdd_hom_app, Functor.CommShift.isoAdd_hom_app,
      Functor.CommShift.isoAdd_inv_app, Functor.map_comp, Functor.map_comp,
      Functor.map_comp, assoc, assoc, assoc, LiftCommShift.iso_hom_app, lift_map_functor_map]
    congr 1
    rw [← cancel_epi ((shiftFunctor (Quotient r) b ⋙ lift r F hF).map
      (NatTrans.app (Functor.commShiftIso (functor r) a).hom X))]
    simp only [← Functor.comp_map, ← Functor.comp_obj]
    rw [(LiftCommShift.iso F r hF b).hom.naturality_assoc (((functor r).commShiftIso a).hom.app X)]
    simp only [Functor.comp_obj, LiftCommShift.iso_hom_app, Iso.hom_inv_id_app,
      Functor.comp_map, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app,
      Functor.map_id, id_comp, lift_obj_functor_obj]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ IsIso f

Tactic:
let e := Triangle.isoMk A B (asIso f.hom₁) (asIso f.hom₂) (asIso f.hom₃)
    (by simp) (by simp) (by simp)
  exact (inferInstance : IsIso e.hom)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ IsIso f

Tactic:
by
  let e := Triangle.isoMk A B (asIso f.hom₁) (asIso f.hom₂) (asIso f.hom₃)
    (by simp) (by simp) (by simp)
  exact (inferInstance : IsIso e.hom)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 A.obj₂

Tactic:
← comp_hom₂,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ (e.hom ≫ e.inv).hom₂ = 𝟙 A.obj₂
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 B.obj₂

Tactic:
← comp_hom₂,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ (e.inv ≫ e.hom).hom₂ = 𝟙 B.obj₂
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case e_a.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ (a * m + a * n').negOnePow = (a * m).negOnePow * (a * n').negOnePow

Tactic:
Int.negOnePow_add

Goal state after:
case e_a.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ (a * m).negOnePow * (a * n').negOnePow = (a * m).negOnePow * (a * n').negOnePow