mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : (aeval x) (∑ x_1, (monomial ↑x_1) (g x_1)) = 0
⊢ (∑ x_1, C (g x_1) * X ^ ↑x_1).degree < (minpoly K x).degree

Tactic:
exact (degree_eq_natDegree <| minpoly.ne_zero h).symm ▸ degree_sum_fin_lt _

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
⊢ pb.equivOfRoot (pb.map e) h₁ h₂ = e

Tactic:
ext x

Goal state after:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
x : S
⊢ (pb.equivOfRoot (pb.map e) h₁ h₂) x = e x
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
m : R
hm : Squarefree m
⊢ m ≠ 0

Tactic:
by
  rintro rfl
  exact not_squarefree_zero hm

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x * x ∣ x ^ n

Tactic:
rw [← sq]

Goal state after:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x ^ 2 ∣ x ^ n
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
⊢ d ∣ y

Tactic:
obtain ⟨c, hc⟩ : a ∣ d := ha.isRadical 2 d ⟨b, by rw [sq, eq]⟩

Goal state after:
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
c : R
hc : d = a * c
⊢ d ∣ y
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ q * q ∣ p

Tactic:
rw [← sq]

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ q ^ 2 ∣ p
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : p = 0
⊢ rootMultiplicity x p ≤ 1

Tactic:
simp [hp]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1

Tactic:
by
  classical
  by_cases hp : p = 0
  · simp [hp]
  rw [rootMultiplicity_eq_multiplicity, if_neg hp, ← Nat.cast_le (α := ℕ∞),
    Nat.cast_one, ← (finiteMultiplicity_X_sub_C x hp).emultiplicity_eq_multiplicity]
  apply emultiplicity_le_one_of_separable (not_isUnit_X_sub_C _) hsep

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h.inr.zero
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬IsUnit (f.coeff 0)
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
ih : ∀ m < 0, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f = C (f.coeff 0)
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
isUnit_iff_ne_zero,

Goal state after:
case h.inr.zero
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.coeff 0 ≠ 0
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
ih : ∀ m < 0, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f = C (f.coeff 0)
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
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
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ¬∃ s, Nonempty (Basis (↥s) A M)
H' : ¬∃ t, Nonempty (Basis (↥t) A N)
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Tactic:
simp only [coe_det, H, H', MonoidHom.one_apply, dif_neg, not_false_eq_true]

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : PerfectField K
f : L[X]
hf : Irreducible f
⊢ f.Separable

Tactic:
obtain ⟨_, _, hi, h⟩ := hf.exists_dvd_monic_irreducible_of_isIntegral (K := K)

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
inst✝ : PerfectField K
f : L[X]
hf : Irreducible f
w✝ : K[X]
left✝ : w✝.Monic
hi : Irreducible w✝
h : f ∣ map (algebraMap K L) w✝
⊢ f.Separable
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Ideal.span {p} = Ideal.span {annIdealGenerator 𝕜 a}
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p

Tactic:
Ideal.span_singleton_eq_span_singleton

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
x✝ : 𝕜[X]
⊢ x✝ ∈ annIdeal 𝕜 f ↔ x✝ ∈ Module.annihilator 𝕜[X] (Module.AEval' f)

Tactic:
rw [mem_annIdeal_iff_aeval_eq_zero, DFunLike.ext_iff, Module.mem_annihilator]

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
x✝ : 𝕜[X]
⊢ (∀ (x : M), ((aeval f) x✝) x = 0 x) ↔ ∀ (m : Module.AEval' f), x✝ • m = 0
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
⊢ ∃ s, map i f = C (i f.leadingCoeff) * ∏ a ∈ s, (X - C a)

Tactic:
classical
  obtain ⟨s, h⟩ := splits_iff_exists_multiset.1 sp
  use s.toFinset
  rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq, leadingCoeff_map]
  apply nodup_of_separable_prod
  apply Separable.of_mul_right
  rw [← h]
  exact sep.map

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: 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)
⊢ f.comp (Ideal.Quotient.mk (span {p})) = g.comp (Ideal.Quotient.mk (span {p}))

Tactic:
ext x

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

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)
⊢ (f.comp (Ideal.Quotient.mk (span {p}))) X = (g.comp (Ideal.Quotient.mk (span {p}))) X
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: A₁ : Type u_1
B₁ : Type u_2
A₂ : Type u_3
B₂ : Type u_4
inst✝⁵ : Field A₁
inst✝⁴ : Ring B₁
inst✝³ : Field A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x✝ : Algebra.IsSeparable A₂ B₂
⊢ (algebraMap A₁ B₁).comp ↑e₁.symm = (↑e₂.symm).comp (algebraMap A₂ B₂)

Tactic:
ext x

Goal state after:
A₁ : Type u_1
B₁ : Type u_2
A₂ : Type u_3
B₂ : Type u_4
inst✝⁵ : Field A₁
inst✝⁴ : Ring B₁
inst✝³ : Field A₂
inst✝² : Ring B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x✝ : Algebra.IsSeparable A₂ B₂
x : A₂
⊢ ((algebraMap A₁ B₁).comp ↑e₁.symm) x = ((↑e₂.symm).comp (algebraMap A₂ B₂)) x
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 ι
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit ((toMatrix v v') f).det
⊢ ↑(ofIsUnitDet h) = f

Tactic:
ext x

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

Tactic:
by
  by_cases hR : Nontrivial R
  · let ⟨ι, b⟩ := (Module.Free.exists_basis R M).some
    have : Finite ι := Module.Finite.finite_basis b
    have : Fintype ι := Fintype.ofFinite ι
    have : DecidableEq ι := Classical.typeDecidableEq ι
    exact LinearEquiv.ofIsUnitDet (v := b) (v' := b) (f := f) (by rwa [det_toMatrix b])
  · exact 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
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
this : Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
⊢ f = f' ∘ₗ ↑e

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
this : Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
x : M
⊢ f x = (f' ∘ₗ ↑e) x
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
g : R[X]
hg : g.Monic
f✝ : AdjoinRoot g
f : R[X]
⊢ g ∣ g * (f /ₘ g)

Tactic:
exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
⊢ f = 0

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
⊢ f x = 0 x
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
this : ∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p
⊢ (f - (algebraMap R (End R M)) μ).IsFinitelySemisimple ↔ f.IsFinitelySemisimple

Tactic:
by
    simp_rw [isFinitelySemisimple_iff, mem_invtSubmodule, this]

Goal state after:
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 y z : L
⊢ -(⁅⁅z, x⁆, y⁆ + ⁅x, ⁅z, y⁆⁆) = -⁅-⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆

Tactic:
neg_lie,

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : L
⊢ -(⁅⁅z, x⁆, y⁆ + ⁅x, ⁅z, y⁆⁆) = - -⁅⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆
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 y z : L
⊢ -(⁅⁅z, x⁆, y⁆ + ⁅x, ⁅z, y⁆⁆) = - -⁅⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆

Tactic:
neg_lie,

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

Tactic:
ext x

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 ∈ LieAlgebra.center R L
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case h
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)
s₁ :
  ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i =
    ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
⊢ {ij ∈ R2N ×ˢ R2N | ij.1 ≤ N ∧ ij.2 ≤ N} = RN ×ˢ RN

Tactic:
ext x

Goal state after:
case h
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)
s₁ :
  ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i =
    ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
x : ℕ × ℕ
⊢ x ∈ {ij ∈ R2N ×ˢ R2N | ij.1 ≤ N ∧ ij.2 ≤ N} ↔ x ∈ RN ×ˢ RN
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ idealizer I = normalizer I

Tactic:
ext x

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ idealizer I ↔ x ∈ normalizer I
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
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
⊢ (∃ k, derivedSeries A (A ⊗[R] L) k = ⊥) → IsSolvable L

Tactic:
isSolvable_iff R

Goal state after:
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
⊢ (∃ k, derivedSeries A (A ⊗[R] L) k = ⊥) → ∃ k, derivedSeries R L k = ⊥
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : IsSolvable L
h : Injective ⇑f
⊢ IsSolvable L'

Tactic:
isSolvable_iff R

Goal state after:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
⊢ ∃ k, derivedSeries R L' k = ⊥
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : IsSolvable L'
h : Surjective ⇑f
⊢ IsSolvable L

Tactic:
isSolvable_iff R

Goal state after:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
⊢ ∃ k, derivedSeries R L k = ⊥
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 : ℕ
⊢ derivedLengthOfIdeal R L I = k + 1 ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥ ∧ derivedSeriesOfIdeal R L k I ≠ ⊥

Tactic:
let s := { k | derivedSeriesOfIdeal R L k I = ⊥ }

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 = ⊥}
⊢ derivedLengthOfIdeal R L I = k + 1 ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥ ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
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
inst✝ : IsSolvable ↥I
⊢ derivedLengthOfIdeal R L I = 0 ↔ I = ⊥

Tactic:
let s := { k | derivedSeriesOfIdeal R L k I = ⊥ }

Goal state after:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : IsSolvable ↥I
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLengthOfIdeal R L I = 0 ↔ I = ⊥
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✝⁷ : 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
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
y z : A ⊗[R] L
hy : ⁅y, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N
hz : ⁅z, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N
⊢ ⁅y + z, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N

Tactic:
rw [add_lie]
        exact ((N : Submodule R M).baseChange A).add_mem hy hz

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

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
⊢ (fun x ↦ ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x) = fun x ↦ ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x

Tactic:
ext x

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
x : L ⧸ I
⊢ (∃ x_1 n, ⁅↑x_1, ↑n⁆ = x) ↔ ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x
Module: Mathlib.FieldTheory.IntermediateField.Algebraic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional K ↥E
h_le : F ≤ E
h : F = E
⊢ finrank K ↥F = finrank K ↥E

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Algebraic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
h_le : F ≤ E
h : F = E
⊢ finrank (↥F) L = finrank (↥E) L

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
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:
ext x

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
x : F
| g • l x * (toFun G F) x g'
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
⊢ f ∣ f * g

Tactic:
exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
⊢ finrank (↥(subfield G F)) F ≤ Fintype.card G

Tactic:
rw [← @Nat.cast_le Cardinal, finrank_eq_rank]
  apply rank_le_card

Goal state after:
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
⊢ ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'

Tactic:
ext x

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
x : E
⊢ (algebraMap E K) x = (⇑(algebraMap (↥E') K) ∘ ⇑i') x
Module: Mathlib.RingTheory.Adjoin.Dimension

Goal state before:
pp: R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : Cardinal.aleph0 ≤ Module.rank R ↥A
this : Module.rank R ↥(toSubmodule A) ≤ Module.rank R ↥(toSubmodule (A ⊔ B))
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
rw [show finrank R A = 0 from Cardinal.toNat_apply_of_aleph0_le hA,
    show finrank R ↥(A ⊔ B) = 0 from Cardinal.toNat_apply_of_aleph0_le (hA.trans this), zero_mul]

Goal state after: