mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι
⊢ (e.det v • (Basis.mk hli hsp).coord i) ((Basis.mk hli hsp) k) = ((↑e.det).toLinearMap v i) ((Basis.mk hli hsp) k)

Tactic:
rcases eq_or_ne k i with (rfl | hik) <;>
    simp only [smul_eq_mul, coe_mk, LinearMap.smul_apply,
      MultilinearMap.toLinearMap_apply]

Goal state after:
case inl
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)
k : ι
⊢ e.det v * ((Basis.mk hli hsp).coord k) (v k) = ↑e.det (update v k (v k))

case inr
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
⊢ e.det v * ((Basis.mk hli hsp).coord i) (v k) = ↑e.det (update v i (v k))
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
this : ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p
⊢ (f - (algebraMap R (End R M)) μ).IsSemisimple ↔ f.IsSemisimple

Tactic:
simp [mem_invtSubmodule, isSemisimple_iff, this]

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁴ : Module.Finite K R
this✝³ : Module.Finite R S
this✝² : Module.Finite K S
this✝¹ : IsArtinianRing R
this✝ : IsReduced R
this : IsReduced S
a✝ : R
p✝ p q : K[X]
hp :
  Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f}))) p))
    g
hq :
  Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f}))) q))
    g
⊢ Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f}))) (p + q)))
    g

Tactic:
by simpa [R] using! hp.add_left hq

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

Tactic:
sum_sigma'

Goal state after:
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)
⊢ ∑ x ∈ (range (2 * N + 1)).sigma fun i ↦ range (i + 1),
      ((↑x.snd !)⁻¹ * (↑(x.fst - x.snd)!)⁻¹) • (a ^ x.snd * b ^ (x.fst - x.snd)) =
    ∑ ij ∈ range (2 * N + 1) ×ˢ range (2 * N + 1) with ij.1 + ij.2 ≤ 2 * N,
      ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : L
⊢ ((-inner R L L).toFun ⁅x, y⁆) z = ⁅(-inner R L L).toFun x, (-inner R L L).toFun y⁆ z

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.neg_apply, coe_neg,
        Pi.neg_apply, inner_apply_apply, commutator_apply]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : L
⊢ -⁅z, ⁅x, y⁆⁆ = -⁅-⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_2
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)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
restrict :
  ∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
⊢ ∑ i ∈ RN, ∑ j ∈ RN, ((↑i !)⁻¹ * (↑j !)⁻¹) • (a ^ i * b ^ j) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)

Tactic:
sum_sigma'

Goal state after:
case calc_2
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)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
restrict :
  ∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
⊢ ∑ x ∈ RN.sigma fun i ↦ RN, ((↑x.fst !)⁻¹ * (↑x.snd !)⁻¹) • (a ^ x.fst * b ^ x.snd) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x m : L
⊢ (↑(toEnd R L M)).toFun ⁅x, m⁆ = ⁅x, (↑(toEnd R L M)).toFun m⁆

Tactic:
by ext n; simp [LieRing.of_associative_ring_bracket]

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
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
k : ℕ
⊢ derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤ = LieSubmodule.baseChange A (D k ⊤)

Tactic:
← derivedSeriesOfIdeal_baseChange,

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
k : ℕ
⊢ derivedSeriesOfIdeal A (A ⊗[R] L) k ⊤ = derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A ⊤)
Module: Mathlib.Algebra.Lie.Solvable

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'
f : L' →ₗ⁅R⁆ L
hL' : IsSolvable L'
h : Surjective ⇑f
⊢ IsSolvable L

Tactic:
by
  rw [isSolvable_iff R] at hL' ⊢
  apply hL'.imp
  intro k hk
  rw [← LieIdeal.derivedSeries_map_eq k h, hk]
  simp only [LieIdeal.map_eq_bot_iff, bot_le]

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
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
⊢ k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s

Tactic:
h₁₂

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
⊢ k₁ ∈ s → k₂ ∈ s
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
N : LieSubmodule R L M
⊢ Submodule.span R {x | ∃ x_1, ∃ n ∈ N, ⁅x_1, n⁆ = x} =
    Submodule.span R ((fun a ↦ ⁅x, a⁆) '' ↑↑N ∪ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x})

Tactic:
refine le_antisymm (Submodule.span_le.mpr ?_) (Submodule.span_mono fun z hz => ?_)

Goal state after:
case refine_1
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
N : LieSubmodule R L M
⊢ {x | ∃ x_1, ∃ n ∈ N, ⁅x_1, n⁆ = x} ⊆
    ↑(Submodule.span R ((fun a ↦ ⁅x, a⁆) '' ↑↑N ∪ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}))

case refine_2
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
N : LieSubmodule R L M
z : M
hz : z ∈ (fun a ↦ ⁅x, a⁆) '' ↑↑N ∪ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}
⊢ z ∈ {x | ∃ x_1, ∃ n ∈ N, ⁅x_1, n⁆ = x}
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
this✝¹ : LieRingModule L M := LieRingModule.compLieHom M f
this✝ : LieModule R L M := compLieHom M f
hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
surj_id : Surjective ⇑LinearMap.id
this : LieModule.IsNilpotent L M
⊢ LieModule.IsNilpotent L₂ M

Tactic:
apply hf.lieModuleIsNilpotent _ surj_id

Goal state after:
R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
this✝¹ : LieRingModule L M := ⋯
this✝ : LieModule R L M := ⋯
hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
surj_id : Surjective ⇑LinearMap.id
this : LieModule.IsNilpotent L M
⊢ ∀ (x : L) (m : M), ⁅f x, LinearMap.id m⁆ = LinearMap.id ⁅x, m⁆
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✝⁷ : 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
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
⊢ {x | ∃ x_1 ∈ baseChange A I, ∃ n ∈ baseChange A N, ⁅x_1, n⁆ = x} ⊆ ↑(Submodule.span A s)

Tactic:
· rintro - ⟨x, hx, m, hm, rfl⟩
    rw [mem_baseChange_iff] at hx hm
    refine Submodule.span_induction₂ (p := fun x m _ _ ↦ ⁅x, m⁆ ∈ Submodule.span A s)
      ?_ (by simp) (by simp) ?_ ?_ ?_ ?_ hx hm
    · rintro - - ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩; exact Submodule.subset_span ⟨x, hx, y, hy, by simp⟩
    all_goals { intros; simp [add_mem, Submodule.smul_mem, *] }

Goal state after:
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
k : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
⊢ ↑(lowerCentralSeries R (↥(toEnd R L M).range) M (k + 1)) = ↑(lowerCentralSeries R L M (k + 1))

Tactic:
simp only [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (lowerCentralSeries R (toEnd R L M).range M k).mem_toSubmodule, ih]

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
k : ℕ
ih : ↑(lowerCentralSeries R (↥(toEnd R L M).range) M k) = ↑(lowerCentralSeries R L M k)
⊢ Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ↑(lowerCentralSeries R L M k), ⁅x_1, n⁆ = x} =
    Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}
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
his : i ∈ s
⊢ l i ∈ subfield G F

Tactic:
g

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
g : G
⊢ g • l i = l i
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
⊢ Polynomial.eval₂ (subfield G F).subtype x (minpoly G F x) = Polynomial.eval x (prodXSubSMul G F x)

Tactic:
Polynomial.eval₂_eq_eval_map

Goal state after:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ Polynomial.eval x (Polynomial.map (subfield G F).subtype (minpoly G F x)) = Polynomial.eval x (prodXSubSMul G F x)
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 ↥(IsScalarTower.toAlgHom F K L).range
        ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).roots.toFinset) =
    ⊤

Tactic:
IsScalarTower.adjoin_range_toAlgHom,

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 K L).comp (algebraMap F K)) g).roots.toFinset) =
    ⊤
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: case a.left
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin (↥(adjoin F S)) T)

pp: case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ ↑(adjoin (↥(adjoin F S)) T)

Tactic:
· exact Set.range_subset_iff.mpr fun f ↦ Subfield.subset_closure (.inl ⟨f, rfl⟩)

Goal state after:
case a.right
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ ↑(adjoin (↥(adjoin F S)) T)
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
p : (x : E) → x ∈ adjoin F s → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E) x) ⋯
add : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : x ∈ adjoin F s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x * y) ⋯
x : E
h : x ∈ adjoin F s
⊢ p 1 ⋯

Tactic:
by simp_rw [← (Algebra.algebraMap F E).map_one]; exact algebraMap 1

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

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : IsAlgClosed k
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Algebra.IsAlgebraic k ↥L
x : K
hx : x ∈ L
⊢ x ∈ ⊥

Tactic:
obtain ⟨y, hy⟩ := (IsAlgClosed.algebraMap_bijective_of_isIntegral (k := k)).2 (⟨x, hx⟩ : L)

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : IsAlgClosed k
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Algebra.IsAlgebraic k ↥L
x : K
hx : x ∈ L
y : k
hy : (algebraMap k ↥L) y = ⟨x, hx⟩
⊢ x ∈ ⊥
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case inl
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
h✝ : IsEmpty ι
⊢ ⊥.toSubalgebra = ⊥

Tactic:
bot_toSubalgebra

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
K : IntermediateField F E
⊢ K.toSubalgebra = ⊥ ↔ K.toSubalgebra = ⊥.toSubalgebra

Tactic:
bot_toSubalgebra

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ K.toSubalgebra = ⊥ ↔ K.toSubalgebra = ⊥
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.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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
⊢ x ∈ corootSpace α ↔ ↑x ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)

Tactic:
corootSpace

Goal state after:
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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
⊢ x ∈
      (LieModuleHom.codRestrict H.toLieSubmodule ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯))
          ⋯).range ↔
    ↑x ∈
      LieSubmodule.map H.toLieSubmodule.incl
        (LieModuleHom.codRestrict H.toLieSubmodule ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯))
            ⋯).range
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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
⊢ x ∈ corootSpace α ↔ x ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}

Tactic:
set s : Set H := ({⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} : Set H)

Goal state after:
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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
⊢ x ∈ corootSpace α ↔ x ∈ Submodule.span R s
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
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
χ₁ χ₂ : L → R
h : χ₁ ≠ χ₂
x : L
hx : χ₁ x ≠ χ₂ x
⊢ Disjoint (genWeightSpace M χ₁) (genWeightSpace M χ₂)

Tactic:
exact (disjoint_genWeightSpaceOf R L M hx).mono
    (genWeightSpace_le_genWeightSpaceOf M x χ₁) (genWeightSpace_le_genWeightSpaceOf M x χ₂)

Goal state after: