mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case refine_1
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 : (x : M) → x ∈ ⨆ i, N i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx✝ : x✝ ∈ ⨆ i, N i
i : ι
x : M
hx : x ∈ N i
⊢ ∃ (hx : x ∈ ⨆ i, N i), motive x hx

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

pp: case refine_3
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 : (x : M) → x ∈ ⨆ i, N i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, N i
x y : M
⊢ (∃ (hx : x ∈ ⨆ i, N i), motive x hx) →
    (∃ (hx : y ∈ ⨆ i, N i), motive y hx) → ∃ (hx : x + y ∈ ⨆ i, N i), motive (x + y) hx

Tactic:
· exact ⟨_, mem _ _ hx⟩

Goal state after:
case refine_2
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 : (x : M) → x ∈ ⨆ i, N i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : x ∈ ⨆ i, N i
⊢ ∃ (hx : 0 ∈ ⨆ i, N i), motive 0 hx

case refine_3
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 : (x : M) → x ∈ ⨆ i, N i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, N i
x y : M
⊢ (∃ (hx : x ∈ ⨆ i, N i), motive x hx) →
    (∃ (hx : y ∈ ⨆ i, N i), motive y hx) → ∃ (hx : x + y ∈ ⨆ i, N i), motive (x + y) hx
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
x : L
hx : x ∈ LieAlgebra.center R L
y : L
⊢ Commute ((toEnd R L M) y) ((toEnd R L M) x)

Tactic:
commute_iff_lie_eq,

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
x : L
hx : x ∈ LieAlgebra.center R L
y : L
⊢ ⁅(toEnd R L M) y, (toEnd R L M) x⁆ = 0
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 : LieSubmodule R L M
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆

Tactic:
have h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆ := by
    rw [sup_le_iff]; constructor <;>
    apply mono_lie_left <;> [exact le_sup_left; exact le_sup_right]
  suffices ⁅I ⊔ J, N⁆ ≤ ⁅I, N⁆ ⊔ ⁅J, N⁆ by exact le_antisymm this h
  rw [lieIdeal_oper_eq_span, lieSpan_le]
  rintro m ⟨⟨x, hx⟩, n, h⟩
  simp only [SetLike.mem_coe]
  rw [LieSubmodule.mem_sup] at hx ⊢
  rcases hx with ⟨x₁, hx₁, x₂, hx₂, hx'⟩
  use ⁅((⟨x₁, hx₁⟩ : I) : L), (n : N)⁆; constructor; · apply lie_coe_mem_lie
  use ⁅((⟨x₂, hx₂⟩ : J) : L), (n : N)⁆; constructor; · apply lie_coe_mem_lie
  simp [← h, ← hx']

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
h : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
root : (aeval h.gen) p = 0
⊢ ↑h.dim ≤ p.degree

Tactic:
by
  rw [degree_eq_natDegree ne_zero]
  exact WithBot.coe_le_coe.2 (h.dim_le_natDegree_of_root ne_zero root)

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j ↦ if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

Tactic:
Algebra.leftMulMatrix_apply,

Goal state after:
case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ (LinearMap.toMatrix pb.basis pb.basis) ((Algebra.lmul A S) pb.gen) =
    Matrix.of fun i j ↦ if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
⊢ pb.equivOfRoot (pb.map e) h₁ h₂ = e

Tactic:
ext x
  obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
  simp [aeval_algEquiv]

Goal state after:
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
inst✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ LinearMap.det f = 1

Tactic:
rw [← f.det_toMatrix b]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ ((toMatrix b b) f).det = 1
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : ℕ
hp : ExpChar K p
y : K
⊢ ∃ a, (frobenius K p) a = y

Tactic:
rcases hp with _ | hp

Goal state after:
case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : PerfectField K
y : K
inst✝ : CharZero K
⊢ ∃ a, (frobenius K 1) a = y

case prime
K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : ℕ
y : K
hp : Nat.Prime p
hchar✝ : CharP K p
⊢ ∃ a, (frobenius K p) a = y
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : PerfectRing R p
inst✝ : DecidableEq R
⊢ (Multiset.map (⇑(frobenius R p)) ((expand R p) f).roots).toFinset = f.roots.toFinset

Tactic:
roots_expand_map_frobenius,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : PerfectRing R p
inst✝ : DecidableEq R
⊢ (p • f.roots).toFinset = f.roots.toFinset
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : (map (algebraMap F K) f).Splits
⊢ (f.aroots K).Nodup ↔ f.Separable

Tactic:
rw [nodup_roots_iff_of_splits (map_ne_zero hf) h, separable_map]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr
F : Type u_1
K : Type u_3
inst✝² : CommRing F
inst✝¹ : Ring K
inst✝ : Algebra F K
x : K
h : IsSeparable F x
h✝ : Nontrivial F
⊢ IsIntegral F x

Tactic:
· exact of_not_not (h.ne_zero <| minpoly.eq_zero ·)

Goal state after:
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
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit ((toMatrix v v') f).det
x : M
⊢ ((toLin v' v) ((toMatrix v v') f)⁻¹) (f x) = ((toLin v v) (((toMatrix v v') f)⁻¹ * (toMatrix v v') f)) x

Tactic:
by
        rw [toLin_mul v v' v, toLin_toMatrix, LinearMap.comp_apply]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
h : IsNilpotent ((LieAlgebra.ad R L) ↑x)
⊢ IsNilpotent ((LieAlgebra.ad R ↥K) x)

Tactic:
by
  obtain ⟨n, hn⟩ := h
  use n
  exact Module.End.submodule_pow_eq_zero_of_pow_eq_zero (K.ad_comp_incl_eq x) hn

Goal state after:
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
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
this : Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
⊢ Associated (LinearMap.det f) (LinearMap.det f')

Tactic:
convert! this using 2

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
this : Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
⊢ f = f' ∘ₗ ↑e
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S →ₐ[R] T
p : S[X]
q : T[X]
h : q ∣ Polynomial.map (↑f) p
r : R
⊢ (↑↑(map (↑f) p q h)).toFun ((algebraMap R (AdjoinRoot p)) r) = (algebraMap R (AdjoinRoot q)) r

Tactic:
by simp [map, AdjoinRoot.algebraMap_eq']

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
this : (↑i !)⁻¹ * ↑(i.choose j) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹
⊢ (↑i !)⁻¹ • (a ^ j * b ^ (i - j) * ↑(i.choose j)) = ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (i - j))

Tactic:
rw [← Nat.cast_commute (i.choose j), ← this, ← mul_smul_comm, ← nsmul_eq_mul,
          mul_smul, ← smul_assoc, smul_comm, smul_assoc]
        norm_cast

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x : L
m : M
hm : m ∈ {m | ∀ (x : L), ⁅x, m⁆ ∈ N}
y : L
⊢ ⁅y, ⁅x, m⁆⁆ ∈ N

Tactic:
rw [leibniz_lie]; exact N.add_mem' (hm ⁅y, x⁆) (N.lie_mem (hm y))

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

Goal state before:
pp: case refine_3.refine_2
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
a₁ : A
l₁ : L
⊢ ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) z₂ + ((bracket' R A L L) z₂) (a₁ ⊗ₜ[R] l₁) = 0

Tactic:
refine z₂.induction_on ?_ ?_ ?_

Goal state after:
case refine_3.refine_2.refine_1
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
a₁ : A
l₁ : L
⊢ ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) 0 + ((bracket' R A L L) 0) (a₁ ⊗ₜ[R] l₁) = 0

case refine_3.refine_2.refine_2
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
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L), ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y) + ((bracket' R A L L) (x ⊗ₜ[R] y)) (a₁ ⊗ₜ[R] l₁) = 0

case refine_3.refine_2.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
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x + ((bracket' R A L L) x) (a₁ ⊗ₜ[R] l₁) = 0 →
      ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y + ((bracket' R A L L) y) (a₁ ⊗ₜ[R] l₁) = 0 →
        ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y) + ((bracket' R A L L) (x + y)) (a₁ ⊗ₜ[R] l₁) = 0
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_3.refine_2.refine_2
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
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂) + ((bracket' R A L L) (a₂ ⊗ₜ[R] l₂)) (a₁ ⊗ₜ[R] l₁) = 0

Tactic:
simp only [← lie_skew l₂ l₁, mul_comm a₁ a₂, TensorProduct.tmul_neg, bracket'_tmul,
          add_neg_cancel]

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
inst✝ : LieModule R L M
⊢ map N.incl (lowerCentralSeries R L (↥N) k) = lcs k N

Tactic:
lowerCentralSeries_eq_lcs_comap,

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
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ map N.incl (comap N.incl (lcs k N)) = lcs k N
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
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
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ ⁅x, ⁅y, (⇑((toEnd R L M) x) ∘ ⇑((toEnd R L M) y))^[k] m⁆⁆ ∈ ⁅⊤, ⁅⊤, lowerCentralSeries R L M (2 * k)⁆⁆

Tactic:
refine LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ?_

Goal state after:
case succ
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
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ ⁅y, (⇑((toEnd R L M) x) ∘ ⇑((toEnd R L M) y))^[k] m⁆ ∈ ⁅⊤, lowerCentralSeries R L M (2 * k)⁆
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case H.H
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z✝¹ z✝ : L
⊢ ↑((↑f).quotKerEquivRange ⁅Submodule.Quotient.mk z✝¹, Submodule.Quotient.mk z✝⁆) =
    ↑⁅(↑f).quotKerEquivRange (Submodule.Quotient.mk z✝¹), (↑f).quotKerEquivRange (Submodule.Quotient.mk z✝)⁆

Tactic:
LieSubalgebra.coe_bracket f.range

Goal state after:
case H.H
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z✝¹ z✝ : L
⊢ ↑((↑f).quotKerEquivRange ⁅Submodule.Quotient.mk z✝¹, Submodule.Quotient.mk z✝⁆) =
    ⁅↑((↑f).quotKerEquivRange (Submodule.Quotient.mk z✝¹)), ↑((↑f).quotKerEquivRange (Submodule.Quotient.mk z✝))⁆
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
⊢ i ∈ s → l i ∈ subfield G F

Tactic:
his

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
⊢ l i ∈ subfield G F
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
⊢ f = 1 ∨ g = 1

Tactic:
by
  have hf2 : f ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_right _ _
  have hg2 : g ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_left _ _
  have := eval₂ G F x
  rw [← hfg, Polynomial.eval₂_mul, mul_eq_zero] at this
  rcases this with this | this
  · right
    have hf3 : f = minpoly G F x :=
      Polynomial.eq_of_monic_of_associated hf (monic G F x)
        (associated_of_dvd_dvd hf2 <| @of_eval₂ G _ F _ _ _ x f this)
    rwa [← mul_one (minpoly G F x), hf3, mul_right_inj' (monic G F x).ne_zero] at hfg
  · left
    have hg3 : g = minpoly G F x :=
      Polynomial.eq_of_monic_of_associated hg (monic G F x)
        (associated_of_dvd_dvd hg2 <| @of_eval₂ G _ F _ _ _ x g this)
    rwa [← one_mul (minpoly G F x), hg3, mul_left_inj' (monic G F x).ne_zero] at hfg

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
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
x✝¹ : L
x✝ : x✝¹ ∈ Set.range ⇑(algebraMap F L)
x : F
hx : (algebraMap F L) x = x✝¹
⊢ g.toRingHom ((algebraMap F A) x) = x✝¹

Tactic:
simp [← hx]

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin
        ↥(Subalgebra.map (IsScalarTower.toAlgHom F K L)
            (Algebra.adjoin F ↑(Polynomial.map (algebraMap F K) f).roots.toFinset))
        ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).roots.toFinset) =
    ⊤

Tactic:
← rootSet,

Goal state after:
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin ↥(Subalgebra.map (IsScalarTower.toAlgHom F K L) (Algebra.adjoin F (f.rootSet K)))
        ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).roots.toFinset) =
    ⊤
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin K ↑(Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) g)).roots.toFinset) =
    ⊤

Tactic:
← rootSet,

Goal state after:
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F (Algebra.adjoin K ((Polynomial.map (algebraMap F K) g).rootSet L)) = ⊤
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 (↥⊥ →ₐ[F] L)

Tactic:
exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩

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

Goal state before:
pp: 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 ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)

Tactic:
refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
    · rw [coe_empty, Algebra.adjoin_empty]
      exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
    rw [forall_mem_insert] at H
    rcases H with ⟨⟨H1, H2⟩, H3⟩
    obtain ⟨f⟩ := ih H3
    choose H3 _ using H3
    rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
    set Ks := Algebra.adjoin F (s : Set K)
    have : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
    let := fieldOfFiniteDimensional F Ks
    let := (f : Ks →+* L).toAlgebra
    have H5 : IsIntegral Ks a := H1.tower_top
    have H6 : ((minpoly Ks a).map (algebraMap Ks L)).Splits := by
      refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
      rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']
      exact minpoly.dvd_map_of_isScalarTower F Ks a
    obtain ⟨y, hy⟩ := H6.exists_eval_eq_zero (by simp [(minpoly.degree_pos H5).ne'])
    rw [eval_map] at hy
    exact ⟨Subalgebra.ofRestrictScalars F _ <| Algebra.adjoin.liftSingleton Ks a y hy⟩

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

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
x : L
inst✝ : Algebra R L
int : IsIntegral R x
h : (Polynomial.map (algebraMap R K) (minpoly R x)).Splits
f : K →ₐ[R] L
⊢ x ∈ ⇑f '' (minpoly R x).rootSet K

Tactic:
by
    rw [h.image_rootSet, mem_rootSet']
    exact ⟨((minpoly.monic int).map _).ne_zero, minpoly.aeval R x⟩

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

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
E : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field E
inst✝³ : Algebra K L
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : adjoin K ↑s = restrictScalars K E'
⊢ adjoin L ↑s ≤ E'

Tactic:
rw [adjoin_le_iff]
    exact (subset_adjoin K _).trans_eq congr(($hs : Set E))

Goal state after: