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

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 : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0

Tactic:
rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_eq_bot_iff]
  refine ⟨fun h x hx m hm => h ⁅x, m⁆ ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩
  rintro h - ⟨⟨x, hx⟩, ⟨⟨n, hn⟩, rfl⟩⟩
  exact h x hx n hn

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x : M
⊢ x ∈ ↑N ⊓ ↑N' ↔ x ∈ ↑N ∧ x ∈ ↑N'

Tactic:
Submodule.mem_inf

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x : M
⊢ x ∈ ↑N ∧ x ∈ ↑N' ↔ x ∈ ↑N ∧ x ∈ ↑N'
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
⊢ s ⊆ ↑(lieSpan R L s)

Tactic:
by
  intro m hm
  rw [SetLike.mem_coe, mem_lieSpan]
  intro N hN
  exact hN hm

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

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (Polynomial.aeval x) (⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) = 0

Tactic:
exact (degree_lt_wf.min_mem _ hx).2

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

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ minpoly A x ∣ p

Tactic:
← modByMonic_eq_zero_iff_dvd (monic hx)

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hp : (Polynomial.aeval x) p = 0
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ p %ₘ minpoly A x = 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : ∑ i, (pb.basis.repr b) i • pb.basis i = b
⊢ b ≡ (algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩) [SMOD Ideal.span {pb.gen}]

Tactic:
rw [← insert_erase (mem_univ ⟨0, pb.dim_pos⟩), sum_insert (notMem_erase _ _)] at H

Goal state after:
case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b
⊢ b ≡ (algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩) [SMOD Ideal.span {pb.gen}]
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆ = 2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆)

Tactic:
by rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) (f %ₘ minpoly A pb.gen)

Tactic:
have : (f %ₘ minpoly A pb.gen).natDegree < pb.dim := by
    rw [← pb.natDegree_minpoly]
    apply natDegree_lt_natDegree hf
    exact degree_modByMonic_lt _ (minpoly.monic pb.isIntegral_gen)

Goal state after:
case neg
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) (f %ₘ minpoly A pb.gen)
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬Separable 0

Tactic:
rintro ⟨x, y, h⟩

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
x y : R[X]
h : x * 0 + y * derivative 0 = 1
⊢ False
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
h : (f ^ (n + 2)).Separable
⊢ IsUnit f ∨ f.Separable ∧ n + 2 = 1 ∨ n + 2 = 0

Tactic:
pow_succ,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
h : (f ^ (n + 1) * f).Separable
⊢ IsUnit f ∨ f.Separable ∧ n + 2 = 1 ∨ n + 2 = 0
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ emultiplicity a x ≤ 1 ∨ IsUnit a

Tactic:
rw [or_iff_not_imp_right]
    intro hu
    rcases eq_or_ne a 0 with rfl | h0
    · simp [x0]
    rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
    apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)
    rw [emultiplicity_eq_count_normalizedFactors hib x0]
    exact_mod_cast h (normalize b)

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
a✝ : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
⊢ (M * N).det = ((N * M).submatrix ⇑e ⇑e).det

Tactic:
← submatrix_mul_equiv _ _ _ (Equiv.refl n) _,

Goal state after:
A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
a✝ : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
⊢ (M * N).det = (N.submatrix ⇑e ⇑(Equiv.refl n) * M.submatrix ⇑(Equiv.refl n) ⇑e).det
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ¬∃ s, Nonempty (Basis (↥s) A M)
⊢ LinearMap.det (c • f) = c ^ finrank A M * LinearMap.det f

Tactic:
have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H
      simp [coe_det, H, this]

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case prime
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
f✝ : K[X]
hf : Irreducible f✝
⊢ f✝.Separable

Tactic:
rcases separable_or p hf with h | ⟨-, g, -, rfl⟩

Goal state after:
case prime.inl
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
f✝ : K[X]
hf : Irreducible f✝
h : f✝.Separable
⊢ f✝.Separable

case prime.inr
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
g : K[X]
hf : Irreducible ((expand K p) g)
⊢ ((expand K p) g).Separable
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : (X ^ p ^ 1 - C y).roots = p ^ 1 • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}

Tactic:
rwa [pow_one, iterateFrobeniusEquiv_one] at H

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
m : ℕ
H : ((X ^ p ^ 1 - C y) ^ m).roots = (m * p ^ 1) • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}

Tactic:
rwa [pow_one, iterateFrobeniusEquiv_one] at H

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✝² : 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)))
⊢ (toMatrix B B) (pi fun i ↦ f i ∘ₗ proj i) = blockDiagonal fun i ↦ (toMatrix b b) (f i)

Tactic:
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩

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₂ : ι
⊢ (toMatrix B B) (pi fun i ↦ f i ∘ₗ proj i) (i₁, i₂) (j₁, j₂) =
    blockDiagonal (fun i ↦ (toMatrix b b) (f i)) (i₁, i₂) (j₁, j₂)
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ ∃ s, p = s • annIdealGenerator 𝕜 a

Tactic:
@eq_comm _ p,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ ∃ s, s • annIdealGenerator 𝕜 a = p
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hli
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := ⋯
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
⊢ LinearIndependent K fun i ↦ root f ^ ↑i

Tactic:
rw [← deg_f', ← minpoly_eq]
    exact linearIndependent_pow (root f)

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ eval₂ ↑(ofId R ↥R[x]) ⟨x, ⋯⟩ (minpoly R x) = 0

Tactic:
change aeval _ _ = _; simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe]

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 : End K M
t : K
h : f.IsSemisimple
⊢ (t • f).IsSemisimple

Tactic:
by
  wlog ht : t ≠ 0; · simp [not_not.mp ht]
  rwa [IsSemisimple_smul_iff ht]

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ (x y : LieDerivation R L L), ↑(x + y) = ↑x + ↑y

Tactic:
intro D1 D2

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 : LieDerivation R L L
⊢ ↑(D1 + D2) = ↑D1 + ↑D2
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ (m : R) (x : LieDerivation R L L), ↑(m • x) = (RingHom.id R) m • ↑x

Tactic:
intro D1 D2

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 : R
D2 : LieDerivation R L L
⊢ ↑(D1 • D2) = (RingHom.id R) D1 • ↑D2
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ {x y : LieDerivation R L L}, ↑⁅x, y⁆ = ⁅↑x, ↑y⁆

Tactic:
intro D1 D2

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 : LieDerivation R L L
⊢ ↑⁅D1, D2⁆ = ⁅↑D1, ↑D2⁆
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 : L
⊢ x ∈ (ad R L).ker ↔ x ∈ LieAlgebra.center R L

Tactic:
← LieAlgebra.self_module_ker_eq_center,

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ x ∈ (ad R L).ker ↔ x ∈ LieModule.ker R L L
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case succ.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
⊢ (aeval x) P ^ 2 ^ (n + 1) ∣
    Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) ^ 2 * (aeval (P.newtonMap^[n] x)) P ^ 2

Tactic:
pow_succ,

Goal state after:
case succ.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
⊢ (aeval x) P ^ (2 ^ n * 2) ∣
    Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) ^ 2 * (aeval (P.newtonMap^[n] x)) P ^ 2
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_3.refine_2
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
⊢ ∀ (x : A) (y : L), ((bracket' R A L L) (x ⊗ₜ[R] y)) z₂ + ((bracket' R A L L) z₂) (x ⊗ₜ[R] y) = 0

Tactic:
intro a₁

Goal state after:
case refine_3.refine_2
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
a₁ : A
⊢ ∀ (y : L), ((bracket' R A L L) (a₁ ⊗ₜ[R] y)) z₂ + ((bracket' R A L L) z₂) (a₁ ⊗ₜ[R] y) = 0
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
n : ℕ
ih : derivedSeriesOfIdeal R L (n + 1) ⊤ = ⊤ ↔ derivedSeriesOfIdeal R L 1 ⊤ = ⊤
h : derivedSeriesOfIdeal R L 1 ⊤ = ⊤
⊢ ⁅derivedSeriesOfIdeal R L (n + 1) ⊤, derivedSeriesOfIdeal R L (n + 1) ⊤⁆ = ⊤

Tactic:
rwa [ih.mpr h]

Goal state after:
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✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
⊢ ∀ (x : A) (y_1 : L),
    ((bracket' R A L M) (x ⊗ₜ[R] y_1)) (((bracket' R A L M) y) z) =
      ((bracket' R A L M) (((bracket' R A L L) (x ⊗ₜ[R] y_1)) y)) z +
        ((bracket' R A L M) y) (((bracket' R A L M) (x ⊗ₜ[R] y_1)) z)

Tactic:
intro a₁

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
⊢ ∀ (y_1 : L),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] y_1)) (((bracket' R A L M) y) z) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] y_1)) y)) z +
        ((bracket' R A L M) y) (((bracket' R A L M) (a₁ ⊗ₜ[R] y_1)) z)
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 = ⊥}
⊢ derivedLengthOfIdeal R L I = k + 1 ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥ ∧ derivedSeriesOfIdeal R L k I ≠ ⊥

Tactic:
change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

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 = ⊥}
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
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✝¹⁶ : 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 : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L),
    (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_1) y) =
          ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y_1))
            ((TensorProduct.map f.toLinearMap ↑g) y) →
        (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x + y_1)) y) =
          ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x + y_1)))
            ((TensorProduct.map f.toLinearMap ↑g) y)

Tactic:
intro _ _
        refine y.induction_on (by simp) (fun _ _ h ↦ by simp [h]) (by simp_all)

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

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ derivedSeries R L 0 ≤ lowerCentralSeries R L L 0

Tactic:
rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]

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, lowerCentralSeries R L M k = ⊥

Tactic:
by
  obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L M
  rw [eq_bot_iff, ← hk]
  exact iInf_le _ _

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
x : L
m : M
k : ℕ
hk : ∀ (x : L), (toEnd R L M) x ^ k = 0
⊢ ((toEnd R L M) x ^ k) m = 0

Tactic:
by simp [hk x]

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 : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ nilpotencyLength L M = k + 1 ↔ lowerCentralSeries ℤ L M (k + 1) = ⊥ ∧ ¬lowerCentralSeries ℤ L M k = ⊥

Tactic:
change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

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
k : ℕ
aux : ∀ (k : ℕ), lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥
s : Set ℕ := {k | lowerCentralSeries ℤ L M k = ⊥}
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
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
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ K = adjoin F S

Tactic:
apply toSubalgebra_injective

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ K.toSubalgebra = (adjoin F S).toSubalgebra
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
S : Set E
L₁ L₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' : ∀ (x : ↥L₁.carrier), L₂.emb ((inclusion h₁₂) x) = L₁.emb x
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' : ∀ (x : ↥L₂.carrier), L₃.emb ((inclusion h₂₃) x) = L₂.emb x
x✝ : ↥L₁.carrier
⊢ L₂.emb ((inclusion h₁₂) x✝) = L₁.emb x✝

Tactic:
h₁₂'

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
S : Set E
L₁ L₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' : ∀ (x : ↥L₁.carrier), L₂.emb ((inclusion h₁₂) x) = L₁.emb x
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' : ∀ (x : ↥L₂.carrier), L₃.emb ((inclusion h₂₃) x) = L₂.emb x
x✝ : ↥L₁.carrier
⊢ L₁.emb x✝ = L₁.emb x✝
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
⊢ σ ((aeval a) p) = (fun k ↦ eval k p) '' σ a

Tactic:
refine Or.elim (le_or_gt (degree p) 0) (fun h => ?_) (map_polynomial_aeval_of_degree_pos a p)

Goal state after:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : (σ a).Nonempty
a✝ : Nontrivial A
h : p.degree ≤ 0
⊢ σ ((aeval a) p) = (fun k ↦ eval k p) '' σ a
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)
x : E
hx : x ∈ ⨆ i, f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ x1 ∈ (minpoly F x1).rootSet E

Tactic:
· rw [mem_rootSet_of_ne, minpoly.aeval]
    exact minpoly.ne_zero (isIntegral_iff.mp (Algebra.IsIntegral.isIntegral (⟨x1, hx1⟩ : f i)))

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
α : E
⊢ minpoly F ((algebraMap (↥F⟮α⟯) E) (AdjoinSimple.gen F α)) = minpoly F α

Tactic:
AdjoinSimple.algebraMap_gen

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ minpoly F α = minpoly F α