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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ I ≤ f.ker ↔ ∀ x ∈ I, f x = 0

Tactic:
by
  constructor <;> intro h x hx
  · specialize h hx; rw [mem_ker] at h; exact h
  · rw [mem_ker]; apply h x hx

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
⊢ ↑(map f I) = Submodule.map ↑f ↑I

Tactic:
map,

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : Function.Surjective ⇑f
J : LieIdeal R L' :=
  let __src := Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule;
  { toSubmodule := __src, lie_mem := ⋯ }
⊢ ↑(LieSubmodule.lieSpan R L' ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)) = Submodule.map ↑f ↑I
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L'
y : L
hy₂ : ↑f y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ f.ker
hy : z₁ + z₂ = y
⊢ f z₁ ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)

Tactic:
exact ⟨z₁, hz₁, rfl⟩

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

Goal state before:
pp: case mp
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
inst✝ : LieModule R L M
m : M
⊢ (∃ x n, ⁅↑x, ↑n⁆ = m) → ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m

pp: case mpr
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
inst✝ : LieModule R L M
m : M
⊢ (∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m) → ∃ x n, ⁅↑x, ↑n⁆ = m

Tactic:
· rintro ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩
    exact ⟨x, hx, n, hn, rfl⟩

Goal state after:
case mpr
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
inst✝ : LieModule R L M
m : M
⊢ (∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m) → ∃ x n, ⁅↑x, ↑n⁆ = m
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 : LieSubmodule R L M
⊢ N ≤ sSup ((fun x ↦ lieSpan R L {x}) '' ↑N)

Tactic:
← toSubmodule_le_toSubmodule,

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 : LieSubmodule R L M
⊢ ↑N ≤ ↑(sSup ((fun x ↦ lieSpan R L {x}) '' ↑N))
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
⊢ p ∈ RingHom.ker (Polynomial.aeval x) ↔ p ∈ A[X] ∙ minpoly A x

Tactic:
simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton,
    dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)]

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

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'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ = x
⊢ x ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)

Tactic:
rw [← hx]

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'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ = x
⊢ ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree

Tactic:
have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq

Goal state after:
case pos.refine_2
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
H : q.natDegree < orderOf σ
hs : ∑ x, q.coeff ↑x • (σ ^ ↑x).toLinearMap = 0
⊢ q = 0

Tactic:
simpa using Fintype.linearIndependent_iff.mp
      (((linearIndependent_algHom_toLinearMap' K L L).comp _ AlgEquiv.coe_toAlgHom_injective).comp _
        (Subtype.val_injective.comp ((finEquivPowers hσ).injective)))
      (q.coeff ∘ (↑)) hs ⟨_, H⟩

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
⊢ y ∈ Submodule.span R (Set.range fun i ↦ x ^ ↑i) ↔ ∃ f, f.natDegree < d ∧ y = (aeval x) f

Tactic:
rw [mem_span_pow']

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, f.degree < ↑d ∧ y = (aeval x) f) ↔ ∃ f, f.natDegree < d ∧ y = (aeval x) f
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr.e_a
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
⊢ ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x ∈ Ideal.span {pb.gen}

Tactic:
coe_basis

Goal state after:
case inr.e_a
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
⊢ ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • (fun i ↦ pb.gen ^ ↑i) x ∈ Ideal.span {pb.gen}
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ¬∀ (x : R), x * x ∣ 0 → IsUnit x

Tactic:
not_forall

Goal state after:
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ∃ x, ¬(x * x ∣ 0 → IsUnit x)
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r → ∀ (x : R), Irreducible x → ¬x * x ∣ r
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ 0
⊢ p * z ∣ p ^ 1

Tactic:
simp [isUnit_of_dvd_one (pow_zero y ▸ hy')]

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

Goal state before:
pp: case mpr.inr
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
hu : ¬IsUnit a
h0 : a ≠ 0
b : R
hib : Irreducible b
hdvd : b ∣ a
⊢ emultiplicity a x ≤ 1

Tactic:
apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)

Goal state after:
case mpr.inr
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
hu : ¬IsUnit a
h0 : a ≠ 0
b : R
hib : Irreducible b
hdvd : b ∣ a
⊢ emultiplicity b x ≤ 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : (∏ i ∈ s, (X - C (f i))).Separable
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
⊢ x = y

Tactic:
by
  classical
  by_contra hxy
  rw [← insert_erase hx, prod_insert (notMem_erase _ _), ←
    insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy), prod_insert (notMem_erase _ _), ←
    mul_assoc, hfxy, ← sq] at hfs
  cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p m n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ x = (iterateFrobeniusEquiv R p n) ((iterateFrobeniusEquiv R p n).symm x)

Tactic:
RingEquiv.apply_symm_apply

Goal state after:
R : Type u_1
p m n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ x = x
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : ℕ
hp : ExpChar K p
⊢ PerfectRing K p

Tactic:
refine PerfectRing.ofSurjective _ _ fun y ↦ ?_
  rcases hp with _ | hp
  · simp [frobenius]
  rw [← not_forall_not]
  apply mt (X_pow_sub_C_irreducible_of_prime hp)
  apply mt separable_of_irreducible
  simp [separable_def, isCoprime_zero_right, isUnit_iff_degree_eq_zero,
    derivative_X_pow, degree_X_pow_sub_C hp.pos, hp.ne_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

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

Tactic:
refine ⟨b.equivFun.symm v, ?_, b.equivFun.symm.map_ne_zero_iff.mpr hv_ne_zero⟩

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Free R M
f : M →ₗ[R] M
hf : LinearMap.det f = 0
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : Fin (finrank R M) → R
hv_ne_zero : v ≠ 0
hv_zero : (toMatrix b b) f *ᵥ v = 0
⊢ f (b.equivFun.symm v) = 0
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✝ : DecidableEq R
⊢ Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset ⊆ f.roots.toFinset

Tactic:
Finset.image_toFinset,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : DecidableEq R
⊢ (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots).toFinset ⊆ f.roots.toFinset
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)))
⊢ LinearMap.det (pi fun i ↦ f i ∘ₗ proj i) = ∏ i, LinearMap.det (f i)

Tactic:
← LinearMap.det_toMatrix B,

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)))
⊢ ((toMatrix B B) (pi fun i ↦ f i ∘ₗ proj i)).det = ∏ i, LinearMap.det (f i)
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
inst✝ : DecidableEq R
⊢ Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset = f.roots.toFinset

Tactic:
Finset.image_toFinset,

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
inst✝ : DecidableEq R
⊢ (Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots).toFinset = f.roots.toFinset
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : PerfectRing R p
inst✝ : DecidableEq R
⊢ Finset.image (⇑(frobenius R p)) ((expand R p) f).roots.toFinset = f.roots.toFinset

Tactic:
Finset.image_toFinset,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : PerfectRing R p
inst✝ : DecidableEq R
⊢ (Multiset.map (⇑(frobenius R p)) ((expand R p) f).roots).toFinset = f.roots.toFinset
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_3
E' : Type u_4
inst✝³ : Field E
inst✝² : Field E'
inst✝¹ : Algebra F E
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable F (f x)
x✝ : Algebra E E' := f.toAlgebra
this : IsScalarTower F E E'
⊢ IsSeparable F x

Tactic:
exact h.tower_bot

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
⊢ (lift i a h) (root f) = a

Tactic:
by rw [root, lift_mk, eval₂_X]

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
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ Associated (Polynomial.map (↑f.symm) q) p

Tactic:
have : (RingHomClass.toRingHom f.toRingEquiv.symm).comp (RingHomClass.toRingHom f) =
        .id S := by ext; exact f.symm_apply_apply _
      simpa [Polynomial.map_map, -RingEquiv.symm_mk, this]
        using! associated_map_map f.symm.toRingHom h.symm

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : ι → ι → R
⊢ det M = detRowAlternating M

Tactic:
det

Goal state after:
R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : ι → ι → R
⊢ detRowAlternating M = detRowAlternating M
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
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
i : ℕ
hk : f ^ i = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i_1, ∃ (_ : i_1 ≤ i), (f ^ i_1) x = x_1}
hi : i ≤ i
⊢ ∃ (_ : i ≤ i), (f ^ i) x = f ((f ^ i) x)

Tactic:
simp [hk]

Goal state after:
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case e'_4
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 (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) =
    0

Tactic:
have : IsUnit (aeval (P.newtonMap^[n] x) <| derivative P) :=
        isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub h' <|
        isNilpotent_iterate_newtonMap_sub_of_isNilpotent h n

Goal state after:
case e'_4
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
this : IsUnit ((aeval (P.newtonMap^[n] x)) (derivative 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) =
    0
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p a b c d x y : R
inst✝ : GCDMonoid R
h1 : p ∣ a * x + b * y
h2 : p ∣ c * x + d * y
⊢ p ∣ (a * d - b * c) * gcd x y

Tactic:
by
  rw [← (gcd_mul_left' (a * d - b * c) x y).dvd_iff_dvd_right]
  exact (dvd_gcd_iff _ _ _).2 ⟨dvd_mul_sub_mul_mul_left_of_dvd h1 h2,
    dvd_mul_sub_mul_mul_right_of_dvd h1 h2⟩

Goal state after:
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:
by
  intro m hm
  rw [mem_normalizer]
  exact fun x => N.lie_mem hm

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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
inst✝ : LieModule R L₂ M₂
hf_surj : Surjective ⇑f
hg_surj : Surjective ⇑g
k : ℕ
ih : ↑(lowerCentralSeries R L₂ M₂ k) ≤ Submodule.map g ↑(lowerCentralSeries R L M k)
this :
  {m | ∃ x, ∃ n ∈ lowerCentralSeries R L M k, ⁅x, g n⁆ = m} ⊆
    ⇑g '' {m | ∃ x, ∃ n ∈ lowerCentralSeries R L M k, ⁅x, n⁆ = m}
⊢ ↑(lowerCentralSeries R L₂ M₂ (k + 1)) ≤ Submodule.map g ↑(lowerCentralSeries R L M (k + 1))

Tactic:
by
      simp only [← LieSubmodule.mem_toSubmodule] at this
      simp_rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span',
        Submodule.map_span, LieSubmodule.mem_top, true_and, ← LieSubmodule.mem_toSubmodule]
      refine Submodule.span_mono (Set.Subset.trans ?_ this)
      rintro m₁ ⟨x, n, hn, rfl⟩
      obtain ⟨n', hn', rfl⟩ := ih hn
      exact ⟨x, n', hn', rfl⟩

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

Goal state before:
pp: case h
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'
h₁ : ∃ k, lowerCentralSeries R L L k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ⇑f
k : ℕ
hk : lowerCentralSeries R L L k = ⊥
⊢ lowerCentralSeries R L' L' k = ⊥

Tactic:
← LieIdeal.lowerCentralSeries_map_eq k h₂,

Goal state after:
case h
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'
h₁ : ∃ k, lowerCentralSeries R L L k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ⇑f
k : ℕ
hk : lowerCentralSeries R L L k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) = ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

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
inst✝ : IsNilpotent L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k = ⊥

Tactic:
simp [hk]

Goal state after:
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
inst✝⁵ : Field F
E : Type u_3
inst✝⁴ : Field E
inst✝³ : Algebra F E
M : Type u_5
N : Type u_6
inst✝² : Field N
inst✝¹ : Field M
inst✝ : Algebra M N
h : ∀ (x : E), IsIntegral F x ∧ (map (algebraMap F E) (minpoly F x)).Splits
f : F ≃+* M
g : E ≃+* N
hcomp : (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E)
this : Normal F E
x : N
⊢ (map (↑g) (map (algebraMap F E) (minpoly F (g.symm x)))).Splits

Tactic:
exact (h (g.symm x)).2.map _

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case inr
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
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x g = 0
⊢ f = 1 ∨ g = 1

Tactic:
left
    have hg3 : g = minpoly G F x :=
      Polynomial.eq_of_monic_of_associated hg (monic G F x)
        (associated_of_dvd_dvd hg2 <| @of_eval₂ G _ F _ _ _ x g this)
    rwa [← one_mul (minpoly G F x), hg3, mul_left_inj' (monic G F x).ne_zero] at hfg

Goal state after:
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
K : IntermediateField F E
S : Set E
⊢ adjoin F ↑K ⊔ adjoin F S = K ⊔ adjoin F S

Tactic:
adjoin_self

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
⊢ K ⊔ adjoin F S = K ⊔ adjoin F S
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
ι : Sort u_3
f : ι → IntermediateField F E
⊢ ⨆ i, f i = ⨆ i, adjoin F ↑(f i)

Tactic:
adjoin_self

Goal state after: