mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ TwoSquare.GuitartExact (Φ.functor ⋙ W₂.Q).rightUnitor.symm.hom

Tactic:
TwoSquare.guitartExact_iff_isConnected_downwards

Goal state after:
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
⊢ ∀ {X₂ : C₂} {X₃ : W₂.Localization} (g : W₂.Q.obj X₂ ⟶ (𝟭 W₂.Localization).obj X₃),
    IsConnected (TwoSquare.CostructuredArrowDownwards (Φ.functor ⋙ W₂.Q).rightUnitor.symm.hom g)
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app (CostructuredArrow.mk φ) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
⊢ ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app
        (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ))

Tactic:
have : IsIso (F.map w) := by
        have := Localization.inverts L W w hw
        rw [← NatIso.naturality_2 e w]
        dsimp
        infer_instance
      have eq := s.ι.naturality
        (CostructuredArrow.homMk w : CostructuredArrow.mk φ ⟶ CostructuredArrow.mk
          ((Localization.isoOfHom L W w hw).inv ≫ φ))
      dsimp at eq hφ ⊢
      rw [comp_id] at eq
      rw [assoc] at hφ
      rw [map_comp, assoc, assoc, ← cancel_epi (F.map w), eq, ← hφ,
        NatTrans.naturality_assoc, comp_map, ← G.map_comp_assoc]
      simp

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Abelian C₁
inst✝⁶ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Abelian C₂
inst✝³ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
X : C₁
⊢ F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X) ≫
      (F.mapDerivedCategorySingleFunctor 0).hom.app X =
    DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).hom.app X)

Tactic:
by
  simp [Functor.mapDerivedCategorySingleFunctor, Functor.mapCochainComplexSingleFunctor,
    CochainComplex.singleFunctor, CochainComplex.singleFunctors,
    DerivedCategory.singleFunctorIsoCompQ]

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Abelian C₁
inst✝⁶ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Abelian C₂
inst✝³ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
X : C₁
⊢ (F.mapDerivedCategorySingleFunctor 0).inv.app X ≫
      F.mapDerivedCategoryFactors.hom.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X) =
    DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app X)

Tactic:
by
  simp [Functor.mapDerivedCategorySingleFunctor, Functor.mapCochainComplexSingleFunctor,
    CochainComplex.singleFunctor, CochainComplex.singleFunctors,
    DerivedCategory.singleFunctorIsoCompQ]

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₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
⊢ (double f hi₀₁).X k = (double f hi₀₁).X i₁

Tactic:
rw [hk₁]

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₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
⊢ K.X i₁ = K.X k

Tactic:
rw [hk₁]

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

Goal state before:
pp: case pos
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₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
h₁ : k₀ = i₁
⊢ (if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
subst h₁

Goal state after:
case pos
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₀ : ι
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
hi₀₁ : c.Rel i₀ k₀
h : i₀ ≠ k₀
φ₁ : X₁ ⟶ K.X k₀
comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0
⊢ (if hk₁ : k₀ = k₀ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case pos.ofNat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
p : ℤ
n : ℕ
hmp : Int.ofNat (n + 1) + 1 = p
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
⊢ h.d (Int.ofNat n) (Int.ofNat (n + 1)) ≫ h.d (Int.ofNat (n + 1)) p = 0

Tactic:
obtain rfl : p = .ofNat (n + 2) := by simp [← hmp]; lia

Goal state after:
case pos.ofNat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n : ℕ
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
hmp : Int.ofNat (n + 1) + 1 = Int.ofNat (n + 2)
⊢ h.d (Int.ofNat n) (Int.ofNat (n + 1)) ≫ h.d (Int.ofNat (n + 1)) (Int.ofNat (n + 2)) = 0
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
⊢ shiftFunctor C 0 ≅ 𝟭 (DifferentialObject S C)

Tactic:
refine NatIso.ofComponents (fun X => mkIso ((shiftFunctorZero C S).app X.obj) ?_) (fun f => ?_)

Goal state after:
case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ ((shiftFunctor C 0).obj X).d ≫ (CategoryTheory.shiftFunctor C 1).map ((shiftFunctorZero C S).app X.obj).hom =
    ((shiftFunctorZero C S).app X.obj).hom ≫ ((𝟭 (DifferentialObject S C)).obj X).d

case refine_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C 0).map f ≫ (mkIso ((shiftFunctorZero C S).app Y✝.obj) ⋯).hom =
    (mkIso ((shiftFunctorZero C S).app X✝.obj) ⋯).hom ≫ (𝟭 (DifferentialObject S C)).map f
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ φ.app P = F.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ G.map P.decompId_p

Tactic:
by
  rw [← φ.naturality, ← assoc, ← F.map_comp]
  conv_lhs => rw [← id_comp (φ.app P), ← F.map_id]
  congr
  apply decompId

Goal state after:
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
inst✝ : IsIdempotentComplete D
⊢ (functorExtension₂ C D).IsEquivalence

Tactic:
by
  rw [← karoubiUniversal₂_functor_eq]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case succ.hL
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt ((ChainComplex.single₀ C).obj Z) (n✝ + 1)

Tactic:
apply ChainComplex.exactAt_succ_single_obj

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F =
    (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
      HomologicalComplex.homologyMap
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map
            (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y)))
          0 ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (projectiveResolution Y).complex).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F

Tactic:
erw [← NatTrans.naturality_assoc]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map
          (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y))) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (projectiveResolution Y).complex) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (projectiveResolution Y).complex).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
⊢ leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default
  simp only [(γ.smul a).leftHomologyMap'_eq, LeftHomologyMapData.smul_φH, γ.leftHomologyMap'_eq]

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

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex C c
⊢ (forget C c).map (α_ K₁ K₂ K₃).hom =
    (((Iso.refl ((forget C c).obj (K₁ ⊗ K₂) ⊗ (forget C c).obj K₃)).symm ≪≫
          ((Iso.refl ((forget C c).obj K₁ ⊗ (forget C c).obj K₂)).symm ⊗ᵢ Iso.refl ((forget C c).obj K₃))) ≪≫
        α_ ((forget C c).obj K₁) ((forget C c).obj K₂) ((forget C c).obj K₃) ≪≫
          (Iso.refl ((forget C c).obj K₁) ⊗ᵢ Iso.refl ((forget C c).obj K₂ ⊗ (forget C c).obj K₃)) ≪≫
            Iso.refl ((forget C c).obj K₁ ⊗ (forget C c).obj (K₂ ⊗ K₃))).hom

Tactic:
by
    dsimp [forget]
    simp only [tensorHom_id, whiskerRight_tensor, id_whiskerRight,
      id_comp, Iso.inv_hom_id, comp_id, assoc]
    erw [id_whiskerRight]
    rw [id_comp]
    erw [id_comp]
    rfl

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

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.g =
    0
⊢ ∃ A' π,
    ∃ (_ : Epi π),
      ∃ x₁,
        π ≫ z =
          x₁ ≫
            { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
                f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
                zero := ⋯ }.f

Tactic:
refine ⟨A, 𝟙 _, inferInstance,
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ?_, ?_⟩ <;> dsimp

Goal state after:
case refine_1
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.g =
    0
⊢ (z ≫ X.iCycles f₂ f₃ n₀) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁ = 0

case refine_2
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.g =
    0
⊢ 𝟙 A ≫ z =
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ⋯ ≫
      X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
      f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.Exact

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements]
  intro A z hz
  refine ⟨A, 𝟙 _, inferInstance,
    X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ?_, ?_⟩ <;> dsimp
  · rw [assoc, ← X.Ψ_fromOpcycles f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ hn₁, reassoc_of% hz, zero_comp]
  · rw [← cancel_mono (X.iCycles f₂ f₃ n₀), id_comp, assoc,
      X.cyclesMap_i _ _ _ _ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) (𝟙 _) n₀ (by cat_disch),
      Functor.map_id, comp_id, liftCycles_i]

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

Goal state before:
pp: case h₁
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)).τ₁

Tactic:
dsimp; convert! (X.H _).map_id _; cat_disch

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

Goal state before:
pp: case h₂
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)).τ₂

Tactic:
dsimp; convert! (X.H _).map_id _; cat_disch

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

Goal state before:
pp: case h₃
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₃ =
    (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)).τ₃

Tactic:
dsimp; convert! (X.H _).map_id _; cat_disch

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₃
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv ≫
      ShortComplex.cyclesMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) =
    X.cyclesMap f₁ f₂ f₁' f₂' (homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯) n₁ ≫
      (X.cyclesIso f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂).inv

Tactic:
simp [← cancel_mono (ShortComplex.iCycles _), cyclesMap_i]

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 j : ι
f : i ⟶ j
i' j' : ι
f' : i' ⟶ j'
β : mk₃ (𝟙 i) f (𝟙 j) ⟶ mk₃ (𝟙 i') f' (𝟙 j')
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hβ :
  β =
    homMk₃ ((homMk₁ (β.app 1) (β.app 2) ⋯).app 0) ((homMk₁ (β.app 1) (β.app 2) ⋯).app 0)
      ((homMk₁ (β.app 1) (β.app 2) ⋯).app 1) ((homMk₁ (β.app 1) (β.app 2) ⋯).app 1) ⋯ ⋯ ⋯
⊢ X.map (𝟙 i) f (𝟙 j) (𝟙 i') f' (𝟙 j') β n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f' n₀ n₁ n₂ hn₁ hn₂).hom =
    (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.H n₁).map (homMk₁ (β.app 1) (β.app 2) ⋯)

Tactic:
exact (ShortComplex.LeftHomologyMapData.ofZeros
    (X.shortComplexMap _ _ _ _ _ _ β n₀ n₁ n₂ hn₁ hn₂) ..).homologyMap_comm

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
t : R
x y : A
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
by
    rw [LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket,
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_sub]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : x ∈ N ∧ I x ≠ ⊥
⊢ False

Tactic:
rw [← Ideal.span_singleton_le_iff_mem] at hx

Goal state after:
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
⊢ False
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mpr
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'
⊢ (∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z) → ∀ (x m : L') (x_1 : L), f x_1 = m → ∃ y, f y = ⁅x, m⁆

Tactic:
intro h x y z hz

Goal state after:
case mpr
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'
h : ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z
x y : L'
z : L
hz : f z = y
⊢ ∃ y_1, f y_1 = ⁅x, y⁆
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'
x : L
⊢ f x ∈ LieIdeal.map f ⊤

Tactic:
exact LieIdeal.mem_map (LieSubmodule.mem_top x)

Goal state after: