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

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful

Tactic:
by
  let := Localization.preadditive L₁ (B.inverseImage A.ι).trW
  let := Localization.preadditive L₂ B.trW
  have := Localization.functor_additive L₁ (B.inverseImage A.ι).trW
  have := Localization.functor_additive L₂ B.trW
  let F := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
  let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F :=
    CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
  refine Functor.faithful_of_comp_cancel_zero_of_hasLeftCalculusOfFractions L₁
    (B.inverseImage A.ι).trW F (fun X₁ X₂ f hf ↦ ?_)
  replace hf : L₂.map f.hom = L₂.map 0 := by
    simp [← dsimp% NatIso.naturality_2 e f, hf]
  rw [MorphismProperty.map_eq_iff_postcomp L₂ B.trW] at hf
  obtain ⟨X₃, s, hs, fac⟩ := hf
  obtain ⟨X₄, t, a, hX₄, ht, fac'⟩ :=
    IsVerdierRightLocalizing.fac' s X₂.property hs
  let t' : X₂ ⟶ ⟨X₄, hX₄⟩ := A.homMk t
  have := Localization.inverts L₁ (B.inverseImage A.ι).trW t'
    (by rwa [trW_inverseImage_ι_iff])
  rw [← cancel_mono (L₁.map t'), zero_comp, ← L₁.map_comp, ← L₁.map_zero]
  congr 1
  ext
  simp [t', ← fac', reassoc_of% fac]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
⊢ ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), epiWithInjectiveKernel g → epiWithInjectiveKernel f

Tactic:
by
    rintro X' Y' X Y f' f r ⟨_, hf⟩
    have : Epi f' :=
      (MorphismProperty.epimorphisms C).of_retract r (.infer_property _)
    let r' : Retract (kernel f') (kernel f) :=
      { i := kernel.map _ _ r.i.left r.i.right (Arrow.w r.i).symm
        r := kernel.map _ _ r.r.left r.r.right (Arrow.w r.r).symm
        retract := by ext; simp }
    exact ⟨inferInstance, r'.injective⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj T.obj₁)
mem : Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k ∈ distinguishedTriangles
H : Octahedron ⋯ ⋯ hT mem := someOctahedron ⋯ ⋯ hT mem
⊢ t.IsGE Z n

Tactic:
exact t.isGE₂ _ H.mem n (by dsimp; infer_instance) (by dsimp; infer_instance)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsCofibrant X
h✝ : LeftHomotopyRel f g
Q : PathObject Y
inst✝ : Q.IsGood
P : Cylinder X := ⋯.choose
h : ⋯.choose.LeftHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₀ = f

Tactic:
have := sq.fac_right =≫ prod.fst

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsCofibrant X
h✝ : LeftHomotopyRel f g
Q : PathObject Y
inst✝ : Q.IsGood
P : Cylinder X := ⋯.choose
h : ⋯.choose.LeftHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
this : (sq.lift ≫ Q.p) ≫ prod.fst = prod.lift (P.π ≫ f) h.h ≫ prod.fst
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₀ = f
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsCofibrant X
h✝ : LeftHomotopyRel f g
Q : PathObject Y
inst✝ : Q.IsGood
P : Cylinder X := ⋯.choose
h : ⋯.choose.LeftHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
this : sq.lift ≫ Q.p ≫ prod.fst = prod.lift (P.π ≫ f) h.h ≫ prod.fst
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₀ = f

Tactic:
Q.p_fst,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsCofibrant X
h✝ : LeftHomotopyRel f g
Q : PathObject Y
inst✝ : Q.IsGood
P : Cylinder X := ⋯.choose
h : ⋯.choose.LeftHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
this : sq.lift ≫ Q.p₀ = prod.lift (P.π ≫ f) h.h ≫ prod.fst
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₀ = f
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h✝ : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject Z
left✝ : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
sq : CommSq h.h f P.p (prod.lift f₀ f₁)
⊢ sq.lift ≫ P.p₀ = f₀

Tactic:
have := sq.fac_right =≫ prod.fst

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h✝ : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject Z
left✝ : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
sq : CommSq h.h f P.p (prod.lift f₀ f₁)
this : (sq.lift ≫ P.p) ≫ prod.fst = prod.lift f₀ f₁ ≫ prod.fst
⊢ sq.lift ≫ P.p₀ = f₀
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : C
inst✝ : IsFibrant Y
f g : resolutionObj X ⟶ Y
h : RightHomotopyRel (iResolutionObj X ≫ f) (iResolutionObj X ≫ g)
⊢ toHoCat.map (homMk f) = toHoCat.map (homMk g)

Tactic:
apply toHoCat_map_eq

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : C
inst✝ : IsFibrant Y
f g : resolutionObj X ⟶ Y
h : RightHomotopyRel (iResolutionObj X ≫ f) (iResolutionObj X ≫ g)
⊢ homRel C (homMk f) (homMk g)
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
⊢ RightHomotopyRel (iResolutionObj X ≫ resolutionMap (𝟙 X)) (iResolutionObj X ≫ 𝟙 (mk (resolutionObj X)).obj)

Tactic:
simpa using .refl _

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ RightHomotopyRel (iResolutionObj X₁ ≫ resolutionMap (f ≫ g))
    (iResolutionObj X₁ ≫ (homMk (resolutionMap f)).hom ≫ (homMk (resolutionMap g)).hom)

Tactic:
simpa using .refl _

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: case mp
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
hF : F.HasPointwiseRightDerivedFunctor W₂
X₁ : C₁
⊢ (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X₁

Tactic:
hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure

Goal state after:
case mp
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
hF : F.HasPointwiseRightDerivedFunctor W₂
X₁ : C₁
⊢ F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor.obj X₁)
Module: Mathlib.CategoryTheory.GuitartExact.KanExtension

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝¹ : ∀ (F : C₁ ⥤ D), L.HasLeftKanExtension F
inst✝ : ∀ (F : C₂ ⥤ D), R.HasLeftKanExtension F
F : C₂ ⥤ D
⊢ IsIso (w.lanBaseChange.app F) ↔
    (StructuredArrow.right ((LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w)).IsLeftKanExtension
      (StructuredArrow.hom ((LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w))

Tactic:
by
  rw [lanBaseChange_app, isIso_lanAdjunction_homEquiv_symm_iff]
  simp

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

Goal state before:
pp: case refine_2.refine_1
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ (pathObject.lift f₀ f₁ (homotopyOfEq f₀ f₁ ⋯) ≫
        (pathObject.mapHomologicalComplexObjIso K₂ (InjectiveObject.ι C) ⋯).inv) ≫
      (((Plus.prepathObject { obj := K₂, property := ⋯ }).map (CochainComplex.Plus.localizerMorphism C).functor).map
          (CochainComplex.plus C).ι).p₀ =
    (ObjectProperty.homMk f₀).hom

Tactic:
dsimp [Functor.mapCochainComplexPlus]

Goal state after:
case refine_2.refine_1
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ (pathObject.lift f₀ f₁ (homotopyOfEq f₀ f₁ ⋯) ≫
        (pathObject.mapHomologicalComplexObjIso K₂ (InjectiveObject.ι C) ⋯).inv) ≫
      ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).map (pathObject.π₀ K₂) =
    f₀
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ (pathObject.lift f₀ f₁ (homotopyOfEq f₀ f₁ ⋯) ≫
        (pathObject.mapHomologicalComplexObjIso K₂ (InjectiveObject.ι C) ⋯).inv) ≫
      (((Plus.prepathObject { obj := K₂, property := ⋯ }).map (CochainComplex.Plus.localizerMorphism C).functor).map
          (CochainComplex.plus C).ι).p₁ =
    (ObjectProperty.homMk f₁).hom

Tactic:
dsimp [Functor.mapCochainComplexPlus]

Goal state after:
case refine_2.refine_2
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ (pathObject.lift f₀ f₁ (homotopyOfEq f₀ f₁ ⋯) ≫
        (pathObject.mapHomologicalComplexObjIso K₂ (InjectiveObject.ι C) ⋯).inv) ≫
      ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).map (pathObject.π₁ K₂) =
    f₁
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasExt C
inst✝ : HasExt D
S : ShortComplex C
hS : S.ShortExact
⊢ mapExactFunctor F hS.extClass = ⋯.extClass

Tactic:
by
  ext
  rw [Ext.mapExactFunctor_hom, hS.extClass_hom]
  exact (hS.mapShiftedHom_singleδ' F).trans (hS.map_of_exact F).extClass_hom.symm

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
X' : C
g : X' ⟶ X
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ (Cochain.fromSingleEquiv h) ↑(fromSingleMk (g ≫ f) h q' hq' ⋯) =
    (Cochain.fromSingleEquiv h) ↑((fromSingleMk f h q' hq' hf).precomp ((singleFunctor C p).map g))

Tactic:
by simp [Cochain.fromSingleMk_precomp]

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
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f
h₂ : F.map ((toKaroubi C).map f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map ((toKaroubi C).map f.f)
h₃ : X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f

Tactic:
rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X : GradedObject J D
j : J
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j, 0), ⋯⟩ =
    (F.obj (X j)).map (singleObjApplyIso 0 Y).hom ≫ e.hom.app (X j)

Tactic:
by
  simp [mapBifunctorRightUnitorCofan]

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₀ 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₁₂
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.toCycles f₃ f₄ f₃₄ h₃₄ n₁ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ =
    X.δ f₁₂ f₃₄ n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃

Tactic:
by
  subst h₁₂ h₃₄
  simp only [d, δ_toCycles_assoc, toCycles_πE_descE]

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₂
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).Exact

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements]
  intro A x₂ hx₂
  dsimp at x₂ hx₂
  obtain ⟨A₁, π₁, _, y₂, hy₂⟩ :=
    surjective_up_to_refinements_of_epi (X.pOpcycles f₁₂ f₃ n₁) x₂
  obtain ⟨A₂, π₂, _, y₁, hy₁⟩ :=
    (X.cokernelSequenceE_exact f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).exact_up_to_refinements y₂
      (by simpa only [Category.assoc, p_opcyclesToE, hx₂, comp_zero]
        using! hy₂.symm =≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)
  dsimp at y₁ hy₁
  obtain ⟨a, b, rfl⟩ : ∃ a b, y₁ = a ≫ biprod.inl + b ≫ biprod.inr :=
    ⟨y₁ ≫ biprod.fst, y₁ ≫ biprod.snd, by ext <;> simp⟩
  simp only [Preadditive.add_comp, Category.assoc, biprod.inl_desc, biprod.inr_desc] at hy₁
  refine ⟨A₂, π₂ ≫ π₁, inferInstance, a, ?_⟩
  simp [Category.assoc, hy₂, reassoc_of% hy₁, Preadditive.add_comp, δ_pOpcycles,
    comp_zero, add_zero]

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

Tactic:
subst hβ
    exact hom_ext₁ rfl rfl

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

Tactic:
obtain rfl : α = homMk₁ (β.app 1) (β.app 2) (naturality' β 1 2) := by
    subst hβ
    exact hom_ext₁ rfl rfl
  exact (ShortComplex.LeftHomologyMapData.ofZeros
    (X.shortComplexMap _ _ _ _ _ _ β n₀ n₁ n₂ hn₁ hn₂) ..).homologyMap_comm

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

Goal state before:
pp: L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅-x, m⁆ + ⁅x, m⁆ = 0

Tactic:
← add_lie

Goal state after:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅-x + x, m⁆ = 0
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {α β : Type u_5} (a : α ≃ β),
    (∀ {M : α → Type u_6} [inst : (i : α) → AddCommGroup (M i)] [inst_1 : (i : α) → Module R (M i)]
        [∀ (i : α), IsArtinian R (M i)], IsArtinian R ((i : α) → M i)) →
      ∀ {M : β → Type u_6} [inst : (i : β) → AddCommGroup (M i)] [inst_1 : (i : β) → Module R (M i)]
        [∀ (i : β), IsArtinian R (M i)], IsArtinian R ((i : β) → M i)

Tactic:
exact fun e h ↦ isArtinian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
a b : R
hab : a * b = 1
⊢ b * a = 1

Tactic:
by
    have ⟨c, hca⟩ := IsArtinian.surjective_of_injective_endomorphism
      (.toSpanSingleton R R a) (isRightRegular_of_mul_eq_one hab) 1
    rwa [← left_inv_eq_right_inv hca hab]

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

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy : y ∈ f.range
⊢ ∃ a, f.rangeRestrict a = ⟨y, hy⟩

Tactic:
mem_range

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy✝ : y ∈ f.range
hy : ∃ y_1, f y_1 = y
⊢ ∃ a, f.rangeRestrict a = ⟨y, hy✝⟩
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ ∃ K, K.toSubmodule = p

Tactic:
use { p with lie_mem' := h _ _ }

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

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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I : LieIdeal R L
⊢ ∀ {x y : L}, x ∈ (↑I).carrier → y ∈ (↑I).carrier → ⁅x, y⁆ ∈ (↑I).carrier

Tactic:
by intro x y _ hy; apply lie_mem_right; exact hy

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'
⊢ f.ker = ⊥ ↔ Function.Injective ⇑f

Tactic:
by
  rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule,
    LinearMap.ker_eq_bot, coe_toLinearMap]

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅J, I⁆ ≤ I

Tactic:
exact lie_le_right I J

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
ι : Sort u_1
N : ι → LieSubmodule R L M
⊢ ↑(⨆ i, N i) = ⊤ ↔ ⨆ i, N i = ⊤

Tactic:
← top_toSubmodule (L := L),

Goal state after:
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
ι : Sort u_1
N : ι → LieSubmodule R L M
⊢ ↑(⨆ i, N i) = ↑⊤ ↔ ⨆ i, N i = ⊤
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ f.ker = ⊥ ↔ Function.Injective ⇑f

Tactic:
by
  rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule,
    LinearMap.ker_eq_bot, coe_toLinearMap]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree

Tactic:
have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq
      have H := minpoly.min A x (qmo.comp_X_add_C _) this
      rw [degree_eq_natDegree qmo.ne_zero,
        degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero, natDegree_comp,
        natDegree_X_sub_C, mul_one]
      rwa [degree_eq_natDegree (minpoly.ne_zero hx),
        degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
        natDegree_X_add_C, mul_one] at H

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I ⊓ I₁ = I₁
h₂ : I ⊓ I₂ = I₂
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
rw [h₁, h₂]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: case mp.mem
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y : ↥R[x]
a : R
ha : a ∈ ↑I
⊢ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑((algebraMap R ↥R[x]) a)

Tactic:
exact ⟨C a, fun i ↦ by rw [coeff_C]; aesop, aeval_C _ _⟩

Goal state after: