mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Homotopy φ₁ φ₂
a : R
⊢ a • φ₁.τ₂ = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂

Tactic:
rw [h.comm₂]

Goal state after:
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 : Homotopy φ₁ φ₂
a : R
⊢ a • (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂
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:
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: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
pq : ℤ × Fin l
⊢ pq.2.castSucc ≤ pq.2.succ

Tactic:
by simp [Fin.le_iff_val_le_val]

Goal state after:
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:
by 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 j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₂₃ : j ⟶ l
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₂ ≫ biprod.lift ((X.H n₁).map (twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) (X.δ f₁ f₂₃ n₁ n₂ ⋯) = 0
⊢ X.liftOpcycles f₂ f₃ f₂₃ h₂₃ x₂ ⋯ ≫ (X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = 0

Tactic:
by
        dsimp
        rw [← X.fromOpcyles_δ f₁ f₂ f₃ f₂₃ h₂₃ n₁ n₂,
          X.liftOpcycles_fromOpcycles_assoc]
        simpa using hx₂ =≫ biprod.snd

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

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

Tactic:
by
  dsimp
  rw [Preadditive.mono_iff_cancel_zero]
  intro A x hx
  replace hx := hx =≫ X.fromOpcycles f₁₂ f₃ _ rfl n₁
  rw [zero_comp, Category.assoc,
    X.opcyclesMap_fromOpcycles f₁ f₂₃ f₁₂ f₃ (f₁₂ ≫ f₃) (by cat_disch) _ rfl _ (𝟙 _) n₁
      (by simp) (by cat_disch), Functor.map_id, Category.comp_id] at hx
  rw [← cancel_mono (X.fromOpcycles f₁ f₂₃ (f₁₂ ≫ f₃) (by cat_disch) n₁), hx, zero_comp]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
x : R
⊢ IsUnit x ↔ IsRegular x

Tactic:
by
  rw [isRegular_iff, ← isUnit_iff_isLeftRegular, and_iff_left_of_imp (·.isRegular.2)]

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
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}
ne : ∀ x ∈ N, I x = ⊥
⊢ ∀ r ∈ Jac ^ n, ∀ s ∈ N, r * s ∈ ⊥

Tactic:
refine fun ri hi rn hn ↦ ?_

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
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}
ne : ∀ x ∈ N, I x = ⊥
ri : R
hi : ri ∈ Jac ^ n
rn : R
hn : rn ∈ N
⊢ ri * rn ∈ ⊥
Module: Mathlib.Algebra.Lie.IdealOperations

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
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
x : L
hx : x ∈ I
m : M
hm : m ∈ N
⊢ ⁅↑⟨x, hx⟩, ↑⟨m, hm⟩⁆ ∈ ↑N'

Tactic:
exact h x hx m hm

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
motive : M → Prop
x : M
hx : x ∈ ⨆ i, N i
mem : ∀ (i : ι), ∀ y ∈ N i, motive y
zero : motive 0
add : ∀ (y z : M), motive y → motive z → motive (y + z)
⊢ motive x

Tactic:
rw [← LieSubmodule.mem_toSubmodule, LieSubmodule.iSup_toSubmodule] at hx

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
motive : M → Prop
x : M
hx : x ∈ ⨆ i, ↑(N i)
mem : ∀ (i : ι), ∀ y ∈ N i, motive y
zero : motive 0
add : ∀ (y z : M), motive y → motive z → motive (y + z)
⊢ motive x
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mp
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
N : LieSubmodule R L M
⊢ Nontrivial ↥N → N ≠ ⊥

Tactic:
rintro ⟨⟨m₁, h₁⟩, ⟨m₂, h₂⟩, h₁₂⟩ rfl

Goal state after:
case mp
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
m₁ m₂ : M
h₁ : m₁ ∈ ⊥
h₂ : m₂ ∈ ⊥
h₁₂ : ⟨m₁, h₁⟩ ≠ ⟨m₂, h₂⟩
⊢ False
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
M : 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
I : LieIdeal R L
⊢ ↑⁅I, maxTrivSubmodule R L M⁆ = ↑⊥

Tactic:
LieSubmodule.lieIdeal_oper_eq_linear_span,

Goal state after:
R : Type u
L : Type v
M : 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
I : LieIdeal R L
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = ↑⊥
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
int : IsIntegral A x
⊢ 2 ≤ (minpoly A x).natDegree ↔ x ∉ (algebraMap A B).range

Tactic:
by
  rw [iff_not_comm, ← natDegree_eq_one_iff, not_le]
  exact ⟨fun h ↦ h.trans_lt one_lt_two, fun h ↦ by linarith only [minpoly.natDegree_pos int, h]⟩

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ ↑⁅map f I₁, map f I₂⁆ ≤ Submodule.map ↑f ↑⁅I₁, I₂⁆

Tactic:
LieSubmodule.lieIdeal_oper_eq_linear_span,

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ Submodule.map ↑f ↑⁅I₁, I₂⁆
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ Submodule.map ↑f ↑⁅I₁, I₂⁆

Tactic:
LieSubmodule.lieIdeal_oper_eq_linear_span,

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : Function.Surjective ⇑f
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ Submodule.map (↑f) (Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x})
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₂ : LieIdeal R L
⊢ map I₁.incl (comap I₁.incl I₂) = I₁.incl.idealRange ⊓ I₂

Tactic:
← map_comap_eq

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I₁ I₂ : LieIdeal R L
⊢ map I₁.incl (comap I₁.incl I₂) = map I₁.incl (comap I₁.incl I₂)

R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I₁ I₂ : LieIdeal R L
⊢ I₁.incl.IsIdealMorphism
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
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : (minpoly A x).degree ≤ (q.comp (X + C a)).degree
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree

Tactic:
degree_eq_natDegree (minpoly.ne_zero hx),

Goal state after:
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
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : ↑(minpoly A x).natDegree ≤ (q.comp (X + C a)).degree
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ Submodule.comap ↑f ↑⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ =
    Submodule.comap (↑f) (Submodule.map ↑f ↑⁅comap f J₁, comap f J₂⁆)

Tactic:
LieSubmodule.lieIdeal_oper_eq_linear_span,

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ Submodule.comap (↑f) (Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}) =
    Submodule.comap (↑f) (Submodule.map ↑f ↑⁅comap f J₁, comap f J₂⁆)
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
ι : Type u_6
s : Finset ι
x y : ι → M
hxy : ∀ i ∈ s, x i ≡ y i [SMOD U]
⊢ ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => simp [SModEq.rfl]
  | cons i s _ ih =>
    grw [Finset.sum_cons, Finset.sum_cons, hxy i (Finset.mem_cons_self i s),
      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ Submodule.comap (↑f) (Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}) =
    Submodule.comap (↑f) (Submodule.map ↑f ↑⁅comap f J₁, comap f J₂⁆)

Tactic:
LieSubmodule.lieIdeal_oper_eq_linear_span,

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ Submodule.comap (↑f) (Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}) =
    Submodule.comap (↑f) (Submodule.map (↑f) (Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}))
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
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : f pb.gen = g pb.gen
⊢ f = g

Tactic:
ext x
  obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
  rw [← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]

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

Goal state before:
pp: 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 : Ideal.map (algebraMap R ↥R[x]) I ⊔ Ideal.span {⟨x, ⋯⟩} = ⊤
⊢ ∃ p, p.leadingCoeff - 1 ∈ I ∧ (aeval ⅟x) p = 0

Tactic:
by
  rw [← Ideal.one_eq_top, ← Ideal.add_eq_sup, Ideal.add_eq_one_iff] at h
  have ⟨y, hy, z, hz, eq⟩ := h
  have ⟨p, hp⟩ := (mem_ideal_map_adjoin ..).mp hy
  have ⟨w, hw⟩ := Ideal.mem_span_singleton.mp hz
  have ⟨q, hq⟩ := adjoin_eq_exists_aeval R x w
  use (1 - p - X * q).reverse
  have : (1 - p - X * q).coeff 0 - 1 ∈ I := by simpa using hp.1 0
  apply_fun (·.1) at eq hw
  dsimp at eq
  rw [reverse_leadingCoeff, trailingCoeff_eq_coeff_zero]
  · exact ⟨this, (eval₂_reverse_eq_zero_iff ..).mpr <| by simp [← aeval_def, hp.2, hq, ← eq, hw]⟩
  · exact fun h ↦ hI <| by simpa [h, Ideal.eq_top_iff_one]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : (Multiset.map (fun a ↦ X - C a) s).prod.Separable
⊢ s.Nodup

Tactic:
rw [Multiset.nodup_iff_ne_cons_cons]
  rintro a t rfl
  refine not_isUnit_X_sub_C a (isUnit_of_self_mul_dvd_separable hs ?_)
  simpa only [Multiset.map_cons, Multiset.prod_cons] using mul_dvd_mul_left _ (dvd_mul_right _ _)

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
hn : n ≠ 0
⊢ derivative ((expand F (p ^ n)) f) = 0

Tactic:
rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case monomial
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S[X]
n : ℕ
a : R
a✝ : (aeval (root f)) (C a * X ^ n) = (mk f) (Polynomial.map (algebraMap R S) (C a * X ^ n))
⊢ (aeval (root f)) (C a * X ^ (n + 1)) = (mk f) (Polynomial.map (algebraMap R S) (C a * X ^ (n + 1)))

Tactic:
simp_all [pow_add, ← mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case inr
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
r : ℕ
h₂ : r ∈ Ico k (nilpotencyClass a)
⊢ ((↑r !)⁻¹ • a ^ r) • m = 0

Tactic:
rw [smul_assoc, ← pow_sub_mul_pow a (mem_Ico.1 h₂).1, mul_smul, h, smul_zero, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inr.inl
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
j : n
k : m
⊢ e ↑(bW k) ∈ W

Tactic:
exact he (Submodule.coe_mem (bW k))

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: case inr
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁴ : Module.Finite K R
this✝³ : Module.Finite R S
this✝² : Module.Finite K S
this✝¹ : IsArtinianRing R
this✝ : IsReduced R
this : IsReduced S
φ : S →ₐ[K] End K M :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
x : End K M
hx : x ∈ {g}
⊢ g ∈ ↑φ.range

Tactic:
exact ⟨AdjoinRoot.root _, eval₂_X _ _⟩

Goal state after:
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
a b : K[X]
h : a * P ^ k + b * P' = 1
⊢ (aeval f) b * (aeval f) P' = 1

Tactic:
simpa only [map_add, map_mul, map_one, minpoly.dvd_iff.mp nil, mul_zero, zero_add]
        using (aeval f).congr_arg h

Goal state after:
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
⊢ ∃ n ∈ K[f], ∃ s ∈ K[f], IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
set ff : adjoin K {f} := ⟨f, self_mem_adjoin_singleton K f⟩
  set P' := derivative P
  have nil' : IsNilpotent (aeval ff P) := by
    use k
    obtain ⟨q, hq⟩ := nil
    rw [← map_pow, Subtype.ext_iff]
    simp [ff, hq]
  have sep' : IsUnit (aeval ff P') := by
    obtain ⟨a, b, h⟩ : IsCoprime (P ^ k) P' := sep.pow_left
    replace h : (aeval f b) * (aeval f P') = 1 := by
      simpa only [map_add, map_mul, map_one, minpoly.dvd_iff.mp nil, mul_zero, zero_add]
        using (aeval f).congr_arg h
    refine .of_mul_eq_one_right (aeval ff b) (Subtype.ext_iff.mpr ?_)
    simpa [ff, coe_aeval_mk_apply] using h
  obtain ⟨⟨s, mem⟩, ⟨⟨k, hk⟩, hss⟩, -⟩ := existsUnique_nilpotent_sub_and_aeval_eq_zero nil' sep'
  refine ⟨f - s, ?_, s, mem, ⟨k, ?_⟩, ?_, (sub_add_cancel f s).symm⟩
  · exact sub_mem (self_mem_adjoin_singleton K f) mem
  · rw [Subtype.ext_iff] at hk
    simpa using hk
  · replace hss : aeval s P = 0 := by rwa [Subtype.ext_iff, coe_aeval_mk_apply] at hss
    exact isSemisimple_of_squarefree_aeval_eq_zero sep.squarefree hss

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
h : IsNilpotent a
⊢ exp a * exp (-a) = 1

Tactic:
simp [← exp_add_of_commute (Commute.neg_right rfl) h h.neg]

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

Goal state before:
pp: case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x y : L
hy : y ∈ H
hx : ⁅⟨y, hy⟩, (LieSubmodule.Quotient.mk' H.toLieSubmodule) x⁆ = 0
⊢ ⁅y, x⁆ ∈ H

Tactic:
rwa [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero] at hx

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

Goal state before:
pp: R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
⊢ IsSolvable (A ⊗[R] L) ↔ IsSolvable L

Tactic:
refine ⟨?_, fun _ ↦ inferInstance⟩
  rw [isSolvable_iff A, isSolvable_iff R]
  rintro ⟨k, h⟩
  use k
  rw [eq_bot_iff] at h ⊢
  intro x hx
  rw [derivedSeries_baseChange] at h
  specialize h <| Submodule.tmul_mem_baseChange_of_mem 1 hx
  rw [LieSubmodule.mem_bot] at h ⊢
  rwa [Module.FaithfullyFlat.one_tmul_eq_zero_iff] at h

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable ↥I
⊢ derivedAbelianOfIdeal I = ⊥ ↔ I = ⊥

Tactic:
by
  dsimp only [derivedAbelianOfIdeal]
  split
  · simp_all only [derivedLength_zero]
  · rename_i k h
    obtain ⟨_, h₂⟩ := (derivedSeries_of_derivedLength_succ R L I k).mp h
    have h₃ : I ≠ ⊥ := by rintro rfl; apply h₂; apply derivedSeries_of_bot_eq_bot
    simp only [h₂, h₃]

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

Goal state before:
pp: R : Type u
L : Type v
M : 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
⊢ IsNilpotent L M ↔ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
simp [isNilpotent_iff_int, SetLike.ext'_iff, coe_lowerCentralSeries_eq_int R L M]

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ baseChange A I
m : A ⊗[R] M
hm : m ∈ baseChange A N
⊢ ⁅x, m⁆ ∈ ↑(Submodule.span A s)

Tactic:
rw [mem_baseChange_iff] at hx hm

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ⁅x, m⁆ ∈ ↑(Submodule.span A s)
Module: Mathlib.FieldTheory.Finiteness

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
⊢ span K (Basis.ofVectorSpaceIndex K V) = span K (Set.range ⇑b)

Tactic:
Basis.coe_ofVectorSpace,

Goal state after:
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
⊢ span K (Basis.ofVectorSpaceIndex K V) = span K (Set.range Subtype.val)