mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Dual R (n → R)
⊢ (fun v ↦ { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ })
      ((fun f i ↦ f ((LinearMap.single R (fun a ↦ R) i) 1)) f) =
    f

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i ↦ x ^ ↑i

Tactic:
rw [minpoly.eq_zero h, natDegree_zero]
    exact linearIndependent_empty_type

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) = 0
⊢ g i = 0

Tactic:
apply_fun lcoeff K i at h0

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 : (lcoeff K ↑i) (∑ x_1, (monomial ↑x_1) (g x_1)) = (lcoeff K ↑i) 0
⊢ g i = 0
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case mpr.inl
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
hu : ¬IsUnit 0
⊢ emultiplicity 0 x ≤ 1

Tactic:
simp [x0]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι' : Type u_7
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
tb : Trunc (Basis ι A M)
b' : Basis ι' A M
f : M →ₗ[A] M
⊢ (detAux tb) f = ((toMatrix b' b') f).det

Tactic:
induction tb using Trunc.induction_on with

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
h : derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ g * ↑u ∣ derivative f

Tactic:
Units.mul_right_dvd

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
h : derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ g ∣ derivative f
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : derivative f = 0
hp : p > 0
this : IsLocalHom (expand F p)
⊢ Irreducible (?m.112 (contract p f))

Tactic:
← expand_contract p H hp.ne'

Goal state after:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf✝ : Irreducible f
hf : Irreducible ((expand F p) (contract p f))
H : derivative f = 0
hp : p > 0
this : IsLocalHom (expand F p)
⊢ Irreducible ((?m.147 H hp this) (contract p f))
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ 1 f = 1

pp: case hnc
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ ¬∃ s, Nonempty (Basis (↥s) R M)

Tactic:
MonoidHom.one_apply

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ 1 = 1

case hnc
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ ¬∃ s, Nonempty (Basis (↥s) R M)
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h.inr.zero
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
ih : ∀ m < 0, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f = C (f.coeff 0)
hf0 : f ≠ 0
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
h1,

Goal state after:
case h.inr.zero
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
ih : ∀ m < 0, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f = C 0
hf0 : f ≠ 0
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
n : ℕ
⊢ (X ^ n - 1).Separable ↔ ↑n ≠ 0

Tactic:
by
  rcases (Nat.eq_zero_or_pos n) with (hz | hpos)
  · simp_all [not_separable_zero]
  · exact X_pow_sub_C_separable_iff hpos one_ne_zero

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case h₀
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial ↑b) (Pi.single i 1 b) = 0

Tactic:
intro j _ hj

Goal state after:
case h₀
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i j : Fin g.natDegree
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ (monomial ↑j) (Pi.single i 1 j) = 0
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: 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
⊢ a.IsSemisimple

Tactic:
have : IsReduced S := by
    simp_rw [S, AdjoinRoot, ← Ideal.isRadical_iff_quotient_reduced, ← isRadical_iff_span_singleton]
    exact (PerfectField.separable_iff_squarefree.mpr hg.minpoly_squarefree).map.squarefree.isRadical

Goal state after:
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
⊢ a.IsSemisimple
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
m n : M
⊢ (let __spread.0 := (↑(LieModule.toEnd R L M)).flip (m + n);
    { toLinearMap := __spread.0, leibniz' := ⋯ }) =
    (let __spread.0 := (↑(LieModule.toEnd R L M)).flip m;
      { toLinearMap := __spread.0, leibniz' := ⋯ }) +
      let __spread.0 := (↑(LieModule.toEnd R L M)).flip n;
      { toLinearMap := __spread.0, leibniz' := ⋯ }

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
t : R
m : M
⊢ (let __spread.0 := (↑(LieModule.toEnd R L M)).flip (t • m);
    { toLinearMap := __spread.0, leibniz' := ⋯ }) =
    (RingHom.id R) t •
      let __spread.0 := (↑(LieModule.toEnd R L M)).flip m;
      { toLinearMap := __spread.0, leibniz' := ⋯ }

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
t : R
x : L
D : LieDerivation R L M
⊢ ⁅t • x, D⁆ = t • ⁅x, D⁆

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
t : R
x : L
D : LieDerivation R L M
⊢ ⁅x, t • D⁆ = t • ⁅x, D⁆

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ↑((ad R L) x) = (LieAlgebra.ad R L) x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
⊢ ⁅(ad R L) x, D⁆ = ⁅x, D⁆

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ (derivative (map (algebraMap R S) P)) * (r₂ - r₁) + u * (r₂ - r₁) ^ 2
this : IsUnit ((aeval r₁) (derivative P))
⊢ IsUnit ((aeval r₁) (derivative P) + u * (r₂ - r₁))

Tactic:
← sub_sub_sub_cancel_right r₂ r₁ x

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
r₁ r₂ : S
x✝¹ : IsNilpotent (r₁ - x) ∧ (aeval r₁) P = 0
x✝ : IsNilpotent (r₂ - x) ∧ (aeval r₂) P = 0
hr₁ : IsNilpotent (r₁ - x)
hr₁' : (aeval r₁) P = 0
hr₂ : IsNilpotent (r₂ - x)
hr₂' : (aeval r₂) P = 0
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ (derivative (map (algebraMap R S) P)) * (r₂ - r₁) + u * (r₂ - r₁) ^ 2
this : IsUnit ((aeval r₁) (derivative P))
⊢ IsUnit ((aeval r₁) (derivative P) + u * (r₂ - x - (r₁ - x)))
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal p
⊢ i + j = p

Tactic:
simpa using hij

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

Goal state before:
pp: case mpr
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
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
N : LieSubmodule R L M
m : M
⊢ (∃ a ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}, ↑(toModuleHom R L M) a = m) → ∃ x n, ⁅↑x, ↑n⁆ = m

Tactic:
rintro ⟨t, ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩, h⟩; rw [← h]; use ⟨x, hx⟩, ⟨n, hn⟩; rfl

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

Goal state before:
pp: case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : M
⊢ ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (a₃ ⊗ₜ[R] l₃)) =
    ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (a₃ ⊗ₜ[R] l₃) +
      ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (a₃ ⊗ₜ[R] l₃))

Tactic:
simp only [bracket'_tmul]

Goal state after:
case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
a₃ : A
l₃ : M
⊢ (a₁ * (a₂ * a₃)) ⊗ₜ[R] ⁅l₁, ⁅l₂, l₃⁆⁆ = (a₁ * a₂ * a₃) ⊗ₜ[R] ⁅⁅l₁, l₂⁆, l₃⁆ + (a₂ * (a₁ * a₃)) ⊗ₜ[R] ⁅l₂, ⁅l₁, l₃⁆⁆
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y z : A ⊗[R] L
⊢ ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆

Tactic:
simp only [bracket_def, map_add]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : A ⊗[R] L
y z : A ⊗[R] M
⊢ ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆

Tactic:
simp only [bracket_def, map_add]

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

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 : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
⊢ (mk' N).ker = N

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
⊢ map (↑g) (m • C b) = (MonoidHom.id M) m • map (↑g) (C b)

Tactic:
MonoidHom.id_apply,

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
⊢ map (↑g) (m • C b) = m • map (↑g) (C b)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L (M ⧸ N) k

Tactic:
exact map_lowerCentralSeries_le k (LieSubmodule.Quotient.mk' N)

Goal state after:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ map (↑g) (m • (C b * X ^ (n + 1))) = (MonoidHom.id M) m • map (↑g) (C b * X ^ (n + 1))

Tactic:
MonoidHom.id_apply,

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ map (↑g) (m • (C b * X ^ (n + 1))) = m • map (↑g) (C b * X ^ (n + 1))
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.ofVectorSpaceIndex K V).Finite → IsNoetherian K V

Tactic:
· intro hbfinite
    refine
      @isNoetherian_of_linearEquiv K K (⊤ : Submodule K V) V _ _ _ _ _ _ (RingHom.id K) _ _ _
        (LinearEquiv.ofTop _ rfl) (id ?_)
    refine isNoetherian_of_fg_of_noetherian _ ⟨Set.Finite.toFinset hbfinite, ?_⟩
    rw [Set.Finite.coe_toFinset, ← b.span_eq, Basis.coe_ofVectorSpace, Subtype.range_coe]

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
⊢ (∃ k, lowerCentralSeries R (↥(toEnd R L M).range) M k = ⊥) ↔ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
constructor <;> rintro ⟨k, hk⟩ <;> use k <;>
      rw [← LieSubmodule.toSubmodule_inj] at hk ⊢ <;>
    simpa using hk

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

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
⊢ ↑(I.lcs M (k + 1)) = ↑(lowerCentralSeries R (↥I) M (k + 1))

Tactic:
simp_rw [lowerCentralSeries_succ, lcs_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (I.lcs M k).mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule, LieSubmodule.mem_top,
      true_and, (I : LieSubalgebra R L).coe_bracket_of_module]
    simp

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Algebraic

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this✝ : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≤ finrank (↥F) L

pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this✝ : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≠ finrank (↥F) L

Tactic:
· exact Module.finrank_top_le_finrank_of_isScalarTower _ _ _

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this✝ : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≠ finrank (↥F) L
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K
inst✝¹⁴ : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹³ : Field K₁
inst✝¹² : Field K₂
inst✝¹¹ : Field K₃
inst✝¹⁰ : Algebra F K₁
inst✝⁹ : Algebra F K₂
inst✝⁸ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
inst✝⁵ : Algebra E K₁
inst✝⁴ : Algebra E K₂
inst✝³ : Algebra E K₃
inst✝² : IsScalarTower F E K₁
inst✝¹ : IsScalarTower F E K₂
inst✝ : IsScalarTower F E K₃
h : Normal F E
x : ↥(toAlgHom F E K₁).range
this : Subalgebra.map ϕ (toAlgHom F E K₁).range ≤ ?m.176
⊢ ϕ ↑x ∈ (toAlgHom F E K₂).range

Tactic:
exact this ⟨x, Subtype.mem x, rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁹ : Field F
inst✝⁸ : CommRing A
inst✝⁷ : Algebra F A
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
inst✝² : Field L
inst✝¹ : Algebra F L
g : A →ₐ[F] L
inst✝ : IsScalarTower F A K
hg : Function.Injective ⇑g
⊢ (↑(liftAlgHom hg)).comp (algebraMap A K) = ↑g

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁹ : Field F
inst✝⁸ : CommRing A
inst✝⁷ : Algebra F A
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
inst✝² : Field L
inst✝¹ : Algebra F L
g : A →ₐ[F] L
inst✝ : IsScalarTower F A K
hg : Function.Injective ⇑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑(liftAlgHom hg)).comp (algebraMap A K) = ↑g

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ p.roots
r_nu : ¬IsUnit (a - ↑ₐ r)
⊢ r ∈ σ a

Tactic:
rwa [mem_iff, ← IsUnit.sub_iff]

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

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Ring K
inst✝² : IsDomain K
hk : IsAlgClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsIntegral k K
x : K
hq : (minpoly k x).leadingCoeff = 1
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x

Tactic:
have h : (minpoly k x).degree = 1 := degree_eq_one_of_irreducible k (minpoly.irreducible
    (Algebra.IsIntegral.isIntegral x))

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Ring K
inst✝² : IsDomain K
hk : IsAlgClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsIntegral k K
x : K
hq : (minpoly k x).leadingCoeff = 1
h : (minpoly k x).degree = 1
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹⁶ : Field k
K : Type u
inst✝¹⁵ : Field K
L : Type v
M : Type w
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : Field M
inst✝¹¹ : Algebra K M
inst✝¹⁰ : IsAlgClosed M
inst✝⁹ : Algebra.IsAlgebraic K L
R : Type u
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type v
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
inst✝³ : Algebra R M
inst✝² : IsTorsionFree R S
inst✝¹ : IsTorsionFree R M
inst✝ : Algebra.IsAlgebraic R S
this✝ : IsDomain R := Function.Injective.isDomain (algebraMap R S) (FaithfulSMul.algebraMap_injective R S)
this : Algebra (FractionRing R) (FractionRing S) := FractionRing.liftAlgebra R (FractionRing S)
⊢ Algebra.IsAlgebraic (FractionRing R) (FractionRing S)

Tactic:
have := FractionRing.isScalarTower_liftAlgebra R (FractionRing S)

Goal state after:
k : Type u
inst✝¹⁶ : Field k
K : Type u
inst✝¹⁵ : Field K
L : Type v
M : Type w
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : Field M
inst✝¹¹ : Algebra K M
inst✝¹⁰ : IsAlgClosed M
inst✝⁹ : Algebra.IsAlgebraic K L
R : Type u
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type v
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
inst✝³ : Algebra R M
inst✝² : IsTorsionFree R S
inst✝¹ : IsTorsionFree R M
inst✝ : Algebra.IsAlgebraic R S
this✝¹ : IsDomain R := Function.Injective.isDomain (algebraMap R S) (FaithfulSMul.algebraMap_injective R S)
this✝ : Algebra (FractionRing R) (FractionRing S) := FractionRing.liftAlgebra R (FractionRing S)
this : IsScalarTower R (FractionRing R) (FractionRing S)
⊢ Algebra.IsAlgebraic (FractionRing R) (FractionRing S)