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
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
⊢ Module.Finite R M

Tactic:
by
  by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
  · rcases H with ⟨s, ⟨hs⟩⟩
    exact Module.Finite.of_basis hs
  · classical simp [LinearMap.coe_det, H] at hf

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
s : R
⊢ count (s ^ p ^ n) (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots) ≤
    count (s ^ p ^ n) (p ^ n • f.roots)

Tactic:
simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
      count_eq_card_filter_eq]

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
s : R
⊢ (filter (fun a ↦ s ^ p ^ n = (iterateFrobenius R p n) a) ((expand R (p ^ n)) f).roots).card ≤
    (filter (fun x ↦ s = x) ((expand R (p ^ n)) f).roots).card
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots ≤ p ^ n • f.roots

Tactic:
by
  classical
  refine le_iff_count.2 fun r ↦ ?_
  by_cases h : ∃ s, r = s ^ p ^ n
  · obtain ⟨s, rfl⟩ := h
    simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
      count_eq_card_filter_eq]
    exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)
  convert! Nat.zero_le _
  simp_rw [count_map, card_eq_zero]
  exact ext' fun t ↦ count_zero t ▸ count_filter_of_neg fun h' ↦ h ⟨t, h'⟩

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr
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
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ n₁ = n₁ + 0 ∧ (expand F (p ^ 0)) g₂ = g₂

Tactic:
add_zero,

Goal state after:
case inr
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
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
⊢ n₁ = n₁ ∧ (expand F (p ^ 0)) g₂ = g₂
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ p ^ n •
      Multiset.map (fun x ↦ (iterateFrobeniusEquiv R p n) x)
        (Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots) =
    p ^ n • f.roots

Tactic:
Multiset.map_map,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ p ^ n • Multiset.map ((fun x ↦ (iterateFrobeniusEquiv R p n) x) ∘ ⇑(iterateFrobeniusEquiv R p n).symm) f.roots =
    p ^ n • f.roots
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a

Tactic:
by_cases h : annIdealGenerator 𝕜 a = 0
  · rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]
  · rw [annIdealGenerator, Ideal.span_singleton_mul_right_unit, Ideal.span_singleton_generator]
    apply Polynomial.isUnit_C.mpr
    apply IsUnit.mk0
    apply inv_eq_zero.not.mpr
    apply Polynomial.leadingCoeff_eq_zero.not.mpr
    apply (mul_ne_zero_iff.mp h).1

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)).det = ∏ x, ((toMatrix b b) (f x)).det

Tactic:
have : ((LinearMap.toMatrix B B) (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)) =
      Matrix.blockDiagonal (fun i ↦ LinearMap.toMatrix b b (f i)) := by
    ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
    unfold B
    simp_rw [LinearMap.toMatrix_apply', Matrix.blockDiagonal_apply, Basis.coe_reindex,
      Function.comp_apply, Basis.repr_reindex_apply, Equiv.symm_trans_apply, Equiv.prodComm_symm,
      Equiv.prodComm_apply, Equiv.sigmaEquivProd_symm_apply, Prod.swap_prod_mk, Pi.basis_apply,
      Pi.basis_repr, LinearMap.pi_apply, LinearMap.coe_comp, Function.comp_apply,
      LinearMap.toMatrix_apply', LinearMap.coe_proj, Function.eval, Pi.single_apply]
    split_ifs with h
    · rw [h]
    · simp only [map_zero, Finsupp.coe_zero, Pi.zero_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)))
this : (toMatrix B B) (pi fun i ↦ f i ∘ₗ proj i) = blockDiagonal fun i ↦ (toMatrix b b) (f i)
⊢ ((toMatrix B B) (pi fun i ↦ f i ∘ₗ proj i)).det = ∏ x, ((toMatrix b b) (f x)).det
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
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 ι
⊢ IsUnit ((toMatrix b b) f).det

Tactic:
det_toMatrix b

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
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 ι
⊢ IsUnit (LinearMap.det f)
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
f g : R[X]
inst✝³ : CommRing S
i✝ : R →+* S
a : S
h✝ : eval₂ i✝ a f = 0
inst✝² : CommRing T
inst✝¹ : Algebra S R
inst✝ : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i) x p = 0
r : S
⊢ (↑↑(lift i.toRingHom x h)).toFun ((algebraMap S (AdjoinRoot p)) r) = (algebraMap S T) r

Tactic:
by simp [lift_of h, AdjoinRoot.algebraMap_eq']

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
L : Type u_6
F : Type u_7
inst✝³ : Field F
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ x ∈ f.aroots L + 0 ↔ (Equiv.refl L) x ∈ f.aroots L

pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
L : Type u_6
F : Type u_7
inst✝³ : Field F
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ f * C f.leadingCoeff⁻¹ ≠ 0

Tactic:
add_zero,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
L : Type u_6
F : Type u_7
inst✝³ : Field F
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ x ∈ f.aroots L ↔ (Equiv.refl L) x ∈ f.aroots L

R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
L : Type u_6
F : Type u_7
inst✝³ : Field F
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ f * C f.leadingCoeff⁻¹ ≠ 0
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
this : ∑ i ∈ Ico k (nilpotencyClass a), ((↑i !)⁻¹ • a ^ i) • m = 0
⊢ ∑ k ∈ range k, ((↑k !)⁻¹ • a ^ k) • m + 0 = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
add_zero,

Goal state after:
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
this : ∑ i ∈ Ico k (nilpotencyClass a), ((↑i !)⁻¹ • a ^ i) • m = 0
⊢ ∑ k ∈ range k, ((↑k !)⁻¹ • a ^ k) • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m
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
D1 D2 : LieDerivation R L L
a b : L
⊢ ⁅↑D1, ↑D2⁆ ⁅a, b⁆ = ⁅a, ⁅↑D1, ↑D2⁆ b⁆ - ⁅b, ⁅↑D1, ↑D2⁆ a⁆

Tactic:
simp only [Ring.lie_def, apply_lie_eq_add, coeFn_coe,
      LinearMap.sub_apply, Module.End.mul_apply, map_add, sub_lie, lie_sub, ← lie_skew b]
    abel

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
D : LieDerivation R L M
⊢ ⁅x, ↑D⁆ = ↑⁅x, D⁆

Tactic:
by
  ext; simp

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst✝¹⁷ : LieRing L
inst✝¹⁶ : LieAlgebra R L
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : LieRingModule L M
inst✝¹² : LieModule R L M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
x : L
t : M ⊗[R] N
⊢ ∀ (x_1 : M) (y : N), (TensorProduct.map ↑f ↑g) ⁅x, x_1 ⊗ₜ[R] y⁆ = ⁅x, (TensorProduct.map ↑f ↑g) (x_1 ⊗ₜ[R] y)⁆

Tactic:
intro m

Goal state after:
case refine_2
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst✝¹⁷ : LieRing L
inst✝¹⁶ : LieAlgebra R L
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : LieRingModule L M
inst✝¹² : LieModule R L M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
x : L
t : M ⊗[R] N
m : M
⊢ ∀ (y : N), (TensorProduct.map ↑f ↑g) ⁅x, m ⊗ₜ[R] y⁆ = ⁅x, (TensorProduct.map ↑f ↑g) (m ⊗ₜ[R] y)⁆
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
I : LieIdeal R L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
k : ℕ
ih : derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A I) = LieSubmodule.baseChange A (D k I)
⊢ derivedSeriesOfIdeal A (A ⊗[R] L) (k + 1) (LieSubmodule.baseChange A I) = LieSubmodule.baseChange A (D (k + 1) I)

Tactic:
simp only [derivedSeriesOfIdeal_succ, ih, LieSubmodule.lie_baseChange]

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
⊢ ((bracket' R A L L) z₂) z₁ + (((bracket' R A L L) z₁) z₂ + 0) = 0

Tactic:
add_zero,

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
⊢ ((bracket' R A L L) z₂) z₁ + ((bracket' R A L L) z₁) z₂ = 0
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
N : LieSubmodule R L M
⊢ N ≤ N.normalizer

Tactic:
intro m

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
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
N : LieSubmodule R L M
m : M
⊢ m ∈ N → m ∈ N.normalizer
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
⊢ N₁.normalizer ≤ N₂.normalizer

Tactic:
intro m

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
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
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
⊢ m ∈ N₁.normalizer → m ∈ N₂.normalizer
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : 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✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N : LieSubmodule R L M
f : M' →ₗ⁅R,L⁆ M
⊢ comap f N.normalizer = (comap f N).normalizer

Tactic:
by
  ext; simp

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
x' y' z' : L ⧸ I
⊢ ⁅x', y' + z'⁆ = ⁅x', y'⁆ + ⁅x', z'⁆

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

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

Goal state before:
pp: case refine_1
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 : A) (y_1 : L),
    (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x ⊗ₜ[R] y_1)) y) =
      ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x ⊗ₜ[R] y_1)))
        ((TensorProduct.map f.toLinearMap ↑g) y)

Tactic:
intro _ _
        refine y.induction_on (by simp) (fun _ _ ↦ by simp) (fun _ _ h1 h2 ↦ by simp [h1, h2])

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✝⁷ : 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
x : L
⊢ (toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x) = LinearMap.baseChange A ((toEnd R L M) x)

Tactic:
by
  ext; simp

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✝ : IsNilpotent L M
h : ¬IsTrivial L M
⊢ lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1

Tactic:
by
  rw [lowerCentralSeriesLast]
  replace h : 1 < nilpotencyLength L M := by
    by_contra contra
    have := isTrivial_of_nilpotencyLength_le_one L M (not_lt.mp contra)
    contradiction
  rcases hk : nilpotencyLength L M with - | k <;> rw [hk] at h
  · contradiction
  · exact antitone_lowerCentralSeries _ _ _ (Nat.le_of_lt_succ h)

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
h : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
⊢ LieModule.IsNilpotent L M

Tactic:
← isNilpotent_range_toEnd_iff 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
h : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
⊢ LieModule.IsNilpotent (↥(toEnd R L M).range) M
Module: Mathlib.FieldTheory.Finiteness

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Fintype V
⊢ Fintype.card V = Fintype.card K ^ finrank K V

Tactic:
let b := IsNoetherian.finsetBasis K V
  rw [Module.card_fintype b, ← Module.finrank_eq_card_basis b]

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

Goal state before:
pp: case mpr
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₂
inst✝ : LieModule R L₂ M₂
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
h : LieModule.IsNilpotent L₂ M₂
hg : Surjective ⇑↑g.symm
x : L₂
m : M₂
⊢ g.symm ⁅f (f.symm x), g (g.symm m)⁆ = g.symm ⁅x, m⁆

Tactic:
f.apply_symm_apply,

Goal state after:
case mpr
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₂
inst✝ : LieModule R L₂ M₂
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
h : LieModule.IsNilpotent L₂ M₂
hg : Surjective ⇑↑g.symm
x : L₂
m : M₂
⊢ g.symm ⁅x, g (g.symm m)⁆ = g.symm ⁅x, m⁆
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case a
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[↥(subfield G F)] F) ≤ Fintype.card G

Tactic:
· rw [← finrank_eq_card G F]
      exact LE.le.trans_eq (finrank_algHom _ F) (finrank_linearMap_self _ _ _)

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ Subalgebra.restrictScalars F (Algebra.adjoin K ↑(Polynomial.map (algebraMap F L) f).roots.toFinset) =
    Subalgebra.restrictScalars F ⊤

Tactic:
Subalgebra.restrictScalars_top,

Goal state after:
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : F[X]
inst✝ : IsSplittingField F L f
⊢ Subalgebra.restrictScalars F (Algebra.adjoin K ↑(Polynomial.map (algebraMap F L) f).roots.toFinset) = ⊤
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
g : (map (algebraMap K L) (minpoly K x)).Splits
⊢ (map (algebraMap K L) (minpoly K (-x))).Splits

Tactic:
minpoly.neg,

Goal state after:
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
g : (map (algebraMap K L) (minpoly K x)).Splits
⊢ (map (algebraMap K L) ((-1) ^ (minpoly K x).natDegree * (minpoly K x).comp (-X))).Splits
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 T : Set E
⊢ restrictScalars F (adjoin (↥(adjoin F S)) T) = adjoin F (S ∪ T)

Tactic:
rw [SetLike.ext'_iff]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : Set E
⊢ ↑(restrictScalars F (adjoin (↥(adjoin F S)) T)) = ↑(adjoin F (S ∪ T))
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field F'
inst✝⁴ : Field E
inst✝³ : Algebra F F'
inst✝² : Algebra F E
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : IsAlgClosed F'
h : finrank F F' = 2
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
by
  have emb : E →ₐ[F] F' := lift
  have e := AlgEquiv.ofInjectiveField emb
  have := Subalgebra.isSimpleOrder_of_finrank h
  obtain h | h := IsSimpleOrder.eq_bot_or_eq_top emb.range <;> rw [h] at e
  exacts [.inl ⟨e.trans <| Algebra.botEquiv ..⟩, .inr ⟨e.trans Subalgebra.topEquiv⟩]

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
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
this : ∀ μ' ∈ m.support, g (m μ') = if μ' = μ then g (m μ) else 0
⊢ (m.sum fun μ' x ↦ if μ' = μ then g (m μ) else 0) = g (m μ)

Tactic:
Finsupp.sum_ite_eq',

Goal state after:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
this : ∀ μ' ∈ m.support, g (m μ') = if μ' = μ then g (m μ) else 0
⊢ (if μ ∈ m.support then g (m μ) else 0) = g (m μ)