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✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ ((Pi.basis fun x ↦ b).repr
        ((pi fun i ↦ f i ∘ₗ proj i)
          ((Pi.basis fun x ↦ b)
            (((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans
                  (Equiv.prodComm ι (Free.ChooseBasisIndex R M))).symm
              (j₁, j₂)))))
      (((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M))).symm
        (i₁, i₂)) =
    if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0

Tactic:
Equiv.symm_trans_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✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ ((Pi.basis fun x ↦ b).repr
        ((pi fun i ↦ f i ∘ₗ proj i)
          ((Pi.basis fun x ↦ b)
            ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).symm
              ((Equiv.prodComm ι (Free.ChooseBasisIndex R M)).symm (j₁, j₂))))))
      ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).symm
        ((Equiv.prodComm ι (Free.ChooseBasisIndex R M)).symm (i₁, i₂))) =
    if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: K : Type u_5
m : Type u_6
F : Type u_7
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
⊢ (f x).det = x.det

Tactic:
by_cases! Nonempty m

Goal state after:
case pos
K : Type u_5
m : Type u_6
F : Type u_7
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : Nonempty m
⊢ (f x).det = x.det

case neg
K : Type u_5
m : Type u_6
F : Type u_7
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : IsEmpty m
⊢ (f x).det = x.det
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S[X]
p q : R[X]
a✝¹ : (aeval (root f)) p = (mk f) (Polynomial.map (algebraMap R S) p)
a✝ : (aeval (root f)) q = (mk f) (Polynomial.map (algebraMap R S) q)
⊢ (aeval (root f)) (p + q) = (mk f) (Polynomial.map (algebraMap R S) (p + q))

Tactic:
simp_all

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
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit ((toMatrix v v') f).det
x : M
⊢ ((toLin v' v) ((toMatrix v v') f)⁻¹) (f x) =
    ((toLin v' v) ((toMatrix v v') f)⁻¹ ∘ₗ (toLin v v') ((toMatrix v v') f)) x

Tactic:
toLin_toMatrix,

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
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit ((toMatrix v v') f).det
x : M
⊢ ((toLin v' v) ((toMatrix v v') f)⁻¹) (f x) = ((toLin v' v) ((toMatrix v v') f)⁻¹ ∘ₗ f) x
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
this✝ : Finite ι
this : Fintype ι
⊢ M ≃ₗ[R] M

Tactic:
have : DecidableEq ι := Classical.typeDecidableEq ι

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 ι
this✝ : Fintype ι
this : DecidableEq ι
⊢ M ≃ₗ[R] M
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 : End K M
p : K[X]
hp : Squarefree p
hpf : p ∈ RingHom.ker (aeval f)
⊢ f.IsSemisimple

Tactic:
← AEval.annihilator_eq_ker_aeval (M := M),

Goal state after:
M : Type u_2
inst✝² : AddCommGroup M
K : Type u_3
inst✝¹ : Field K
inst✝ : Module K M
f : End K M
p : K[X]
hp : Squarefree p
hpf : p ∈ annihilator K[X] (AEval K M f)
⊢ f.IsSemisimple
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 : End K M
p : K[X]
hp : Squarefree p
hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})
R : Type u_3 := K[X] ⧸ Ideal.span {p}
this✝³ : IsReduced R
this✝² : FiniteDimensional K R
this✝¹ : IsArtinianRing R
this✝ : IsSemisimpleRing R
this : Module R (AEval' f) := hpf.module
e : AEval' f →ₛₗ[Ideal.Quotient.mk (Ideal.span {p})] AEval' f :=
  let __src := AddMonoidHom.id (AEval' f);
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ f.IsSemisimple

Tactic:
exact (e.isSemisimpleModule_iff_of_bijective bijective_id).mpr inferInstance

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_3.i_inj
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₁ y₁ : ℕ
h₁ : ⟨x₁, y₁⟩.snd < ⟨x₁, y₁⟩.fst + 1
x₂ y₂ : ℕ
h₂ : ⟨x₂, y₂⟩.snd < ⟨x₂, y₂⟩.fst + 1
h₃ : ⟨x₁, y₁⟩.snd = ⟨x₂, y₂⟩.snd
h₄ : ⟨x₁, y₁⟩.fst - ⟨x₁, y₁⟩.snd = ⟨x₂, y₂⟩.fst - ⟨x₂, y₂⟩.snd
⊢ ⟨x₁, y₁⟩ = ⟨x₂, y₂⟩

Tactic:
simp_all

Goal state after:
case calc_3.i_inj
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₁ y₁ x₂ y₂ : ℕ
h₁ : y₂ ≤ x₁
h₂ : y₂ ≤ x₂
h₃ : y₁ = y₂
h₄ : x₁ - y₂ = x₂ - y₂
⊢ x₁ = x₂
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_3.i_surj
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 : ℕ := ⋯
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := ⋯
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := ⋯
hRN : RN = range (N + 1)
⊢ ∀ b ∈ {ij ∈ range (2 * N + 1) ×ˢ range (2 * N + 1) | ij.1 + ij.2 ≤ 2 * N},
    ∃ a,
      ∃ (ha : a ∈ (range (2 * N + 1)).sigma fun i ↦ range (i + 1)),
        (match a, ha with
          | ⟨i, j⟩, x => (j, i - j)) =
          b

Tactic:
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⟩

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

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ D 0 I ≤ D l J

Tactic:
h₂,

Goal state after:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ D 0 I ≤ D 0 J
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
fM : End R M
fN : End R N
g : M →ₗ[R] N
h : fN ∘ₗ g = g ∘ₗ fM
m : M
k l : ℕ
kl : ℕ := max k l
hfM : fM ^ kl = 0
hfN : fN ^ kl = 0
this : ∀ (i : ℕ), (fN ^ i) (g m) = g ((fM ^ i) m)
⊢ (exp fN ∘ₗ g) m = (g ∘ₗ exp fM) m

Tactic:
simp [exp_eq_sum hfM, exp_eq_sum hfN, this, map_rat_smul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
this : ((bracket' R A L L) z₁) z₂ + ((bracket' R A L L) z₂) z₁ = 0
⊢ 0 + ((bracket' R A L L) z₂) z₁ + (((bracket' R A L L) z₁) z₂ + ((bracket' R A L L) z₂) z₂) = 0

Tactic:
h₂,

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
this : ((bracket' R A L L) z₁) z₂ + ((bracket' R A L L) z₂) z₁ = 0
⊢ 0 + ((bracket' R A L L) z₂) z₁ + (((bracket' R A L L) z₁) z₂ + 0) = 0
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: case refine_1
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
⊢ ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0

pp: case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
⊢ H.normalizer ≤ H

Tactic:
· rintro ⟨x⟩ hx
    suffices x ∈ H by rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
      coe_toLieSubmodule, mem_toSubmodule]
    rw [← h, H.mem_normalizer_iff']
    intro y hy
    replace hx : ⁅_, LieSubmodule.Quotient.mk' _ x⁆ = 0 := hx ⟨y, hy⟩
    rwa [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero] at hx

Goal state after:
case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
⊢ H.normalizer ≤ H
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case refine_2
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 : LieSubmodule R L L
hI : IsSolvable ↥I
J : LieSubmodule R L L
hJ : IsSolvable ↥J
⊢ IsSolvable ↥(I ⊔ J)

Tactic:
apply LieAlgebra.isSolvableAdd R L

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
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y x✝ y✝ : A ⊗[R] L
⊢ ∀ (x y : A ⊗[R] L),
    ((TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x✝) x) =
          ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x✝))
            ((TensorProduct.map f.toLinearMap ↑g) x) →
        (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y✝) x) =
            ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y✝))
              ((TensorProduct.map f.toLinearMap ↑g) x) →
          (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝ + y✝)) x) =
            ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝ + y✝)))
              ((TensorProduct.map f.toLinearMap ↑g) x)) →
      ((TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x✝) y) =
            ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x✝))
              ((TensorProduct.map f.toLinearMap ↑g) y) →
          (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y✝) y) =
              ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y✝))
                ((TensorProduct.map f.toLinearMap ↑g) y) →
            (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝ + y✝)) y) =
              ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝ + y✝)))
                ((TensorProduct.map f.toLinearMap ↑g) y)) →
        (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x✝) (x + y)) =
            ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x✝))
              ((TensorProduct.map f.toLinearMap ↑g) (x + y)) →
          (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y✝) (x + y)) =
              ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y✝))
                ((TensorProduct.map f.toLinearMap ↑g) (x + y)) →
            (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝ + y✝)) (x + y)) =
              ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝ + y✝)))
                ((TensorProduct.map f.toLinearMap ↑g) (x + y))

Tactic:
simp_all

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

Goal state before:
pp: case succ.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 i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ ↑⁅I, ⊤.lcs M (i + l)⁆ ≤ ↑⁅I, I.lcs M j⁆

Tactic:
norm_cast
      gcongr
      exact le_trans (antitone_lowerCentralSeries R L M le_self_add) hIM

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x' y' : L ⧸ I
⊢ ⁅x', t • y'⁆ = t • ⁅x', y'⁆

Tactic:
by
    induction x', y' using Quotient.inductionOn₂' with | _ x y
    repeat'
      first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_smul (R := R) (M := L)]
    apply congr_arg; apply lie_smul

Goal state after:
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 = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
⊢ LieModule.IsNilpotent L M

Tactic:
have hk' : I.lcs M k = ⊥ := by
    simp only [← toSubmodule_inj, I.coe_lcs_eq, hk, bot_toSubmodule]

Goal state after:
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 = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
⊢ LieModule.IsNilpotent L M
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case refine_1
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
inst✝ : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L M)
⊢ ⊥ ∈ {N | IsNilpotent L ↥N}

Tactic:
simp_all

Goal state after:
case refine_1
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
inst✝ : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L M)
⊢ IsNilpotent L ↥⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case refine_2
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
inst✝ : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L M)
N₁ : LieSubmodule R L M
h₁ : N₁ ∈ {N | IsNilpotent L ↥N}
N₂ : LieSubmodule R L M
h₂ : N₂ ∈ {N | IsNilpotent L ↥N}
⊢ N₁ ⊔ N₂ ∈ {N | IsNilpotent L ↥N}

Tactic:
simp_all

Goal state after:
case refine_2
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
inst✝ : IsNoetherian R M
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L M)
N₁ N₂ : LieSubmodule R L M
h₁ : IsNilpotent L ↥N₁
h₂ : IsNilpotent L ↥N₂
⊢ IsNilpotent L ↥(N₁ ⊔ N₂)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this :
  Subalgebra.restrictScalars K (adjoin ↥E1 ↑E2).toSubalgebra = Subalgebra.restrictScalars K (Algebra.adjoin ↥E1 ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
← restrictScalars_toSubalgebra,

Goal state after:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (restrictScalars K (adjoin ↥E1 ↑E2)).toSubalgebra = Subalgebra.restrictScalars K (Algebra.adjoin ↥E1 ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'
⊢ Subalgebra.restrictScalars F (adjoin E ↑L).toSubalgebra = Subalgebra.restrictScalars F (Algebra.adjoin E ↑L)

Tactic:
← restrictScalars_toSubalgebra,

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i
hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'
⊢ (restrictScalars F (adjoin E ↑L)).toSubalgebra = Subalgebra.restrictScalars F (Algebra.adjoin E ↑L)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
⊢ (adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L

Tactic:
by
  let i := IsScalarTower.toAlgHom F E K
  let E' := i.fieldRange
  let i' : E ≃ₐ[F] E' := AlgEquiv.ofInjectiveField i
  have hi : algebraMap E K = (algebraMap E' K) ∘ i' := by ext x; rfl
  apply_fun _ using Subalgebra.restrictScalars_injective F
  rw [← restrictScalars_toSubalgebra, restrictScalars_adjoin_of_algEquiv i' hi,
    Algebra.restrictScalars_adjoin_of_algEquiv i' hi, restrictScalars_adjoin]
  dsimp only [← E'.coe_type_toSubalgebra]
  rw [Algebra.restrictScalars_adjoin F E'.toSubalgebra]
  exact E'.sup_toSubalgebra_of_isAlgebraic L (halg.imp
    (fun (_ : Algebra.IsAlgebraic F E) ↦ i'.isAlgebraic) id)

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

Goal state before:
pp: F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑f).fieldRange = Subfield.closure (Set.range ⇑(algebraMap F L) ∪ s)

Tactic:
refine ringHom_fieldRange_eq_of_comp_eq_of_range_eq h ?_

Goal state after:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁸ : Field F
inst✝⁷ : CommRing A
inst✝⁶ : Algebra F A
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Field L
inst✝ : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h : (↑f).comp (algebraMap A K) = ↑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑g).range = Subring.closure (Set.range ⇑(algebraMap F L) ∪ s)
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case h.C
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
x : k
a✝ : k'
⊢ e.symm (eval (e x) (C a✝)) = eval x (map e.symm.toRingHom (C a✝))

Tactic:
simp_all

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

Goal state before:
pp: case h.add
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
x : k
p✝ q✝ : k'[X]
a✝¹ : e.symm (eval (e x) p✝) = eval x (map e.symm.toRingHom p✝)
a✝ : e.symm (eval (e x) q✝) = eval x (map e.symm.toRingHom q✝)
⊢ e.symm (eval (e x) (p✝ + q✝)) = eval x (map e.symm.toRingHom (p✝ + q✝))

Tactic:
simp_all

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

Goal state before:
pp: case h.monomial
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
x : k
n✝ : ℕ
a✝¹ : k'
a✝ : e.symm (eval (e x) (C a✝¹ * X ^ n✝)) = eval x (map e.symm.toRingHom (C a✝¹ * X ^ n✝))
⊢ e.symm (eval (e x) (C a✝¹ * X ^ (n✝ + 1))) = eval x (map e.symm.toRingHom (C a✝¹ * X ^ (n✝ + 1)))

Tactic:
simp_all

Goal state after: