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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x y z : L
m n : M
⊢ { toFun := fun m ↦ ⁅0, m⁆, map_zero' := ⋯, map_add' := ⋯ } = 0

Tactic:
ext n; exact zero_lie n

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : n ≤ m
x : M
⊢ ∃ y, (⇑f)^[m] ((⇑f)^[n] y) = (⇑f)^[m] x

Tactic:
← iterate_add_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : n ≤ m
x : M
⊢ ∃ y, (⇑f)^[m + n] y = (⇑f)^[m] x
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
⊢ x ∈ ↑(sInf {N | s ⊆ ↑N}) ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

Tactic:
coe_sInf

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
⊢ x ∈ ⋂ s_1 ∈ {N | s ⊆ ↑N}, ↑s_1 ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
Module: Mathlib.Algebra.Lie.Ideal

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

Tactic:
LieSubmodule.coe_toSubmodule,

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : ↑(map f I) = ⇑f '' ↑I
⊢ ↑(map f I) = ↑(Submodule.map ↑f ↑I)
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(sInf (range fun i ↦ p i)) = ⋂ i, ↑(p i)

Tactic:
coe_sInf

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ⋂ s ∈ range fun i ↦ p i, ↑s = ⋂ i, ↑(p i)
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
s : Set M
x : M
⊢ x ∈ ↑(sInf {N | s ⊆ ↑N}) ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N

Tactic:
coe_sInf

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
s : Set M
x : M
⊢ x ∈ ⋂ s_1 ∈ {N | s ⊆ ↑N}, ↑s_1 ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N
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
s : Set M
⊢ lieSpan R L s ≤ ⊥ ↔ ∀ m ∈ s, m = 0

Tactic:
lieSpan_le,

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
s : Set M
⊢ s ⊆ ↑⊥ ↔ ∀ m ∈ s, m = 0
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian ↥I ↔ I ≤ LieModule.ker R L ↥I

Tactic:
by
  refine ⟨fun hI x hx ↦ LieHom.mem_ker.mpr ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩
  · ext y
    have := IsTrivial.trivial (⟨x, hx⟩ : I) y
    rw [LieIdeal.coe_bracket_of_module] at this
    simp [this]
  · simpa using LinearMap.congr_fun (h hx) ⟨y, hy⟩

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✝ : Nontrivial B
⊢ ¬IsUnit (minpoly A x)

Tactic:
have : Nontrivial A := (algebraMap A B).domain_nontrivial
  by_cases hx : IsIntegral A x
  · exact mt (monic hx).eq_one_of_isUnit (ne_one A x)
  · rw [eq_zero hx]
    exact not_isUnit_zero

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

Goal state before:
pp: case inr
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : (Polynomial.aeval x) p = 0
n : ℕ
hpn : p.degree = ↑n
ind : LinearIndependent A fun i ↦ x ^ ↑i
q : A[X]
lt : q.degree < p.degree
ne : ¬q = 0
hq : (Polynomial.aeval x) (∑ i ∈ Finset.range n, (monomial i) (q.coeff i)) = 0
i : ℕ
le : n ≤ i
⊢ q.coeff i = coeff 0 i

Tactic:
· exact coeff_eq_zero_of_degree_lt ((hpn ▸ lt).trans_le <| WithBot.coe_le_coe.mpr le)

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: F : Type u_3
E : Type u_4
A : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : CommRing A
inst✝³ : Algebra F E
inst✝² : Algebra E A
inst✝¹ : Algebra F A
inst✝ : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : minpoly E a ∈ lifts (algebraMap F E)
⊢ map (algebraMap F E) (minpoly F a) = minpoly E a

Tactic:
refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic ha.tower_top)
    ((algebraMap F E).injective.monic_map_iff.mp <| minpoly.monic ha)
    (minpoly.dvd E a (by simp)) ?_
  obtain ⟨g, hg, hgdeg, hgmon⟩ := lifts_and_natDegree_eq_and_monic h (minpoly.monic ha.tower_top)
  rw [natDegree_map, ← hgdeg]
  refine natDegree_le_of_dvd (minpoly.dvd F a ?_) hgmon.ne_zero
  rw [← aeval_map_algebraMap A, IsScalarTower.algebraMap_eq F E A, ← coe_mapRingHom,
    ← mapRingHom_comp, RingHom.comp_apply, coe_mapRingHom, coe_mapRingHom, hg,
    aeval_map_algebraMap, minpoly.aeval]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
hf₁ : f.ker = ⊥
hf₂ : N₂ ≤ f.range
| comap f ⁅I, N₂⁆

Tactic:
← map_comap_eq N₂ f hf₂

Goal state after:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
hf₁ : f.ker = ⊥
hf₂ : N₂ ≤ f.range
| comap f ⁅I, map f (comap f N₂)⁆
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
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit c

Tactic:
rw [eq_C_of_natDegree_le_zero h, ← Nat.eq_zero_of_le_zero h, ← leadingCoeff, hcm.leadingCoeff,
    C_1]

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit 1
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
r : R
⊢ 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) ⋯)
        ((Ideal.Quotient.mk (Ideal.map C I)) (C r))) =
    (Ideal.Quotient.mk (Ideal.map C I)) (C r)

Tactic:
rw [Ideal.Quotient.lift_mk, eval₂Hom_C, RingHom.comp_apply, eval₂_C, Ideal.Quotient.lift_mk,
      RingHom.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case refine_1.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

Tactic:
exact .inr ((squarefree_iff_no_irreducibles hr).mpr h)

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case mul
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
obtain ⟨y, n, hy, hyx, hy'⟩ := ih hz
    rcases n.eq_zero_or_pos with rfl | hn
    · exact ⟨p, 1, hp.squarefree, dvd_mul_right p z, by simp [isUnit_of_dvd_one (pow_zero y ▸ hy')]⟩
    by_cases hp' : p ∣ y
    · exact ⟨y, n + 1, hy, dvd_mul_of_dvd_right hyx _,
        mul_comm p z ▸ pow_succ y n ▸ mul_dvd_mul hy' hp'⟩
    · suffices Squarefree (p * y) from ⟨p * y, n, this,
        mul_dvd_mul_left p hyx, mul_pow p y n ▸ mul_dvd_mul (dvd_pow_self p hn.ne') hy'⟩
      exact squarefree_mul_iff.mpr ⟨hp.isRelPrime_iff_not_dvd.mpr hp', hp.squarefree, hy⟩

Goal state after:
Module: Mathlib.FieldTheory.Separable

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

Tactic:
by
  have := h.of_mul_left_left; rw [derivative_mul] at this
  exact IsCoprime.of_mul_right_left (IsCoprime.of_add_mul_left_right this)

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case prime.inr
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
g : K[X]
⊢ Irreducible ((expand K p) g) → False

Tactic:
have := Fact.mk hp

Goal state after:
case prime.inr
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
g : K[X]
this : Fact (Nat.Prime p)
⊢ Irreducible ((expand K p) g) → False
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:
by
    convert! this using 2
    ext x
    exact h x

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 : ι
⊢ ∀ (j : ι), v i = v j → i ≠ j → (MultilinearMap.mk' (fun v ↦ (e.toMatrix v).det) ⋯ ⋯).toFun v = 0

Tactic:
j

Goal state after:
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 j : ι
⊢ v i = v j → i ≠ j → (MultilinearMap.mk' (fun v ↦ (e.toMatrix v).det) ⋯ ⋯).toFun v = 0
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
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i k : ι
hik : k ≠ i
⊢ update v i (v k) k = update v i (v k) i

Tactic:
simp [hik]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

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

Tactic:
simp only [LinearMap.toMatrix_apply, sumQuot_repr_inr,
        Matrix.fromBlocks_apply₂₂, b, D]

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

Goal state before:
pp: case calc_3
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 ∈ R2N, ∑ j ∈ range (i + 1), ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (i - j)) =
    ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)

Tactic:
· rw [hR2N, sum_sigma']
      apply sum_bij (fun ⟨i, j⟩ _ ↦ (j, i - j))
      · simp only [mem_sigma, mem_range, mem_filter, mem_product, and_imp]
        lia
      · simp only [mem_sigma, mem_range, Prod.mk.injEq, and_imp]
        rintro ⟨x₁, y₁⟩ - h₁ ⟨x₂, y₂⟩ - h₂ h₃ h₄
        simp_all
        lia
      · simp only [mem_filter, mem_product, mem_range, mem_sigma, exists_prop, Sigma.exists,
          and_imp, Prod.forall, Prod.mk.injEq]
        exact fun x y _ _ _ ↦ ⟨x + y, x, by lia⟩
      · simp only [mem_sigma, mem_range, implies_true]

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

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeriesOfIdeal R (↥I) k ⊤ = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ ⁅comap I.incl (derivedSeriesOfIdeal R L k I), comap I.incl (derivedSeriesOfIdeal R L k I)⁆ =
    comap I.incl ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆

Tactic:
exact comap_bracket_incl_of_le I (derivedSeriesOfIdeal_le_self I k)
      (derivedSeriesOfIdeal_le_self I k)

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 y : A ⊗[R] L
z : A ⊗[R] M
⊢ ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆

Tactic:
simp only [bracket_def]
  refine x.induction_on ?_ ?_ ?_
  · simp only [map_zero, add_zero, LinearMap.zero_apply]
  · intro a₁ l₁
    refine y.induction_on ?_ ?_ ?_
    · simp only [map_zero, add_zero, LinearMap.zero_apply]
    · intro a₂ l₂
      refine z.induction_on ?_ ?_ ?_
      · simp only [map_zero, add_zero]
      · intro a₃ l₃; simp only [bracket'_tmul]
        rw [mul_left_comm a₂ a₁ a₃, mul_assoc, leibniz_lie, TensorProduct.tmul_add]
      · grind
    · grind [LinearMap.add_apply]
  · grind [LinearMap.add_apply]

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
⊢ lowerCentralSeriesLast R L M ≤ maxTrivSubmodule R L M

Tactic:
rw [lowerCentralSeriesLast]

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
⊢ (match nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    maxTrivSubmodule R L M
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✝ : IsNilpotent L M
h : ¬IsTrivial L M
⊢ lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1

Tactic:
rw [lowerCentralSeriesLast]

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✝ : IsNilpotent L M
h : ¬IsTrivial L M
⊢ (match nilpotencyLength L M with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝² : Monoid M
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction M F
m : M
p✝ p q : Polynomial ↥(subfield M F)
ihp : m • p = p
ihq : m • q = q
⊢ m • (p + q) = p + q

Tactic:
by rw [smul_add, ihp, ihq]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
q : Q
hq : (MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F) q = AlgEquiv.ofRingEquiv ⋯
⊢ ∃ a, (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) a = f

Tactic:
revert hq

Goal state after:
G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
q : Q
⊢ (MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F) q = AlgEquiv.ofRingEquiv ⋯ →
    ∃ a, (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) a = f
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 F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField K L ((mapAlg F K) f)
⊢ ((mapAlg F L) f).Splits

Tactic:
by
  rw [mapAlg_comp K L f, mapAlg_eq_map]
  apply IsSplittingField.splits

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)
⊢ Algebra.adjoin F ((f * g).rootSet L) = ⊤

Tactic:
rw [rootSet, aroots_mul (mul_ne_zero hf hg),
      Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin,
      aroots_def, aroots_def, IsScalarTower.algebraMap_eq F K L, ← map_map, (splits K f).roots_map,
      Multiset.toFinset_map, Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet,
      Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet,
      Subalgebra.restrictScalars_top]

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
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ ↔ ∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb

Tactic:
by
  simp_rw [AlgHom.ext_iff]; rfl

Goal state after:
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
S : Set E
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E1 E2 : IntermediateField K L
inst✝¹ : FiniteDimensional K ↥E1
inst✝ : FiniteDimensional K ↥E2
⊢ FiniteDimensional K ↥(E1 ⊔ E2)

Tactic:
let g := Algebra.TensorProduct.productMap E1.val E2.val

Goal state after:
F : Type u_1
inst✝⁷ : Field F
E : Type u_2
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E1 E2 : IntermediateField K L
inst✝¹ : FiniteDimensional K ↥E1
inst✝ : FiniteDimensional K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
⊢ FiniteDimensional K ↥(E1 ⊔ E2)
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝²⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝²⁵ : Field K
inst✝²⁴ : Field J
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Field L
inst✝²⁰ : Field M
inst✝¹⁹ : Algebra R M
inst✝¹⁸ : IsTorsionFree R M
inst✝¹⁷ : IsAlgClosure R M
inst✝¹⁶ : Algebra K M
inst✝¹⁵ : IsAlgClosure K M
inst✝¹⁴ : Algebra S L
inst✝¹³ : IsTorsionFree S L
inst✝¹² : IsAlgClosure S L
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R L
inst✝⁹ : IsScalarTower R S L
inst✝⁸ : Algebra K J
inst✝⁷ : Algebra J L
inst✝⁶ : IsAlgClosure J L
inst✝⁵ : Algebra K L
inst✝⁴ : IsScalarTower K J L
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : Algebra.IsAlgebraic R L
this : IsTorsionFree R L
⊢ L ≃ₐ[R] M

Tactic:
have : IsAlgClosure R L :=
    { isAlgClosed := IsAlgClosure.isAlgClosed S
      isAlgebraic := ‹_› }

Goal state after:
k : Type u
inst✝²⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝²⁵ : Field K
inst✝²⁴ : Field J
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Field L
inst✝²⁰ : Field M
inst✝¹⁹ : Algebra R M
inst✝¹⁸ : IsTorsionFree R M
inst✝¹⁷ : IsAlgClosure R M
inst✝¹⁶ : Algebra K M
inst✝¹⁵ : IsAlgClosure K M
inst✝¹⁴ : Algebra S L
inst✝¹³ : IsTorsionFree S L
inst✝¹² : IsAlgClosure S L
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R L
inst✝⁹ : IsScalarTower R S L
inst✝⁸ : Algebra K J
inst✝⁷ : Algebra J L
inst✝⁶ : IsAlgClosure J L
inst✝⁵ : Algebra K L
inst✝⁴ : IsScalarTower K J L
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : Algebra.IsAlgebraic R L
this✝ : IsTorsionFree R L
this : IsAlgClosure R L
⊢ L ≃ₐ[R] M