mathlib-initiative/mathlib-tactics huggingface dataset:
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
m : M
⊢ ∀ (s : Set (LieSubmodule R L M)),
    s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x

Tactic:
intro s

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
m : M
s : Set (LieSubmodule R L M)
⊢ s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
⊢ (Polynomial.aeval x) p = 0 ↔ p ∈ A[X] ∙ minpoly A x

Tactic:
← minpoly.dvd_iff,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
⊢ minpoly A x ∣ p ↔ p ∈ A[X] ∙ minpoly A 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
h : (minpoly A x).natDegree < 2
⊢ (minpoly A x).natDegree = 1

Tactic:
by linarith only [minpoly.natDegree_pos int, h]

Goal state after:
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✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
⊢ f = 1 ∨ g = 1

Tactic:
rw [← hf.isUnit_iff, ← hg.isUnit_iff]

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
⊢ IsUnit f ∨ IsUnit g
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁹ : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : Ring S
inst✝⁵ : Ring T
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
inst✝¹ : Algebra A T
inst✝ : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp : (algebraMap A T).comp ↑f = (↑g).comp (algebraMap R S)
x : S
⊢ Irreducible ((mapEquiv f) (minpoly R x))

Tactic:
MulEquiv.irreducible_iff

Goal state after:
case refine_1
A : Type u_1
inst✝⁹ : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : Ring S
inst✝⁵ : Ring T
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
inst✝¹ : Algebra A T
inst✝ : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp : (algebraMap A T).comp ↑f = (↑g).comp (algebraMap R S)
x : S
⊢ Irreducible (minpoly R 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₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
rw [← inf_eq_right] at h₁ h₂

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I ⊓ I₁ = I₁
h₂ : I ⊓ I₂ = I₂
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
⊢ f = g

Tactic:
suffices (f : E →ₗ[F] K) = (g : E →ₗ[F] K) by rwa [DFunLike.ext'_iff] at this ⊢

Goal state after:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
⊢ ↑f = ↑g
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
H : q.natDegree < orderOf σ
hs : ∑ x, q.coeff ↑x • (σ ^ ↑x).toLinearMap = 0
⊢ False

Tactic:
apply hq.ne_zero

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
H : q.natDegree < orderOf σ
hs : ∑ x, q.coeff ↑x • (σ ^ ↑x).toLinearMap = 0
⊢ q = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x✝ x : R
⊢ (aeval x✝) ((fun a ↦ C a) x) = x

Tactic:
exact eval_C

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
⊢ ↑(quotientSpanXSubCAlgEquiv y) ((Ideal.Quotient.mkₐ R (Ideal.span {X - C y})) (C x)) = x

Tactic:
exact eval_C

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ Function.RightInverse
    (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) fun i ↦
      (Ideal.Quotient.mk (Ideal.map C I)) (X i))
    ⇑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)

Tactic:
intro f
  apply induction_on f
  · intro r
    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
    simp
  · intro p q hp hq
    simp only [map_add, MvPolynomial.eval₂_add]
      at hp hq ⊢
    rw [hp, hq]
  · intro p i hp
    simp only [hp, coe_eval₂Hom, Ideal.Quotient.lift_mk, eval₂_mul, map_mul, eval₂_X]

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
⊢ root (X ^ n - C a) = 0 ↔ a = 0

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
hn : 0 < n
⊢ root (X ^ n - C a) = 0 ↔ a = 0
Module: Mathlib.FieldTheory.Separable

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

Tactic:
by
  rw [separable_def, derivative_mul]
  exact
    ((hf.mul_right h).add_mul_left_right _).mul_left ((h.symm.mul_right hg).mul_add_right_right _)

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: 𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
⊢ ∀ (s : Finset M) (b : Basis (↥s) 𝕜 M), ((toMatrix b b) f).det = 1

Tactic:
intro s

Goal state after:
𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
⊢ ∀ (b : Basis (↥s) 𝕜 M), ((toMatrix b b) f).det = 1
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ (frobeniusEquiv R p ^ n).symm = (frobeniusEquiv R p).symm ^ n

Tactic:
exact (inv_pow _ _).symm

Goal state after:
Module: Mathlib.FieldTheory.Perfect

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

Tactic:
by
  simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul,
    Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, map_id']

Goal state after:
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ p = annIdealGenerator 𝕜 a

Tactic:
apply eq_of_monic_of_associated p_monic _ p_gen

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ (annIdealGenerator 𝕜 a).Monic
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
a : S
x : R
⊢ a • (of f) x = (of f) (a • x)

Tactic:
rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]

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
v : ι → M
i : ι
x y : M
⊢ (e.toMatrix (update v i (x + y))).det = (e.toMatrix (update v i x)).det + (e.toMatrix (update v i y)).det

Tactic:
by
        simp only [e.toMatrix_update, map_add, Finsupp.coe_add, det_updateCol_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit ((LinearMap.toMatrix e e) ((e.constr ℕ) v)).det
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤

Tactic:
set v' := Basis.map e (LinearEquiv.ofIsUnitDet h) with v'_def

Goal state after:
case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit ((LinearMap.toMatrix e e) ((e.constr ℕ) v)).det
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case pos
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f = 0
⊢ finrank K (K[X] ⧸ span {0}) = natDegree 0

Tactic:
natDegree_zero,

Goal state after:
case pos
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f = 0
⊢ finrank K (K[X] ⧸ span {0}) = 0
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: 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))
n : ℕ
⊢ (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    have ⟨d, hd⟩ := binomExpansion (P.map (algebraMap R S)) (P.newtonMap^[n] x)
      (-Ring.inverse (aeval (P.newtonMap^[n] x) <| derivative P) * aeval (P.newtonMap^[n] x) P)
    rw [eval_map_algebraMap, eval_map_algebraMap] at hd
    rw [iterate_succ', comp_apply, newtonMap_apply, sub_eq_add_neg, neg_mul_eq_neg_mul, hd]
    refine dvd_add ?_ (dvd_mul_of_dvd_right ?_ _)
    · convert! dvd_zero _
      have : IsUnit (aeval (P.newtonMap^[n] x) <| derivative P) :=
        isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub h' <|
        isNilpotent_iterate_newtonMap_sub_of_isNilpotent h n
      rw [derivative_map, eval_map_algebraMap, ← mul_assoc, mul_neg, Ring.mul_inverse_cancel _ this,
        neg_mul, one_mul, add_neg_cancel]
    · rw [neg_mul, even_two.neg_pow, mul_pow, pow_succ, pow_mul]
      exact dvd_mul_of_dvd_right (pow_dvd_pow_of_dvd ih 2) _

Goal state after:
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 ^ m ∣ (x + y) ^ p

Tactic:
rw [h_comm.add_pow']
  refine Finset.dvd_sum fun ⟨i, j⟩ hij ↦ ?_
  replace hij : i + j = p := by simpa using hij
  apply dvd_nsmul_of_dvd
  rcases le_or_gt m i with (hi : m ≤ i) | (hi : i + 1 ≤ m)
  · exact dvd_mul_of_dvd_left (pow_dvd_pow x hi) _
  · simp [pow_eq_zero_of_le (by lia : n ≤ j) hy]

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ x ^ m ∣ (y - x + x) ^ p

Tactic:
apply (h_comm.symm.sub_left rfl).pow_dvd_add_pow_of_pow_eq_zero_left hp _

Goal state after:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ (y - x) ^ n = 0
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
n : ℕ
⊢ derivedSeries R L (n + 1) = ⊤ ↔ derivedSeries R L 1 = ⊤

Tactic:
simp only [derivedSeries_def]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
n : ℕ
⊢ derivedSeriesOfIdeal R L (n + 1) ⊤ = ⊤ ↔ derivedSeriesOfIdeal R L 1 ⊤ = ⊤
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
⊢ let I := derivedSeriesOfIdeal R₂ L k ⊤;
  let S := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x};
  ↑(Submodule.span R₁ S) ⊆ ↑(Submodule.span R₂ S)

Tactic:
intro I

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
⊢ let S := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x};
  ↑(Submodule.span R₁ S) ⊆ ↑(Submodule.span R₂ S)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
⊢ let I := lowerCentralSeries R₂ L M k;
  let S := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x};
  ↑(Submodule.span R₁ S) ⊆ ↑(Submodule.span R₂ S)

Tactic:
intro I

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
⊢ let S := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x};
  ↑(Submodule.span R₁ S) ⊆ ↑(Submodule.span R₂ S)
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅Quotient.mk'' x, t • Quotient.mk'' y⁆ = t • ⁅Quotient.mk'' x, Quotient.mk'' y⁆

Tactic:
first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_smul (R := R) (M := L)]

Goal state after:
case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • Quotient.mk'' y⁆ = t • ⁅mk x, Quotient.mk'' y⁆
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • Quotient.mk'' y⁆ = t • ⁅mk x, Quotient.mk'' y⁆

Tactic:
first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_smul (R := R) (M := L)]

Goal state after:
case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • mk y⁆ = t • ⁅mk x, mk y⁆
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • mk y⁆ = t • ⁅mk x, mk y⁆

Tactic:
first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_smul (R := R) (M := L)]

Goal state after:
case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • mk y⁆ = t • mk ⁅x, y⁆
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • mk y⁆ = t • mk ⁅x, y⁆

Tactic:
first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_smul (R := R) (M := L)]

Goal state after:
case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, Submodule.Quotient.mk (t • y)⁆ = t • mk ⁅x, y⁆
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, Submodule.Quotient.mk (t • y)⁆ = t • mk ⁅x, y⁆

Tactic:
first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_smul (R := R) (M := L)]

Goal state after:
case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ mk ⁅x, t • y⁆ = t • mk ⁅x, y⁆
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ mk ⁅x, t • y⁆ = t • mk ⁅x, y⁆

Tactic:
first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_smul (R := R) (M := L)]

Goal state after:
case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ mk ⁅x, t • y⁆ = Submodule.Quotient.mk (t • ⁅x, y⁆)
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ mk ⁅x, t • y⁆ = Submodule.Quotient.mk (t • ⁅x, y⁆)

Tactic:
first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_smul (R := R) (M := L)]

Goal state after:
case h
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
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ mk ⁅x, t • y⁆ = Submodule.Quotient.mk (t • ⁅x, y⁆)
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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
⊢ map (mk' N) N' = ⊥ ↔ N' ≤ N

Tactic:
by
  rw [← LieModuleHom.le_ker_iff_map, mk'_ker]

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

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₁ : I ≤ center R L
h₂ : ∃ k, lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥
⊢ ∃ k, lowerCentralSeries R L (L ⧸ I) k = ⊥

Tactic:
peel h₂ with k hk

Goal state after:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : ∃ k, lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥
k : ℕ
hk : lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥
⊢ lowerCentralSeries R L (L ⧸ I) k = ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

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'
k : ℕ
f : L →ₗ⁅R⁆ L'
⊢ map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k

Tactic:
induction k with
  | zero => simp only [LieModule.lowerCentralSeries_zero, le_top]
  | succ k ih =>
    simp only [LieModule.lowerCentralSeries_succ]
    exact le_trans (LieIdeal.map_bracket_le f) (LieSubmodule.mono_lie le_top ih)

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
r : K
g : (map (algebraMap K L) (minpoly K x)).Splits
⊢ (map (algebraMap K L) (minpoly K (x - (algebraMap K L) r))).Splits

Tactic:
by
  simpa only [sub_eq_add_neg, map_neg] using minpoly_add_algebraMap_splits (-r) g

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 T : Set E
⊢ adjoin F (S ∪ T) = adjoin F (T ∪ S)

Tactic:
Set.union_comm

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ adjoin F (T ∪ S) = adjoin F (T ∪ S)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case pos
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : FiniteDimensional K ↥E1
this : finrank K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤ finrank K ↥E1.toSubalgebra * finrank K ↥E2.toSubalgebra
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2

Tactic:
change _ ≤ finrank K E1 * finrank K E2 at this

Goal state after:
case pos
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : FiniteDimensional K ↥E1
this : finrank K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤ finrank K ↥E1 * finrank K ↥E2
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2
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
x : E
⊢ ∀ (s : Set (IntermediateField F E)),
    s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → x ∈ ⨆ a, ↑a → ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1

Tactic:
intro s

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
s : Set (IntermediateField F E)
⊢ s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → x ∈ ⨆ a, ↑a → ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1