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

Goal state before:
pp: case pos
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 X' : GradedObject J D
φ : X ⟶ X'
j' : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j')
h : (j', 0) ∈ p ⁻¹' {j'}
⊢ (F.obj (X j')).map (singleObjApplyIso 0 Y).hom ≫ (F.obj (X j')).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j', 0), ⋯⟩ =
    s.inj ⟨(j', 0), h⟩

Tactic:
← Functor.map_comp_assoc,

Goal state after:
case pos
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 X' : GradedObject J D
φ : X ⟶ X'
j' : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j')
h : (j', 0) ∈ p ⁻¹' {j'}
⊢ (F.obj (X j')).map ((singleObjApplyIso 0 Y).hom ≫ (singleObjApplyIso 0 Y).inv) ≫ s.inj ⟨(j', 0), ⋯⟩ =
    s.inj ⟨(j', 0), h⟩
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 X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
m : (mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ s.pt
hm : ∀ (j_1 : ↑(p ⁻¹' {j})), Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) j_1 ≫ m = s.inj j_1
⊢ m =
    e.inv.app (X j) ≫
      (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫
        (F.obj (X j)).map (singleObjApplyIso 0 Y).hom ≫ e.hom.app (X j) ≫ m

Tactic:
← Functor.map_comp_assoc,

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 X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
m : (mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ s.pt
hm : ∀ (j_1 : ↑(p ⁻¹' {j})), Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) j_1 ≫ m = s.inj j_1
⊢ m =
    e.inv.app (X j) ≫
      (F.obj (X j)).map ((singleObjApplyIso 0 Y).inv ≫ (singleObjApplyIso 0 Y).hom) ≫ e.hom.app (X j) ≫ m
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
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv =
    (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).toCycles

Tactic:
simp [← cancel_mono (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂).iCycles]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n : ℤ
hn : n = data.deg pq
⊢ i₁ = data.i₀ r₀ pq ⋯

Tactic:
rw [hi₁, ← data.hi₀₁]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_hom._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_hom._auto_3
⊢ i₁ = data.i₀ r₀ pq ⋯

Tactic:
rw [hi₁, ← data.hi₀₁]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁴ : Category.{?u.6, u_1} C
inst✝³ : Abelian C
inst✝² : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
inst✝¹ : data.HasFirstPageComputation
inst✝ : X.HasSpectralSequence data
pq : κ
i₁ i₂ : ι
hi₁ : i₁ = data.i₁ pq
hi₂ : i₂ = data.i₂ pq
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) spectralSequenceFirstPageXIso_inv._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) spectralSequenceFirstPageXIso_inv._auto_3
⊢ i₁ = data.i₀ r₀ pq ⋯

Tactic:
rw [hi₁, ← data.hi₀₁]

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 k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
y₁ : A₁ ⟶ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
z : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂) := π₁ ≫ x₂ - y₁ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯
⊢ z ≫ (X.sc₂ f₁ f₂ f₁₂ h₁₂ n₁).g = 0

Tactic:
have : z ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = 0 := by simp [z, hy₁]

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.H n₁).obj (mk₁ f₁₂)
hx₂ : x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
y₁ : A₁ ⟶ (X.H n₀).obj (mk₁ f₃)
hy₁ : π₁ ≫ x₂ ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = y₁ ≫ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
z : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂) := π₁ ≫ x₂ - y₁ ≫ X.δ f₁₂ f₃ n₀ n₁ ⋯
this : z ≫ X.toCycles f₁ f₂ f₁₂ h₁₂ n₁ = 0
⊢ z ≫ (X.sc₂ f₁ f₂ f₁₂ h₁₂ n₁).g = 0
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
X✝ Y✝ : Square C
φ : X✝ ⟶ Y✝
⊢ (X✝.map F).f₁₃ ≫ F.map φ.τ₃ = F.map φ.τ₁ ≫ (Y✝.map F).f₁₃

Tactic:
simpa only [Functor.map_comp] using! F.congr_map φ.comm₁₃

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₂
A : C
x₂ : A ⟶ X.cycles f₁ f₂₃ n₁
hx₂ : x₂ ≫ X.iCycles f₁ f₂₃ n₁ ≫ (X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃) = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
x₁ : A₁ ⟶ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ ⋯ ⋯).X₁
hx₁ : π₁ ≫ x₂ ≫ X.iCycles f₁ f₂₃ n₁ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ ⋯ ⋯).f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
exact ⟨A₁, π₁, inferInstance, x₁, by simpa [← cancel_mono (X.iCycles ..)]⟩

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₁
⊢ (h.right.homologyIso ≪≫ h.iso.symm).hom ≫ 𝟙 ((X.H n₁).obj (mk₁ f)) =
    (X.shortComplex (𝟙 i) f (𝟙 j) n₀ n₁ (n₁ + 1) hn₁ hn₂).homologyι ≫ h.right.opcyclesIso.hom

Tactic:
← 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.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₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : β.app 0 = α.app 0
h₁ : β.app 1 = α.app 2
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₁).map (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂) ≫
      (X.H n₁).map
          (homMk₁ ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 1) ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 2)
            ⋯) ≫
        X.pOpcycles f₂' f₃' n₁ =
    (X.H n₁).map (homMk₁ (β.app 0) (β.app 1) ⋯) ≫
      (X.H n₁).map (homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯) ≫
        X.pOpcycles f₂' f₃' n₁

Tactic:
← Functor.map_comp_assoc,

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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
i₀' i₁' i₂' i₃' : ι
f₁' : i₀' ⟶ i₁'
f₂' : i₁' ⟶ i₂'
f₃' : i₂' ⟶ i₃'
f₁₂' : i₀' ⟶ i₂'
h₁₂' : f₁' ≫ f₂' = f₁₂'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₂ f₁₂ f₃ ⟶ mk₂ f₁₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : β.app 0 = α.app 0
h₁ : β.app 1 = α.app 2
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₁).map
        (twoδ₁Toδ₀ f₁ f₂ f₁₂ h₁₂ ≫
          homMk₁ ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 1) ((homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯).app 2)
            ⋯) ≫
      X.pOpcycles f₂' f₃' n₁ =
    (X.H n₁).map (homMk₁ (β.app 0) (β.app 1) ⋯) ≫
      (X.H n₁).map (homMk₁ ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 0) ((threeδ₁Toδ₀ f₁' f₂' f₃' f₁₂' h₁₂').app 1) ⋯) ≫
        X.pOpcycles f₂' f₃' n₁
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆

Tactic:
have h1 := leibniz_lie x y m

Goal state after:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m✝ n : M
t : R
x m : L
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
rw [← lie_skew, ← lie_skew x m, LieAlgebra.lie_smul, smul_neg]

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

Goal state before:

Tactic:
g ⁅x, n⁆ = g ⁅x, f (g n)⁆ := by rw [h₂]
        _ = g (f ⁅x, g n⁆) := by rw [map_lie]
        _ = ⁅x, g n⁆ := h₁ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ nilradical R = iInf MaximalSpectrum.asIdeal

Tactic:
by
  simpa using nilradical_pow_eq_iInf R 1

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

Goal state before:
pp: 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
n : ℕ
hn : Jac ^ n * N = N
⊢ Jac ^ n * (Jac * N) = N

Tactic:
eq

Goal state after:
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
n : ℕ
hn : Jac ^ n * N = N
⊢ Jac ^ n * N = N
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ toEnd R (Module.End R M) M = LieHom.id

Tactic:
ext g m

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : Module.End R M
m : M
⊢ ((toEnd R (Module.End R M) M) g) m = (LieHom.id g) m
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : Module.End R M
m : M
⊢ ((toEnd R (Module.End R M) M) g) m = (LieHom.id g) m

Tactic:
simp [lie_eq_smul]

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 : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
this✝ : I x = N
this : Ideal.span {x} = N
⊢ N ≤ Ring.jacobson R * N

Tactic:
eq

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 ≠ ⊥
this✝ : I x = N
this : Ideal.span {x} = N
⊢ N ≤ N
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' : LieSubalgebra R L
M : Type w
inst✝⁶ : AddCommGroup M
inst✝⁵ : LieRingModule L M
N : Type w₁
inst✝⁴ : AddCommGroup N
inst✝³ : LieRingModule L N
inst✝² : Module R N
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅t • ↑x, m⁆ = t • ⁅x, m⁆

Tactic:
smul_lie,

Goal state after:
R : Type u
L : Type v
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
L' : LieSubalgebra R L
M : Type w
inst✝⁶ : AddCommGroup M
inst✝⁵ : LieRingModule L M
N : Type w₁
inst✝⁴ : AddCommGroup N
inst✝³ : LieRingModule L N
inst✝² : Module R N
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ t • ⁅↑x, m⁆ = t • ⁅x, m⁆
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
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
this : ∀ {x y : L}, x ∈ span R s → y ∈ span R s → ⁅x, y⁆ ∈ span R s
⊢ (lieSpan R L s).toSubmodule = span R s

Tactic:
refine le_antisymm ?_ submodule_span_le_lieSpan

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
this : ∀ {x y : L}, x ∈ span R s → y ∈ span R s → ⁅x, y⁆ ∈ span R s
⊢ (lieSpan R L s).toSubmodule ≤ span R s
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ I.incl.idealRange = I

Tactic:
rw [LieHom.idealRange_eq_lieSpan_range, ← LieSubalgebra.coe_toSubmodule, ←
    LieSubmodule.toSubmodule_inj, incl_range, toLieSubalgebra_toSubmodule,
    LieSubmodule.coe_lieSpan_submodule_eq_iff]
  use I

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

Goal state before:
pp: case h.right
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
x : L
m' : M'
m : M
hm : m ∈ ↑↑N
hfm : f m = m'
⊢ ↑f ⁅x, m⁆ = ⁅x, m'⁆

Tactic:
simp [hfm]

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

Goal state before:
pp: case mpr
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ x = 0 → (minpoly A x).coeff 0 = 0

Tactic:
rintro rfl
    simp

Goal state after:
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
inst✝ : StrongRankCondition R
pb : PowerBasis R S
⊢ Module.finrank R S = pb.dim

Tactic:
rw [Module.finrank_eq_card_basis pb.basis, Fintype.card_fin]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + ⁅L (b * b), L a⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + ⁅L (c * c), L a⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0

Tactic:
← lie_skew (L (b * b)),

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + ⁅L (c * c), L a⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (-⁅L c, L (a * a)⁆ + -⁅L a, L (c * c)⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0

Tactic:
← lie_skew (L (b * b)),

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (-⁅L c, L (a * a)⁆ + -⁅L a, L (c * c)⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (-⁅L c, L (b * b)⁆ + ⁅L (c * c), L b⁆)) =
    0
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst✝ : Invertible x
h : ∃ i ∈ Ideal.map (algebraMap R ↥R[x]) I, ∃ j ∈ Ideal.span {⟨x, ⋯⟩}, i + j = 1
y : ↥R[x]
hy : y ∈ Ideal.map (algebraMap R ↥R[x]) I
z : ↥R[x]
hz : z ∈ Ideal.span {⟨x, ⋯⟩}
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
w : ↥R[x]
q : R[X]
hq : (aeval x) q = ↑w
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq : ↑y + ↑z = 1
hw : ↑z = ↑(⟨x, ⋯⟩ * w)
⊢ (1 - p - X * q).coeff 0 ≠ 0

Tactic:
exact fun h ↦ hI <| by simpa [h, Ideal.eq_top_iff_one]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : (aeval x) (∑ x_1, (monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : ∑ x_1, ((monomial ↑x_1) (g x_1)).coeff ↑i = coeff 0 ↑i
⊢ g i = 0

Tactic:
coeff_monomial,

Goal state after:
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : (aeval x) (∑ x_1, (monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : (∑ x_1, if ↑x_1 = ↑i then g x_1 else 0) = coeff 0 ↑i
⊢ g i = 0
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
⊢ d * d = a * b

Tactic:
eq

Goal state after:
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
⊢ a * b = a * b
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ X.Separable

Tactic:
rw [separable_def, derivative_X]
  exact isCoprime_one_right

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative (f * g))
⊢ f.Separable

Tactic:
derivative_mul

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative f * g + f * derivative g)
⊢ f.Separable
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative (f * g))
⊢ IsCoprime f g

Tactic:
derivative_mul

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative f * g + f * derivative g)
⊢ IsCoprime f g
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) (derivative (q * q * p))
⊢ q * derivative q * p + q * derivative q * p + q * q * derivative p = derivative (q * q) * p + q * q * derivative p

Tactic:
derivative_mul

Goal state after:
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) (derivative (q * q * p))
⊢ q * derivative q * p + q * derivative q * p + q * q * derivative p =
    (derivative q * q + q * derivative q) * p + q * q * derivative p
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ IsCoprime (f * g) (derivative (f * g))

Tactic:
derivative_mul

Goal state after:
R : Type u
inst✝ : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ IsCoprime (f * g) (derivative f * g + f * derivative g)