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

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
⊢ c₁.π c₂ c (i₁, c₂.next i₂) = j'

Tactic:
rw [← h₃, ComplexShape.π_symm c₁ c₂ c]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D
inst✝⁶ : Preadditive C₁
inst✝⁵ : HasZeroMorphisms C₂
inst✝⁴ : Preadditive D
K₁ L₁ : CochainComplex C₁ ℤ
f₁ : K₁ ⟶ L₁
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝³ : F.Additive
inst✝² : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
x : ℤ
inst✝¹ : K₁.HasMapBifunctor K₂ F
inst✝ : L₁.HasMapBifunctor K₂ F
⊢ mapBifunctorMap ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).map f₁) (𝟙 K₂) F
        (ComplexShape.up ℤ) ≫
      (L₁.mapBifunctorShift₁Iso K₂ F x).hom =
    (K₁.mapBifunctorShift₁Iso K₂ F x).hom ≫
      (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).map (mapBifunctorMap f₁ (𝟙 K₂) F (ComplexShape.up ℤ))

Tactic:
ext n p q h
  simp [ι_mapBifunctorShift₁Iso_hom_f _ _ _ _ _ _ _ _ (p + x) (n + x) rfl rfl,
    ι_mapBifunctorShift₁Iso_hom_f_assoc _ _ _ _ _ _ _ _ (p + x) (n + x) rfl rfl]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : toHom (mk x) = 0
⊢ ∃ m, m + 1 = n ∧ ∃ β, δ m n β = ↑x

Tactic:
toHom_mk,

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (Cocycle.equivHomShift.symm x) = 0
⊢ ∃ m, m + 1 = n ∧ ∃ β, δ m n β = ↑x
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²² : Category.{v_1, u_1} C₁
inst✝²¹ : Category.{v_2, u_2} C₂
inst✝²⁰ : Category.{v_3, u_5} C₃
inst✝¹⁹ : Category.{v_4, u_6} C₄
inst✝¹⁸ : Category.{v_6, u_4} C₂₃
inst✝¹⁷ : HasZeroMorphisms C₁
inst✝¹⁶ : HasZeroMorphisms C₂
inst✝¹⁵ : HasZeroMorphisms C₃
inst✝¹⁴ : Preadditive C₂₃
inst✝¹³ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹² : G₂₃.PreservesZeroMorphisms
inst✝¹¹ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁰ : F.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁸ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁷ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁶ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁵ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁴ : TotalComplexShape c₁ c₂₃ c₄
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₃.Rel i₃ (c₃.next i₃)
⊢ (c₁.ε₂ c₂₃ c₄ (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)) •
      (F.obj (K₁.X i₁)).map ((G₂₃.obj (K₂.X i₂)).map (K₃.d i₃ (c₃.next i₃))) ≫
        ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ (c₃.next i₃) j =
    0

Tactic:
rw [shape _ _ _ h, Functor.map_zero, Functor.map_zero, zero_comp, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i' : ι'
⊢ (extendMap f e).f i' = (dNext i') (extend.hom e h.hom) + (prevD i') (extend.hom e h.hom) + (extendMap g e).f i'

Tactic:
by
    by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, rfl⟩ := hi'
      rw [extendMap_f _ _ rfl, extendMap_f _ _ rfl, h.comm i, Preadditive.add_comp,
        Preadditive.add_comp, Preadditive.comp_add, Preadditive.comp_add, add_left_inj]
      congr 1
      · by_cases hi : c.Rel i (c.next i)
        · have hi' : c'.Rel (e.f i) (e.f (c.next i)) := by rwa [e.rel_iff]
          simp [dNext_eq _ hi, dNext_eq _ hi', extend.hom_eq _ _ rfl rfl,
            extend_d_eq _ _ rfl rfl]
        · rw [dNext_eq_zero _ _ hi]
          by_cases hi' : c'.Rel (e.f i) (c'.next (e.f i))
          · simp [dNext_eq _ hi', K.extend_d_from_eq_zero _ _ _ _ rfl hi]
          · simp [dNext_eq_zero _ _ hi']
      · by_cases hi : c.Rel (c.prev i) i
        · have hi' : c'.Rel (e.f (c.prev i)) (e.f i) := by rwa [e.rel_iff]
          simp [prevD_eq _ hi, prevD_eq _ hi', extend.hom_eq _ _ rfl rfl,
            extend_d_eq _ _ rfl rfl]
        · rw [prevD_eq_zero _ _ hi]
          by_cases hi' : c'.Rel (c'.prev (e.f i)) (e.f i)
          · simp [prevD_eq _ hi', L.extend_d_to_eq_zero _ _ _ _ rfl hi]
          · simp [prevD_eq_zero _ _ hi']
    · exact (isZero_extend_X _ _ _ (by tauto)).eq_of_src _ _

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
⊢ ((singleFunctor C n).obj X).IsLE n

Tactic:
let e := (singleFunctorIsoCompQ C n).app X
  dsimp only [Functor.comp_obj] at e
  exact TStructure.t.isLE_of_iso e.symm n

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
inst✝¹ : (cofibrations C).IsStableUnderComposition
X Y : C
i : X ⟶ Y
inst✝ : Cofibration i
hX : Cofibration (initial.to X)
⊢ Cofibration (initial.to Y)

Tactic:
rw [Subsingleton.elim (initial.to Y) (initial.to X ≫ i)]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
inst✝¹ : (cofibrations C).IsStableUnderComposition
X Y : C
i : X ⟶ Y
inst✝ : Cofibration i
hX : Cofibration (initial.to X)
⊢ Cofibration (initial.to X ≫ i)
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hY : IsCofibrant Y
⊢ Cofibration coprod.inl

Tactic:
rw [isCofibrant_iff] at hY

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hY : Cofibration (initial.to Y)
⊢ Cofibration coprod.inl
Module: Mathlib.AlgebraicTopology.ModelCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : HasFiniteLimits C
inst✝³ : HasFiniteColimits C
inst✝² : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : (trivialCofibrations C).MapFactorizationData (fibrations C) f
this✝¹ : Cofibration hf.i
this✝ : WeakEquivalence hf.i
φ : pushout hf.i (Arrow.Hom.left h.i) ⟶ Y := pushout.desc (hf.p ≫ Arrow.Hom.right h.i) w ⋯
this : Fibration hf.p
⊢ WeakEquivalence (pushout.inr hf.i (Arrow.Hom.left h.i) ≫ φ)

Tactic:
simpa [φ]

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp ((δ 0 1 α).comp (Cochain.ofHom ι) ⋯) ⋯ = ↑(cocycle₁' sq hsq)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
⊢ l.homOf ≫ p = b

Tactic:
by
        ext n
        have : ι.f n ≫ p.f n = 0 := by
          simp [← HomologicalComplex.comp_f, hι]
        simpa [l, this] using (hsq n).fac_right

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip✝ : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
hip : QuasiIso i ∨ QuasiIso p
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝¹ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this✝ : ∀ (n : ℤ), Injective ((kernel p).X n)
this : (kernel p).IsKInjective
α : Cochain (cokernel i) (kernel p) 0
hα : δ 0 1 α = ↑β
⊢ sq.HasLift

Tactic:
exact Lifting.hasLift sq _ (cokernelIsCokernel _) (kernelIsKernel _) α hα

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
⊢ QuasiIsoAt (ι f n) n

Tactic:
have := mono_homologyMap_π f n n (by lia)

Goal state after:
case inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
this : Mono (homologyMap (π f n) n)
⊢ QuasiIsoAt (ι f n) n
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₃ X₃' : C₃
e : X₃ ≅ X₃'
⊢ (w.costructuredArrowRightwards X₃).Final ↔ (w.costructuredArrowRightwards X₃').Final

Tactic:
Functor.final_iff_comp_equivalence _ (CostructuredArrow.mapIso (B.mapIso e)).functor,

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₃ X₃' : C₃
e : X₃ ≅ X₃'
⊢ (w.costructuredArrowRightwards X₃ ⋙ (CostructuredArrow.mapIso (B.mapIso e)).functor).Final ↔
    (w.costructuredArrowRightwards X₃').Final
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝³ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝² : Φ.arrow.HasRightResolutions
inst✝¹ : W₂.ContainsIdentities
inst✝ : Φ.IsLocalizedEquivalence
⊢ Φ.IsRightDerivabilityStructure

Tactic:
rw [Φ.isRightDerivabilityStructure_iff (Φ.functor ⋙ W₂.Q) W₂.Q (𝟭 _)
    (Functor.rightUnitor _).symm, TwoSquare.guitartExact_iff_isConnected_downwards]
  apply Constructor.isConnected

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝² : L.IsEquivalence
inst✝¹ : R.IsEquivalence
inst✝ : IsIso w.natTrans
⊢ w.GuitartExact

Tactic:
rw [guitartExact_iff_initial]
  intro X₂
  have := StructuredArrow.isEquivalence_post X₂ T R
  have : (Comma.mapRight _ w : StructuredArrow (R.obj X₂) _ ⥤ _).IsEquivalence :=
    (Comma.mapRightIso _ (asIso w)).isEquivalence_functor
  have := StructuredArrow.isEquivalence_pre (R.obj X₂) L B
  dsimp only [structuredArrowDownwards]
  infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k k' : ι
hk : k = i₀ ∧ k' = i₁ ∧ i₀ ≠ i₁
⊢ X₁ = if k' = i₀ then X₀ else if k' = i₁ then X₁ else 0

Tactic:
if_neg,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k k' : ι
hk : k = i₀ ∧ k' = i₁ ∧ i₀ ≠ i₁
⊢ X₁ = if k' = i₁ then X₁ else 0

case hnc
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k k' : ι
hk : k = i₀ ∧ k' = i₁ ∧ i₀ ≠ i₁
⊢ ¬k' = i₀
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
⊢ f.f 1 ≫
        { X₁ := Q.complex.X (0 + 2), X₂ := Q.complex.X (0 + 1), X₃ := Q.complex.X 0, f := Q.complex.d (0 + 2) (0 + 1),
            g := Q.complex.d (0 + 1) 0, zero := ⋯ }.g -
      P.complex.d 1 0 ≫
        liftHomotopyZeroZero f comm ≫
          { X₁ := Q.complex.X (0 + 2), X₂ := Q.complex.X (0 + 1), X₃ := Q.complex.X 0, f := Q.complex.d (0 + 2) (0 + 1),
              g := Q.complex.d (0 + 1) 0, zero := ⋯ }.g =
    0

Tactic:
HomologicalComplex.Hom.comm,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
⊢ P.complex.d 1 0 ≫ f.f 0 -
      P.complex.d 1 0 ≫
        liftHomotopyZeroZero f comm ≫
          { X₁ := Q.complex.X (0 + 2), X₂ := Q.complex.X (0 + 1), X₃ := Q.complex.X 0, f := Q.complex.d (0 + 2) (0 + 1),
              g := Q.complex.d (0 + 1) 0, zero := ⋯ }.g =
    0
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
⊢ ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map
      { app := fun P ↦ F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p, naturality := ⋯ } =
    τ

Tactic:
by
    ext X
    dsimp
    rw [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi,
      Functor.map_id, Category.id_comp]
    change _ ≫ G.map (𝟙 _) = _
    simp

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
⊢ Zigzag j1 j2

Tactic:
apply Relation.ReflTransGen.single

Goal state after:
case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
⊢ Zag j1 j2
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝³ : X₃.HasTensor X₄
inst✝² : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A
inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
H : X₁.HasTensor₄ObjExt X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
i₂ i₃ : I
⊢ ∀ (i₃_1 : I) (h : i₂ + i₃ + i₃_1 = i₂₃₄),
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₃_1 i₂₃₄ h ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f =
      X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₃_1 i₂₃₄ h ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g

Tactic:
i₄

Goal state after:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝³ : X₃.HasTensor X₄
inst✝² : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A
inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
H : X₁.HasTensor₄ObjExt X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
i₂ i₃ i₄ : I
⊢ ∀ (h : i₂ + i₃ + i₄ = i₂₃₄),
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f =
      X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ X.δ f g (n - 1) n ⋯ ≫ (X.H n).map (homMk₁ (α.app 0) (α.app 1) ⋯) ≫ X.pOpcycles f' g' n = 0

Tactic:
← X.δ_naturality_assoc f g f' g'
        (homMk₁ (α.app 0) (α.app 1) (naturality' α 0 1))
        (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2)) _ _,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ (X.H (n - 1)).map (homMk₁ (α.app 1) (α.app 2) ⋯) ≫
      X.δ f' g' (n - 1) n (CategoryTheory.Abelian.SpectralObject.opcycles._proof_1 n) ≫ X.pOpcycles f' g' n =
    0
Module: Mathlib.Algebra.Homology.SpectralObject.Homology

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂'✝ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' : x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃₄ (threeδ₃Toδ₂ f₂ f₃ f₄ f₃₄ ⋯) n₂ = 0
⊢ (x₂ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) ≫ ((X.sequenceΨ f₂ f₃ f₄ (f₂ ≫ f₃) ⋯ f₃₄ h₃₄ n₁ n₂ ⋯).sc ⋯ 1 ⋯).g = 0

Tactic:
simp [sequenceΨ, Precomp.map, hx₂']

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
⊢ coreE₂CohomologicalNat.i₀ r (p, q) ⋯ ≤ WithBotTop.coe 0

Tactic:
simp only [coreE₂CohomologicalNat_i₀, WithBotTop.coe_le_coe]

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : X.HasSpectralSequence data
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
p q : ℕ
hpq : ∀ (pq' : ℕ × ℕ), ¬(ComplexShape.spectralSequenceNat (r, 1 - r)).Rel (p, q) pq'
hr : autoParam (2 ≤ r) HasSpectralSequence._auto_3
⊢ ↑q - r + 2 ≤ 0
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.cyclesIsoH f n₀ n₁ hn₁).hom ≫ X.toCycles (𝟙 i₀) f f ⋯ n₀ = 𝟙 (X.cycles (𝟙 i₀) f n₀)

Tactic:
by
  simpa using (X.cyclesIsoH f n₀ n₁ hn₁).hom_inv_id

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁ ≫
      X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ =
    0

Tactic:
by
  rw [← cancel_epi (X.pOpcycles ..), comp_zero,
    p_opcyclesMap_assoc _ _ _ _ _ _ (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)]
  simp

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝⁴ : Ring A
R : Type u
inst✝³ : CommRing R
inst✝² : Algebra R A
B : Type w
inst✝¹ : Ring B
inst✝ : Algebra R B
f g : A →ₐ[R] B
h : f.toLieHom = g.toLieHom
⊢ f = g

Tactic:
ext a; exact LieHom.congr_fun h a

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case smul
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s✝ s : Set L
x : L
t : R
x✝ : L
hx✝ : x✝ ∈ lieSpan R L (-s)
hu : x✝ ∈ lieSpan R L s
⊢ t • x✝ ∈ lieSpan R L s

Tactic:
| smul t _ _ hu =>

Goal state after:
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ map f I = ⊥ ↔ I ≤ f.ker

Tactic:
rw [← le_bot_iff]
  exact LieIdeal.map_le_iff_le_comap

Goal state after:
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
S : Set (LieSubmodule R L M)
⊢ ↑(sSup S) = ⨆ N ∈ S, ↑N

Tactic:
rw [sSup_toSubmodule, ← Set.image, sSup_image]

Goal state after: