mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
hx : x ∈ Submodule.span R₁ S
⊢ x ∈ Submodule.span R₂ S

Tactic:
induction hx using Submodule.closure_induction with
  | zero => exact Submodule.zero_mem _
  | add y z hy₁ hz₁ hy₂ hz₂ => exact Submodule.add_mem _ hy₂ hz₂
  | smul_mem c y hy =>
      obtain ⟨a, ha, b, hb, rfl⟩ := hy
      rw [← smul_lie]
      refine Submodule.subset_span ⟨c • a, ?_, b, hb, rfl⟩
      rw [← ih] at ha ⊢
      exact Submodule.smul_mem _ _ ha

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
k : ℕ
⊢ ↑↑(derivedSeriesOfIdeal R L k ⊤) = ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)

Tactic:
induction k with

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

Goal state before:
pp: case h
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
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k = ⊥
⊢ derivedSeries R L k = ⊥

Tactic:
rw [eq_bot_iff] at h ⊢

Goal state after:
case h
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
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k ≤ ⊥
⊢ derivedSeries R L k ≤ ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
k : ℕ
⊢ lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂

Tactic:
induction k with

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
k : ℕ
⊢ ↑↑(lowerCentralSeries R L M k) = ↑↑(lowerCentralSeries ℤ L M k)

Tactic:
induction k with

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
⊢ lcs k N ≤ N

Tactic:
induction k with

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
⊢ lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)

Tactic:
induction k with

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
x : L
m : M
k : ℕ
⊢ (⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k

Tactic:
induction k with

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
x y : L
m : M
k : ℕ
⊢ (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)

Tactic:
induction k with

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 : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k

Tactic:
induction k with

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 : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
⊢ lowerCentralSeries R L M₂ k ≤ LieSubmodule.map f (lowerCentralSeries R L M k)

Tactic:
induction k with

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

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆ ≤ ⁅⊤, lowerCentralSeries R L L k⁆

Tactic:
exact LieSubmodule.mono_lie h' h

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
k : ℕ
⊢ derivedSeries R L k ≤ lowerCentralSeries R L L k

Tactic:
induction k with

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
inst✝ : IsNilpotent L M
⊢ ∃ k, ∀ (x : L), (toEnd R L M) x ^ k = 0

Tactic:
obtain ⟨k, hM⟩ := IsNilpotent.nilpotent R L M

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
inst✝ : IsNilpotent L M
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ ∃ k, ∀ (x : L), (toEnd R L M) x ^ k = 0
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
inst✝ : IsNilpotent L M
x y : L
⊢ _root_.IsNilpotent ((toEnd R L M) x ∘ₗ (toEnd R L M) y)

Tactic:
obtain ⟨k, hM⟩ := IsNilpotent.nilpotent R L M

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
inst✝ : IsNilpotent L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ _root_.IsNilpotent ((toEnd R L M) x ∘ₗ (toEnd R L M) y)
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
⊢ ∃ K', IsEngelian R ↥K' ∧ K < K'

Tactic:
have hxK' : x ∈ K' := Submodule.mem_sup_left (Submodule.subset_span (Set.mem_singleton _))

Goal state after:
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
⊢ ∃ K', IsEngelian R ↥K' ∧ K < K'
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule (↥K') M
_i4 : LieModule R (↥K') M
h : ∀ (x : ↥K'), IsNilpotent ((toEnd R (↥K') M) x)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
⊢ R ∙ ⟨x, hxK'⟩ ⊔ (LieSubalgebra.ofLe hKK').toSubmodule = ⊤

Tactic:
apply Submodule.map_injective_of_injective (K' : Submodule R L).injective_subtype

Goal state after:
R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L := ⋯
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule (↥K') M
_i4 : LieModule R (↥K') M
h : ∀ (x : ↥K'), IsNilpotent ((toEnd R (↥K') M) x)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
⊢ Submodule.map K'.subtype (R ∙ ⟨x, hxK'⟩ ⊔ (LieSubalgebra.ofLe hKK').toSubmodule) = Submodule.map K'.subtype ⊤
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
hK₁ : IsEngelian R ↥K
hK₂ : K < K.normalizer
x : L
hx₁ : x ∈ K.normalizer
hx₂ : x ∉ K
K' : LieSubalgebra R L :=
  let __src := R ∙ x ⊔ K.toSubmodule;
  { toSubmodule := __src, lie_mem' := ⋯ }
hxK' : x ∈ K'
hKK' : K ≤ K'
hK' : K' ≤ K.normalizer
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule (↥K') M
_i4 : LieModule R (↥K') M
h : ∀ (x : ↥K'), IsNilpotent ((toEnd R (↥K') M) x)
I : LieIdeal R ↥K'
hI₁ : LieIdeal.toLieSubalgebra R (↥K') I = LieSubalgebra.ofLe hKK'
⊢ Submodule.map K'.subtype (R ∙ ⟨x, hxK'⟩) ⊔ K.toSubmodule = K'.toSubmodule

Tactic:
rw [Submodule.map_subtype_span_singleton]

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

Tactic:
induction k with

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
h : N₁ ≤ N₂
⊢ ucs k N₁ ≤ ucs k N₂

Tactic:
induction k with

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ucs k N₁ = N₁

Tactic:
induction k with

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ comap N.incl (ucs k ⊥) = ucs k ⊥

Tactic:
induction k with

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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁴ : LieRing L₂
inst✝³ : LieAlgebra R L₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
k : ℕ
⊢ Submodule.map g ↑(lowerCentralSeries R L M k) ≤ ↑(lowerCentralSeries R L₂ M₂ k)

Tactic:
induction k with

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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝ : LieModule R L₂ M₂
hf_surj : Surjective ⇑f
hg_surj : Surjective ⇑g
k : ℕ
⊢ ↑(lowerCentralSeries R L₂ M₂ k) ≤ Submodule.map g ↑(lowerCentralSeries R L M k)

Tactic:
induction k with

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
k : ℕ
⊢ ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)

Tactic:
induction k with

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
k : ℕ
⊢ ↑(lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(lowerCentralSeries R L (↥I) k)

Tactic:
induction k with

Goal state after:
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

Goal state after:
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'
h : Function.Surjective ⇑f
h' : map f ⊤ = ⊤
⊢ map f (lowerCentralSeries R L L k) = lowerCentralSeries R L' L' k

Tactic:
induction k with

Goal state after:
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)
ha : ∃ l ∈ Finsupp.supported F F ↑s, (Finsupp.linearCombination F ⇑(toFun G F)) l = (toFun G F) a
⊢ False

Tactic:
rcases ha with ⟨l, hl, hla⟩

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 : (Finsupp.linearCombination F ⇑(toFun G F)) l = (toFun G F) a
⊢ False
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
inst✝ : LieModule R L M
⊢ ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)

Tactic:
induction k with

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
k : ℕ
⊢ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k = baseChange A (lowerCentralSeries R L M k)

Tactic:
induction k with

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
⊢ adjoin F S = ⊥ ↔ S ⊆ ↑⊥

Tactic:
by
  rw [eq_bot_iff, adjoin_le_iff]

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

Goal state before:
pp: case refine_1
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : (aeval 0) p ≠ 0 ∨ (aeval 0) q ≠ 0
⊢ ¬(p = 0 ∧ q = 0)

Tactic:
contrapose! h

Goal state after:
case refine_1
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
p q : k[X]
h : p = 0 ∧ q = 0
⊢ (aeval 0) p = 0 ∧ (aeval 0) q = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case h.zero
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
ih :
  ∀ m < 0,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = 0
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤

Tactic:
rw [← top_le_iff]
    simp only [Submodule.finrank_eq_zero.1 (Eq.trans (finrank_top _ _) h_dim), bot_le]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case h.succ
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
h_dim_add : finrank K ↥ER + finrank K ↥ES = finrank K V
h_dim_ER : finrank K ↥ER < n.succ
ih_ER : ⨆ μ, f'.maxGenEigenspace μ = ⊤
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤

Tactic:
have ih_ER' : ⨆ (μ : K), (f'.maxGenEigenspace μ).map ER.subtype = ER := by
      simp only [(Submodule.map_iSup _ _).symm, ih_ER, Submodule.map_subtype_top ER]

Goal state after:
case h.succ
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
h_dim_add : finrank K ↥ER + finrank K ↥ES = finrank K V
h_dim_ER : finrank K ↥ER < n.succ
ih_ER : ⨆ μ, f'.maxGenEigenspace μ = ⊤
ih_ER' : ⨆ μ, Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤
Module: Mathlib.FieldTheory.Extension

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

Tactic:
iSup_range',

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
n : ℕ
⊢ (algebraMap (↥K) E) ((minpoly (↥K) α).coeff n) ∈ ↑K

Tactic:
apply Subtype.mem

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_2.refine_1
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
S : Set E
L : Type u_4
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
f : L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits
L' : IntermediateField F E := (IsScalarTower.toAlgHom F L E).fieldRange
f' : ↥L' →ₐ[F] K := f.comp ↑(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).symm
φ : ↥(adjoin (↥L') S) →ₐ[F] K
hφ : AlgHom.domRestrict (↥L') φ = f'
⊢ Set.range ⇑(algebraMap L E) ⊆ ↑(adjoin (↥L') S) ∧ S ⊆ ↑(adjoin (↥L') S)

Tactic:
exact ⟨subset_adjoin_of_subset_left S (F := L'.toSubfield) le_rfl, subset_adjoin _ _⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ : ι → R
s : Finset (ι → R)
⊢ χ₁ ∉ s → Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert χ₂ s _n ih =>
  intro hχ₁₂
  obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂
  specialize ih hχ₁
  rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
  rintro x ⟨hx, hx'⟩
  simp only [SetLike.mem_coe] at hx hx'
  suffices x ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i) by
    rw [← Submodule.mem_bot (R := R), ← (disjoint_iInf_maxGenEigenspace f hχ₁₂).eq_bot]
    exact ⟨hx, this⟩
  obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx'
  suffices ∀ l, ∃ (k : ℕ),
      ((f l - algebraMap R (Module.End R M) (χ₂ l)) ^ k) (y + z) ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓
        Finset.sup s fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i) by
    simpa [ih.eq_bot, Submodule.mem_bot] using! this
  intro l
  let g : Module.End R M := f l - algebraMap R (Module.End R M) (χ₂ l)
  obtain ⟨k, hk : (g ^ k) y = 0⟩ := (mem_iInf_maxGenEigenspace_iff _ _ _).mp hy l
  have aux (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M) (hp : MapsTo f p p) :
      MapsTo ((f - algebraMap R (Module.End R M) φ) ^ k) p p := by
    rw [Module.End.coe_pow]
    exact MapsTo.iterate (fun m hm ↦ p.sub_mem (hp hm) (p.smul_mem _ hm)) k
  refine ⟨k, Submodule.mem_inf.mp ⟨?_, ?_⟩⟩
  · refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ?_ hx
    simp only [Submodule.coe_iInf]
    exact h l χ₁
  · rw [map_add, hk, zero_add]
    suffices (s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i))).map (g ^ k) ≤
        s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i)) from
      this (Submodule.mem_map_of_mem hz)
    simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := ι → R), Submodule.map_iSup (ι := _ ∈ s)]
    refine iSup₂_mono fun χ _ ↦ ?_
    rintro - ⟨u, hu, rfl⟩
    refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ i)) ?_ hu
    simp only [Submodule.coe_iInf]
    exact h l χ

Goal state after: