mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : Φ.HasRightResolutions
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure ↔
    TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom
e' : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
⊢ TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom ↔
    TwoSquare.GuitartExact e.hom

Tactic:
let e'' : (Φ.functor ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
    associator _ _ _ ≪≫ isoWhiskerLeft _ e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : Φ.HasRightResolutions
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
this :
  Φ.IsRightDerivabilityStructure ↔
    TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom
e' : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁
E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂
e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
e'' : (Φ.functor ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F :=
  Φ.functor.associator W₂.Q E₂.functor ≪≫ Φ.functor.isoWhiskerLeft e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F
⊢ TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom ↔
    TwoSquare.GuitartExact e.hom
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE (n + 1)
⊢ Mono { mid := L, ι := f, π := 𝟙 L, ι_π := ⋯ }.ι

Tactic:
by assumption

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

Goal state before:
pp: case hX
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + ↑0
⊢ IsZero (homology K i)

Tactic:
rw [← exactAt_iff_isZero_homology]
        exact exactAt_of_isGE _ (n + 1) i

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

Goal state before:
pp: case hY
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE (n + 1)
i : ℤ
hi : i ≤ n + ↑0
⊢ IsZero (homology L i)

Tactic:
rw [← exactAt_iff_isZero_homology]
        exact exactAt_of_isGE _ (n + 1) i

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.obj.IsStrictlyGE n
L : CochainComplex C ℤ
i : K.obj ⟶ L
w✝¹ : QuasiIso i
w✝ : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE n
L' : CochainComplex (InjectiveObject C) ℤ := HomologicalComplex.liftObjectProperty (isInjective C) L ⋯
hL' : L'.IsStrictlyGE n
⊢ quasiIso C (ObjectProperty.homMk i)

Tactic:
by assumption

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.IsGE n
⊢ K.IsGE n

Tactic:
by assumption

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : K.IsKProjective
⊢ Function.Bijective toSmallShiftedHom

Tactic:
let := HasDerivedCategory.standard C

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : K.IsKProjective
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Function.Bijective toSmallShiftedHom
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: case 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₁)
⊢ (L C).functor.map (Plus.prepathObject { obj := K₂, property := ⋯ }).p₀ =
    (L C).functor.map (Plus.prepathObject { obj := K₂, property := ⋯ }).p₁

pp: case 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₁)
⊢ ((Plus.prepathObject { obj := K₂, property := ⋯ }).map
        (CochainComplex.Plus.localizerMorphism C).functor).RightHomotopy
    (ObjectProperty.homMk f₀) (ObjectProperty.homMk f₁)

Tactic:
· ext : 1
      exact eq_of_homotopy _ _ (pathObject.homotopy₀₁ _ (fun n ↦ ⟨n + 1, by simp⟩))

Goal state after:
case 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₁)
⊢ ((Plus.prepathObject { obj := K₂, property := ⋯ }).map
        (CochainComplex.Plus.localizerMorphism C).functor).RightHomotopy
    (ObjectProperty.homMk f₀) (ObjectProperty.homMk f₁)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain ((singleFunctor C p).obj X) K n
p' q' : ℤ
hpq' : p' + n = q'
hp : ¬p' = p
⊢ ((fun f ↦ fromSingleMk f h)
          ((fun α ↦ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv ≫ α.v p q h) α)).v
      p' q' hpq' =
    α.v p' q' hpq'

Tactic:
· exact (HomologicalComplex.isZero_single_obj_X _ _ _ _ hp).eq_of_src _ _

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 ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α

Tactic:
by
  obtain ⟨f, hf⟩ := Cochain.toSingleMk_surjective α.1 p h
  have hα := ((n + 1).negOnePow • α).δ_eq_zero (n + 1)
  rw [coe_units_smul, δ_units_smul, ← hf, Cochain.δ_toSingleMk _ _ _ p' (by lia),
    smul_smul, Int.units_mul_self, one_smul] at hα
  refine ⟨f, ?_, ?_⟩
  · simpa [← cancel_mono (HomologicalComplex.singleObjXSelf (.up ℤ) q X).inv] using!
    Cochain.congr_v hα p' q (by lia)
  · ext : 1; assumption

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

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K ((singleFunctor C q).obj X) (n - 1)
hα : δ (n - 1) n α = ↑(toSingleMk f h p' hp' hf)
⊢ ∃ g, K.d p p'' ≫ g = f

Tactic:
obtain ⟨g, hg⟩ := Cochain.toSingleMk_surjective α p'' (by lia)

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
α : Cochain K ((singleFunctor C q).obj X) (n - 1)
hα : δ (n - 1) n α = ↑(toSingleMk f h p' hp' hf)
g : K.X p'' ⟶ X
hg : Cochain.toSingleMk g ⋯ = α
⊢ ∃ g, K.d p p'' ≫ g = f
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 : CostructuredArrow (idealPowersToSelfLERadical J) J'
⊢ ∀ (j₂ : CostructuredArrow (idealPowersToSelfLERadical J) J'), Zigzag j1 j₂

Tactic:
j2

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'
⊢ Zigzag j1 j2
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 : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝¹ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y : GradedObject J D
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
j : J
⊢ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y 0 j j ⋯ ≫
      (CofanMapObjFun.iso (mapBifunctorLeftUnitorCofanIsColimit F X e p hp Y j)).inv =
    (F.map (singleObjApplyIso 0 X).hom).app (Y j) ≫ e.hom.app (Y j)

Tactic:
CofanMapObjFun.ιMapObj_iso_inv

Goal state after:
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 : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝¹ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y : GradedObject J D
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
j : J
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩ =
    (F.map (singleObjApplyIso 0 X).hom).app (Y j) ≫ e.hom.app (Y j)
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
inst✝ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
j : J
⊢ ιMapBifunctorMapObj F p X ((single₀ I).obj Y) j 0 j ⋯ ≫
      (CofanMapObjFun.iso (mapBifunctorRightUnitorCofanIsColimit F Y e p hp X j)).inv =
    (F.obj (X j)).map (singleObjApplyIso 0 Y).hom ≫ e.hom.app (X j)

Tactic:
CofanMapObjFun.ιMapObj_iso_inv

Goal state after:
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
inst✝ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
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)
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 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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ IsColimit (CokernelCofork.ofπ (cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)) ⋯)

Tactic:
by
      refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
        (cokernelIsCokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁))
      · exact parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa) (by simp)
      · exact Cofork.ext (Iso.refl _)

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r : ℤ
hr : r₀ ≤ r
pq' : κ
i₂ i₃ : ι
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
⊢ i₂ ≤ i₃

Tactic:
by
  simpa only [hi₂, hi₃] using data.le₂₃ r pq'

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPullback
inst✝ : Mono sq.f₂₄
⊢ MorphismProperty.monomorphisms C sq.f₂₄

Tactic:
by assumption

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPushout
inst✝ : Epi sq.f₁₃
⊢ MorphismProperty.epimorphisms C sq.f₁₃

Tactic:
by assumption

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 ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i j : ι
f : i ⟶ j
hn₂ : n₁ + 1 = n₁ + 1
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂
this :
  h.right.opcyclesIso.hom = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ (X.homologyDataIdId f n₀ n₁ (n₁ + 1) ⋯ ⋯).left.homologyIso.hom ≫ 𝟙 ((X.H n₁).obj (mk₁ f)) =
    ((X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).homologyι ≫
        (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom) ≫
      X.fromOpcycles f (𝟙 j) f ⋯ n₁

Tactic:
rw [Category.assoc, ← this,
    h.left_homologyIso_eq_right_homologyIso_trans_iso_symm,
    ← ShortComplex.RightHomologyData.homologyIso_hom_comp_ι]

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 ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i j : ι
f : i ⟶ j
hn₂ : n₁ + 1 = n₁ + 1
h : (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).HomologyData := X.homologyDataIdId f n₀ n₁ (n₁ + 1) hn₁ hn₂
this :
  h.right.opcyclesIso.hom = (X.opcyclesIso (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).hom ≫ X.fromOpcycles f (𝟙 j) f ⋯ n₁
⊢ (h.right.homologyIso ≪≫ h.iso.symm).hom ≫ 𝟙 ((X.H n₁).obj (mk₁ f)) = h.right.homologyIso.hom ≫ h.right.ι
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ IsRightRegular x✝

Tactic:
exact isUnit_iff_isRightRegular

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
K : LieSubalgebra R L
⊢ K = ⊥ ↔ ∀ x ∈ K, x = 0

Tactic:
rw [_root_.eq_bot_iff]
  exact Iff.rfl

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

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K
x y : L
hx : x ∈ K'
hy : y ∈ K
⊢ ⁅x, y⁆ ∈ K

Tactic:
exact h' ⟨x, hx⟩ ⟨y, h hy⟩ hy

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

Goal state before:
pp: case a
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'
J : LieIdeal R L'
h : f.IsIdealMorphism
⊢ map f (comap f J) ≤ f.idealRange ∧ map f (comap f J) ≤ J

Tactic:
exact ⟨f.map_le_idealRange _, map_comap_le⟩

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra A B
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
⊢ map f (minpoly A x) ≠ 1

Tactic:
by_cases hx : IsIntegral A x

Goal state after:
case pos
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra A B
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : IsIntegral A x
⊢ map f (minpoly A x) ≠ 1

case neg
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra A B
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ map f (minpoly A x) ≠ 1
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
⊢ ¬IsUnit (minpoly A x)

Tactic:
by_cases hx : IsIntegral A x

Goal state after:
case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : IsIntegral A x
⊢ ¬IsUnit (minpoly A x)

case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit (minpoly A x)
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
⊢ minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (X - C a)

Tactic:
by_cases hx : IsIntegral A x

Goal state after:
case pos
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
⊢ minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (X - C a)

case neg
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
⊢ minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (X - C a)
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
⊢ minpoly A (-x) = (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)

Tactic:
by_cases hx : IsIntegral A x

Goal state after:
case pos
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ minpoly A (-x) = (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)

case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ¬IsIntegral A x
⊢ minpoly A (-x) = (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-X)
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: A : Type u_3
inst✝ : CommRing A
I : Ideal A
x y : A
n : ℕ
hxy : x ≡ y [SMOD I]
⊢ x ^ n ≡ y ^ n [SMOD I]

Tactic:
simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_pow] at hxy ⊢
  rw [hxy]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f g : (R ⧸ I)[X]
⊢ (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) (f * g) =
    (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) f *
      (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) g

Tactic:
simp only [coe_eval₂RingHom, eval₂_mul]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ (f %ₘ minpoly A pb.gen).natDegree < (minpoly A pb.gen).natDegree

Tactic:
apply natDegree_lt_natDegree hf

Goal state after:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ (f %ₘ minpoly A pb.gen).degree < (minpoly A pb.gen).degree
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
x : S
hx : B.gen ∈ R[x]
⊢ R[x] = ⊤

Tactic:
by
  rw [_root_.eq_top_iff, ← B.adjoin_gen_eq_top]
  refine adjoin_le ?_
  simp [hx]

Goal state after:
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
⊢ (norm R) ((algebraMap R S) x) = x ^ Fintype.card ι

Tactic:
have := Classical.decEq ι

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ (norm R) ((algebraMap R S) x) = x ^ Fintype.card ι
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x y p : R
k : ℕ
hy : Squarefree y
hp : Prime p
h : p ^ (k + 1) ∣ y * x
⊢ p ^ k ∣ x

Tactic:
exact pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right hy hp h

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
u : Rˣ
a✝ : Nontrivial R
hn : IsUnit ↑0
⊢ (X ^ 0 - C ↑u).Separable

Tactic:
simp at hn

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
⊢ LinearMap.det 0 = 0

Tactic:
have := Classical.decEq ι

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι : Type u_7
inst✝¹ : Finite ι
inst✝ : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
⊢ LinearMap.det 0 = 0