mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis (↥s) A M), P ((toMatrix b b) f).det
h1 : P 1
H : ¬∃ s, Nonempty (Basis (↥s) A M)
⊢ P (LinearMap.det f)

Tactic:
LinearMap.det_def,

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb : ∀ (s : Finset M) (b : Basis (↥s) A M), P ((toMatrix b b) f).det
h1 : P 1
H : ¬∃ s, Nonempty (Basis (↥s) A M)
⊢ P ((if H : ∃ s, Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1) f)
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
⊢ g.natDegree ≠ 0

Tactic:
intro this

Goal state after:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
this : g.natDegree = 0
⊢ False
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
H : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ Module.Finite R M

Tactic:
· classical simp [LinearMap.coe_det, H] at hf

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Free R M
f : M →ₗ[R] M
hf : LinearMap.det f = 0
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : Fin (finrank R M) → R
hv_ne_zero : v ≠ 0
hv_zero : (toMatrix b b) f *ᵥ v = 0
⊢ f (b.equivFun.symm v) = 0

Tactic:
rw [← b.equivFun.injective.eq_iff]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Free R M
f : M →ₗ[R] M
hf : LinearMap.det f = 0
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : Fin (finrank R M) → R
hv_ne_zero : v ≠ 0
hv_zero : (toMatrix b b) f *ᵥ v = 0
⊢ b.equivFun (f (b.equivFun.symm v)) = b.equivFun 0
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) g₂))
h : ∃ r, IsUnit r ∧ C r = g₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂

Tactic:
rcases h with ⟨r, hr, rfl⟩

Goal state after:
case inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : (C r).Separable
hg₁ : ((expand F (p ^ k)) (C r)).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) (C r)))
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) (C r) = C r
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case h₁
R : Type u_1
T : Type u_3
inst✝¹ : CommRing R
inst✝ : Semiring T
p : R[X]
f g : AdjoinRoot p →+* T
hAlg : f.comp (of p) = g.comp (of p)
hRoot : f (root p) = g (root p)
x : R
⊢ ((f.comp (Ideal.Quotient.mk (span {p}))).comp C) x = ((g.comp (Ideal.Quotient.mk (span {p}))).comp C) x

Tactic:
simpa using! congr($(hAlg) x)

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
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
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
⊢ M ≃ₗ[R] M

Tactic:
have : Finite ι := Module.Finite.finite_basis b

Goal state after:
case pos
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
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
this : Finite ι
⊢ M ≃ₗ[R] M
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (C r * X - 1) →ₐ[R] S
⊢ (algebraMap R S) r * g (root (C r * X - 1)) = 1

Tactic:
rw [← g.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]

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
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
G : Type u_5
inst✝² : Group G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
g : G
v : ι → M
⊢ (g • e).det v = e.det (g⁻¹ • v)

Tactic:
det_apply,

Goal state after:
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
G : Type u_5
inst✝² : Group G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
g : G
v : ι → M
⊢ ((g • e).toMatrix v).det = (e.toMatrix (g⁻¹ • v)).det
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ e.det (⇑f ∘ v) = LinearMap.det f * e.det v

Tactic:
det_apply,

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ (e.toMatrix (⇑f ∘ v)).det = LinearMap.det f * e.det v
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ (e.toMatrix (⇑f ∘ v)).det = LinearMap.det f * e.det v

Tactic:
det_apply,

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ (e.toMatrix (⇑f ∘ v)).det = LinearMap.det f * (e.toMatrix v).det
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ b'.det (⇑f ∘ ⇑b) = LinearMap.det (f ∘ₗ ↑(b'.equiv b (Equiv.refl ι)))

Tactic:
det_apply,

Goal state after:
M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ (b'.toMatrix (⇑f ∘ ⇑b)).det = LinearMap.det (f ∘ₗ ↑(b'.equiv b (Equiv.refl ι)))
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 ι
ι' : Type u_6
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.reindex e).det v = b.det (v ∘ ⇑e)

Tactic:
det_apply,

Goal state after:
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 ι
ι' : Type u_6
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ ((b.reindex e).toMatrix v).det = b.det (v ∘ ⇑e)
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 ι
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
⊢ (b.map f).det v = b.det (⇑f.symm ∘ v)

Tactic:
det_apply,

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 ι
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
⊢ ((b.map f).toMatrix v).det = b.det (⇑f.symm ∘ v)
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inr.inl
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 : n
k : m
⊢ W.mkQ (e ↑(bW k)) = 0

Tactic:
rw [← LinearMap.mem_ker, Submodule.ker_mkQ]

Goal state after:
case inr.inl
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 : n
k : m
⊢ e ↑(bW k) ∈ W
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 J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I ↦ ⁅I, I⁆, monotone' := ⋯ }
⊢ D (k + l) (I + J) ≤ D k I + D l J

Tactic:
have h₁ : ∀ I J : LieIdeal R L, D₁ (I ⊔ J) ≤ D₁ I ⊔ J := by
    simp [D₁, LieSubmodule.lie_le_right, LieSubmodule.lie_le_left, le_sup_of_le_right]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
k l : ℕ
D₁ : LieIdeal R L →o LieIdeal R L := { toFun := fun I ↦ ⁅I, I⁆, monotone' := ⋯ }
h₁ : ∀ (I J : LieIdeal R L), D₁ (I ⊔ J) ≤ D₁ I ⊔ J
⊢ D (k + l) (I + J) ≤ D k I + D l J
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case refine_1
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
⊢ ⊥ ∈ {I | IsSolvable ↥I}

Tactic:
exact LieAlgebra.isSolvableBot R L

Goal state after:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ map (↑g) (m • (C b * X ^ (n + 1))) = (MonoidHom.id M) m • map (↑g) (C b * X ^ (n + 1))

Tactic:
by rw [MonoidHom.id_apply, smul_mul', smul_C, smul_pow', smul_X,
        Polynomial.map_mul, map_C, Polynomial.map_pow,
        map_X, coe_fn_coe, g.map_smul, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X,
        smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]

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]
  rcases h : nilpotencyLength L M with - | k
  · exact bot_le
  · rw [le_max_triv_iff_bracket_eq_bot]
    rw [nilpotencyLength_eq_succ_iff R, lowerCentralSeries_succ] at h
    exact h.1

Goal state after:
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
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ⊤ ∈ s
⊢ LieModule.IsNilpotent (↥L') M

Tactic:
← isNilpotent_of_top_iff (R := R)

Goal state after:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ⊤ ∈ s
⊢ LieModule.IsNilpotent (↥⊤) 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
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ ⊤ ≤ ucs k N ↔ LieModule.lowerCentralSeries R L M k ≤ N

Tactic:
← lcs_le_iff

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
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lcs k ⊤ ≤ N ↔ LieModule.lowerCentralSeries R L M k ≤ N
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
M : Type w
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
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 : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) ≤ ↑(lowerCentralSeries R L₂ M₂ k)
⊢ Submodule.span R (⇑g '' {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}) ≤
    ↑(lowerCentralSeries R L₂ M₂ (k + 1))

Tactic:
Submodule.span_le

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
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 : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) ≤ ↑(lowerCentralSeries R L₂ M₂ k)
⊢ ⇑g '' {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x} ⊆ ↑↑(lowerCentralSeries R L₂ M₂ (k + 1))
Module: Mathlib.FieldTheory.Tower

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝⁶ : Semiring F
inst✝⁵ : Semiring K
inst✝⁴ : Module F K
inst✝³ : AddCommMonoid A
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : Module.Finite F A
b : Finset A
hb : span F ↑b = ⊤
⊢ span F ↑b ≤ restrictScalars F (span K ↑b)

Tactic:
Submodule.span_le

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝⁶ : Semiring F
inst✝⁵ : Semiring K
inst✝⁴ : Module F K
inst✝³ : AddCommMonoid A
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : Module.Finite F A
b : Finset A
hb : span F ↑b = ⊤
⊢ ↑b ⊆ ↑(restrictScalars F (span K ↑b))
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case s
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
| s

pp: case f
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
| fun c ↦ ((g • l c - l c) • (toFun G F) c) g'

Tactic:
· skip

Goal state after:
case f
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
| fun c ↦ ((g • l c - l c) • (toFun G F) c) g'
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case s
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
| s

pp: case f
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
| fun x ↦ g • l x * (toFun G F) x g'

Tactic:
· skip

Goal state after:
case f
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
| fun x ↦ g • l x * (toFun G F) x g'
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: K₁ : Type u_6
K₂ : Type u_7
F : Type u_8
K₃ : Type u_9
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
inst✝⁸ : Algebra K₁ K₂
inst✝⁷ : Algebra K₁ K₃
inst✝⁶ : Algebra K₂ K₃
inst✝⁵ : IsScalarTower F K₁ K₃
inst✝⁴ : IsScalarTower F K₁ K₂
inst✝³ : IsScalarTower F K₂ K₃
inst✝² : IsScalarTower K₁ K₂ K₃
inst✝¹ : Normal F K₁
inst✝ : Normal F K₂
f : Gal(K₃/F)
⊢ (AlgEquiv.restrictNormalHom K₁) f = (AlgEquiv.restrictNormalHom K₁) ((AlgEquiv.restrictNormalHom K₂) f)

Tactic:
by
  rw [IsScalarTower.AlgEquiv.restrictNormalHom_comp F K₁ K₂ K₃, MonoidHom.comp_apply]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro
M : Type u
inst✝⁸ : Monoid M
G : Type u
inst✝⁷ : Group G
K : Type u_1
F : Type v
inst✝⁶ : Field F
inst✝⁵ : MulSemiringAction M F
inst✝⁴ : MulSemiringAction G F
m : M
inst✝³ : Field K
inst✝² : Algebra K F
inst✝¹ : SMulCommClass M K F
inst✝ : Finite G
val✝ : Fintype G
⊢ FiniteDimensional (↥(subfield G F)) F

Tactic:
exact IsNoetherian.iff_fg.1
    (IsNoetherian.iff_rank_lt_aleph0.2 <| (rank_le_card G F).trans_lt Cardinal.natCast_lt_aleph0)

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : IsAlgClosed K
inst✝ : FiniteDimensional K V
f : End K V
⊢ ∀ (n : ℕ), finrank K V = n → ⨆ μ, f.maxGenEigenspace μ = ⊤

Tactic:
intro n h_dim

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : IsAlgClosed K
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
h_dim : finrank K V = n
⊢ ⨆ μ, f.maxGenEigenspace μ = ⊤
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : eval a f = 0
h0 : 0 < rootMultiplicity a f
h : f.IsRoot a → g.IsRoot a
⊢ rootMultiplicity a f ≤ rootMultiplicity a f - 1 + rootMultiplicity a g

Tactic:
calc rootMultiplicity a f
        = rootMultiplicity a f - 1 + 1 := (Nat.sub_add_cancel (Nat.succ_le_iff.1 h0)).symm
      _ ≤ rootMultiplicity a f - 1 + rootMultiplicity a g := add_le_add le_rfl (Nat.succ_le_iff.1
        ((rootMultiplicity_pos hg0).2 (h haf)))

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
χ₁ : ι → R
a✝ : χ₁ ∈ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}
χ₂ : ι → R
hχ₂ : χ₂ ∈ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}
hχ₁₂ : ⨅ i, (f i).maxGenEigenspace (χ₁ i) = ⨅ i, (f i).maxGenEigenspace (χ₂ i)
⊢ χ₁ = χ₂

Tactic:
contrapose! hχ₂

Goal state after:
ι : 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
χ₁ : ι → R
a✝ : χ₁ ∈ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}
χ₂ : ι → R
hχ₁₂ : ⨅ i, (f i).maxGenEigenspace (χ₁ i) = ⨅ i, (f i).maxGenEigenspace (χ₂ i)
hχ₂ : χ₁ ≠ χ₂
⊢ χ₂ ∉ {χ | ⨅ i, (f i).maxGenEigenspace (χ i) ≠ ⊥}
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case succ
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
ih : ∃ L, FiniteDimensional F ↥L ∧ n < finrank F ↥L
⊢ ∃ L, FiniteDimensional F ↥L ∧ n + 1 < finrank F ↥L

Tactic:
obtain ⟨L, fin, hn⟩ := ih

Goal state after:
case succ
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional F ↥L
hn : n < finrank F ↥L
⊢ ∃ L, FiniteDimensional F ↥L ∧ n + 1 < finrank F ↥L
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
k : ℕ
⊢ LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule

Tactic:
by
  induction k with
  | zero => simp
  | succ k ih => simp [ih]

Goal state after: