mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ x ∈ s, x ≠ a → IsCoprime (f x) (f a)) ∧ ∀ x ∈ s, ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ (f a * ∏ x ∈ s, f x).Separable

Tactic:
exact
      h2.1.mul (ih h1.2.2 h2.2)
        (IsCoprime.prod_right fun i his => h1.1.2 i his <| Ne.symm <| ne_of_mem_of_not_mem his has)

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case hMM'
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_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ c.toMatrix ⇑c = 1

Tactic:
Basis.toMatrix_self

Goal state after:
case hMM'
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_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ 1 = 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
⊢ (X ^ n - C ↑u).Separable

Tactic:
nontriviality R
  rcases n.eq_zero_or_pos with (rfl | hpos)
  · simp at hn
  apply (separable_def' (X ^ n - C (u : R))).2
  obtain ⟨n', hn'⟩ := hn.exists_left_inv
  refine ⟨-C ↑u⁻¹, C (↑u⁻¹ : R) * C n' * X, ?_⟩
  rw [derivative_sub, derivative_C, sub_zero, derivative_pow X n, derivative_X, mul_one]
  calc
    -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1)) =
        C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) := by
      simp only [C.map_mul, C_eq_natCast]
      ring
    _ = 1 := by
      simp only [Units.inv_mul, hn', C.map_one, mul_one, ← pow_succ',
        Nat.sub_add_cancel (show 1 ≤ n from hpos), sub_add_cancel]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case hM'M
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_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ b.toMatrix ⇑b = 1

Tactic:
Basis.toMatrix_self

Goal state after:
case hM'M
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_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ 1 = 1
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case prime
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
⊢ PerfectField K

Tactic:
refine PerfectField.mk fun hf ↦ ?_

Goal state after:
case prime
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
f✝ : K[X]
hf : Irreducible f✝
⊢ f✝.Separable
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ n₁ = n₁ ∧ g₂ = g₂

Tactic:
constructor <;> rfl

Goal state after:
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
x✝ : 𝕜[X]
⊢ (∀ (x : M), ((aeval f) x✝) x = 0 x) ↔ x✝ ∈ Module.annihilator 𝕜[X] (Module.AEval' f)

Tactic:
Module.mem_annihilator

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
x✝ : 𝕜[X]
⊢ (∀ (x : M), ((aeval f) x✝) x = 0 x) ↔ ∀ (m : Module.AEval' f), x✝ • m = 0
Module: Mathlib.Algebra.Lie.AdjointAction.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent (LinearMap.mulLeft R a)

Tactic:
rwa [LinearMap.isNilpotent_mulLeft_iff]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
⊢ Function.Injective ⇑(of f)

Tactic:
injective_iff_map_eq_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
⊢ ∀ (a : R), (of f) a = 0 → a = 0
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
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
k : ℕ
ih : map f (derivedSeriesOfIdeal R L' k ⊤) ≤ derivedSeriesOfIdeal R L k ⊤
⊢ map f ⁅derivedSeriesOfIdeal R L' k ⊤, derivedSeriesOfIdeal R L' k ⊤⁆ ≤
    ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆

Tactic:
exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie ih ih)

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

Goal state before:
pp: case refine_3.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
y₁ y₂ : A ⊗[R] L
hy₁ : ((bracket' R A L L) y₁) z₂ + ((bracket' R A L L) z₂) y₁ = 0
hy₂ : ((bracket' R A L L) y₂) z₂ + ((bracket' R A L L) z₂) y₂ = 0
⊢ ((bracket' R A L L) (y₁ + y₂)) z₂ + ((bracket' R A L L) z₂) (y₁ + y₂) = 0

Tactic:
simp only [add_add_add_comm, hy₁, hy₂, add_zero, LinearMap.add_apply, map_add]

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
N₁ N₂ : LieSubmodule R L M
k : ℕ
⊢ lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp only [LieSubmodule.lcs_succ, ih, LieSubmodule.lie_sup]

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
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLength R ↥I = derivedLengthOfIdeal R L I

Tactic:
change sInf s₁ = sInf s₂

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s₁ = sInf s₂
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✝¹⁶ : 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
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L),
    (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x) y) =
        ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x))
          ((TensorProduct.map f.toLinearMap ↑g) y) →
      (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y_1) y) =
          ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y_1))
            ((TensorProduct.map f.toLinearMap ↑g) y) →
        (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x + y_1)) y) =
          ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x + y_1)))
            ((TensorProduct.map f.toLinearMap ↑g) y)

Tactic:
· intro _ _
        refine y.induction_on (by simp) (fun _ _ h ↦ by simp [h]) (by simp_all)

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✝⁷ : 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
N : LieSubmodule R L M
⊢ ∀ {x : A ⊗[R] L} {m : A ⊗[R] M},
    m ∈ (Submodule.baseChange A ↑N).carrier → ⁅x, m⁆ ∈ (Submodule.baseChange A ↑N).carrier

Tactic:
by
      intro x m hm
      rw [Submodule.mem_carrier, SetLike.mem_coe] at hm ⊢
      rw [Submodule.baseChange_eq_span] at hm
      obtain ⟨c, rfl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp hm
      refine x.induction_on (by simp) (fun a y ↦ ?_) (fun y z hy hz ↦ ?_)
      · change toEnd A (A ⊗[R] L) (A ⊗[R] M) _ _ ∈ _
        simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, map_smul, toEnd_apply_apply]
        refine Submodule.sum_mem _ fun ⟨_, n, hn, h⟩ _ ↦ Submodule.smul_mem _ _ ?_
        rw [Subtype.coe_mk, ← h]
        exact Submodule.tmul_mem_baseChange_of_mem _ (N.lie_mem hn)
      · rw [add_lie]
        exact ((N : Submodule R M).baseChange A).add_mem hy hz

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
k : ℕ
N : LieSubmodule R L M
M₂✝ : Type w₁
inst✝⁶ : AddCommGroup M₂✝
inst✝⁵ : Module R M₂✝
inst✝⁴ : LieRingModule L M₂✝
inst✝³ : LieModule R L M₂✝
inst✝² : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst✝¹ : IsNilpotent L ↥M₁
inst✝ : IsNilpotent L ↥M₂
⊢ IsNilpotent L ↥(M₁ ⊔ M₂)

Tactic:
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L M₁
  obtain ⟨l, hl⟩ := IsNilpotent.nilpotent R L M₂
  let lcs_eq_bot {m n} (N : LieSubmodule R L M) (le : m ≤ n) (hn : lowerCentralSeries R L N m = ⊥) :
    lowerCentralSeries R L N n = ⊥ := by
    simpa [hn] using antitone_lowerCentralSeries R L N le
  have h₁ : lowerCentralSeries R L M₁ (k ⊔ l) = ⊥ := lcs_eq_bot M₁ (Nat.le_max_left k l) hk
  have h₂ : lowerCentralSeries R L M₂ (k ⊔ l) = ⊥ := lcs_eq_bot M₂ (Nat.le_max_right k l) hl
  refine (isNilpotent_iff R L (M₁ + M₂)).mpr ⟨k ⊔ l, ?_⟩
  simp [LieSubmodule.add_eq_sup, (M₁ ⊔ M₂).lowerCentralSeries_eq_lcs_comap, LieSubmodule.lcs_sup,
    (M₁.lowerCentralSeries_eq_bot_iff_lcs_eq_bot (k ⊔ l)).1 h₁,
    (M₂.lowerCentralSeries_eq_bot_iff_lcs_eq_bot (k ⊔ l)).1 h₂, LieSubmodule.comap_incl_eq_bot]

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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
use k + 1

Goal state after:
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 = ⊥
⊢ lowerCentralSeries R L M (k + 1) = ⊥
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent ((ad R ↥L') ↑x)
X : ↥L'
HX : X ∈ K
⊢ X ∈ Submodule.comap ((ad R ↥L') ↑x) ↑K.toLieSubmodule

Tactic:
simp only [LieSubalgebra.coe_toLieSubmodule, Submodule.mem_comap, ad_apply,
        LieSubalgebra.mem_toSubmodule]

Goal state after:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
this : Nontrivial (↥L' ⧸ K.toLieSubmodule)
x : ↥K
hx : IsNilpotent ((ad R ↥L') ↑x)
X : ↥L'
HX : X ∈ K
⊢ ⁅↑x, X⁆ ∈ K
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : (Polynomial.map (algebraMap K F) f).Splits
hf0 : f = 0
⊢ L →ₐ[K] ↥⊥

Tactic:
rw [← (splits_iff L f).1 (show f.Splits by simp [hf0])]
        exact Algebra.toTop

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: case refine_1
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ x ∈ ∅, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Algebra.adjoin F ↑∅) →ₐ[F] L)

Tactic:
rw [coe_empty, Algebra.adjoin_empty]
      exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
⊢ restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)

Tactic:
by
  rw [← adjoin_self _ K, adjoin_adjoin_left, adjoin_self _ K]

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

Goal state before:
pp: F : Type u_1
inst✝⁹ : Field F
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
S : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : Field A
inst✝⁵ : Field B
inst✝⁴ : Field C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
⊢ ↑((AlgHom.restrictScalars A (Algebra.ofId B C)).comp A⟮b⟯.val) x ∈ A⟮(algebraMap B C) b⟯

Tactic:
rw [show (algebraMap B C) b = (Algebra.ofId B C).restrictScalars A b by rfl,
        ← Set.image_singleton, ← IntermediateField.adjoin_map A {b}]

Goal state after:
F : Type u_1
inst✝⁹ : Field F
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
S : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : Field A
inst✝⁵ : Field B
inst✝⁴ : Field C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
⊢ ↑((AlgHom.restrictScalars A (Algebra.ofId B C)).comp A⟮b⟯.val) x ∈
    map (AlgHom.restrictScalars A (Algebra.ofId B C)) A⟮b⟯
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
x : k[X]
hu : x ∈ nonunits k[X]
h0 : x ≠ 0
w✝¹ w✝ : k[X]
h : ∀ (a : K), (aeval a) (x * w✝¹) ≠ 0 ∨ (aeval a) (x * w✝) ≠ 0
⊢ (map (algebraMap k K) x).degree ≠ 0

Tactic:
by
      simpa only [degree_map] using (ne_of_lt <| degree_pos_of_ne_zero_of_nonunit h0 hu).symm

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Field K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := ↥(adjoin F ↑S) →ₐ[F] K
ω : Ω
θ : ↑c → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = (↑π).carrier ⊔ adjoin F ↑S
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (Set.range θ)

Tactic:
simp_rw [← restrictScalars_adjoin_eq_sup, restrictScalars_adjoin] at eq

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Field K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := ↥(adjoin F ↑S) →ₐ[F] K
ω : Ω
θ : ↑c → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = adjoin F (↑(↑π).carrier ∪ ↑S)
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (Set.range θ)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
h : IsIntegral F α
⊢ (adjoinRootEquivAdjoin F h).symm (AdjoinSimple.gen F α) = AdjoinRoot.root (minpoly F α)

Tactic:
AlgEquiv.symm_apply_eq,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
h : IsIntegral F α
⊢ AdjoinSimple.gen F α = (adjoinRootEquivAdjoin F h) (AdjoinRoot.root (minpoly F α))
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = C f.leadingCoeff * minpoly K x
hi : f ≠ 0
⊢ f.natDegree ∣ finrank K L

Tactic:
key,

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = C f.leadingCoeff * minpoly K x
hi : f ≠ 0
⊢ (C f.leadingCoeff * minpoly K x).natDegree ∣ finrank K L
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case some
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
m : K →₀ V
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
μ' : K
_hμ' : μ' ∈ m.support.erase μ
k : ℕ
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) (some k)
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) (some k)
hlk : ∀ (i : K), ↑(l i) ≤ some k
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) (some k)) ↑((f.genEigenspace μ) (some k))
this : iSupIndep fun x ↦ (f.genEigenspace x) (some k)
⊢ ↑l₀ ≤ some k

Tactic:
· exact Nat.cast_le.2 <| Finset.sup_le fun i _ ↦ Nat.cast_le.1 <| hlk i

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

Goal state before:
pp: K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
⊢ (aeval ((aeval (root p)) g)) f = 0

Tactic:
rw [← aeval_comp]

Goal state after:
K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
⊢ (aeval (root p)) (f.comp g) = 0
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
this : x ∈ H.normalizer
⊢ x = 0

Tactic:
LieSubalgebra.IsCartanSubalgebra.self_normalizing,

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
this : x ∈ H
⊢ x = 0
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ H
y : ↥H
k : ℕ
hk : lowerCentralSeries R (↥H) (↥H) k = ⊥
f : Module.End R ↥H := (toEnd R ↥H ↥H) y
g : Module.End R L := (toEnd R (↥H) L) y
hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f
⊢ ((g ^ k) ∘ₗ H.subtype) ⟨x, hx⟩ = 0

Tactic:
Module.End.commute_pow_left_of_commute hfg k

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ H
y : ↥H
k : ℕ
hk : lowerCentralSeries R (↥H) (↥H) k = ⊥
f : Module.End R ↥H := (toEnd R ↥H ↥H) y
g : Module.End R L := (toEnd R (↥H) L) y
hfg : g ∘ₗ H.subtype = H.subtype ∘ₗ f
⊢ (H.subtype ∘ₗ f ^ k) ⟨x, hx⟩ = 0
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : 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✝ : LieRing.IsNilpotent L
m : M
hm : ∀ (x x_1 : L), ∃ k, ((toEnd R L M) x_1 ^ k) ⁅x, m⁆ = 0
y : L
k : ℕ
hk : ((toEnd R L M) y ^ k) ⁅y, m⁆ = 0
⊢ ∃ k, ((toEnd R L M) y ^ k) m = 0

Tactic:
use k + 1

Goal state after:
case h
R : 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✝ : LieRing.IsNilpotent L
m : M
hm : ∀ (x x_1 : L), ∃ k, ((toEnd R L M) x_1 ^ k) ⁅x, m⁆ = 0
y : L
k : ℕ
hk : ((toEnd R L M) y ^ k) ⁅y, m⁆ = 0
⊢ ((toEnd R L M) y ^ (k + 1)) m = 0
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Tactic:
use k + 1

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ((toEnd R (↥H) L) ⟨y, hy⟩ ^ (k + 1)) x = 0