mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ (f * g).Separable

Tactic:
rw [separable_def, derivative_mul]
  exact
    ((hf.mul_right h).add_mul_left_right _).mul_left ((h.symm.mul_right hg).mul_add_right_right _)

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : Nat.Prime p
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | _ N ih
   =>  _ 

Goal state after:
case h
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih : ∀ m < N, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case mpr
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
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : f.ker ≠ ⊥
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : M
left✝ : v ∈ f.ker
hv_ne_zero : v ≠ 0
⊢ LinearMap.det f = 0

Tactic:
rw [← det_toMatrix b, ← Matrix.exists_mulVec_eq_zero_iff]

Goal state after:
case mpr
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
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : f.ker ≠ ⊥
b : Basis (Fin (finrank R M)) R M := finBasis R M
v : M
left✝ : v ∈ f.ker
hv_ne_zero : v ≠ 0
⊢ ∃ v, v ≠ 0 ∧ (toMatrix b b) f *ᵥ v = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : 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₂ : ι
h : i₂ = j₂
⊢ (b.repr ((f i₂) (b j₁))) i₁ = (b.repr ((f i₂) (b j₁))) i₁

Tactic:
rw [h]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

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

Tactic:
simp only [Polynomial.aeval_C, Polynomial.map_C, mk_C]
    rw [IsScalarTower.algebraMap_apply R S]
    simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ (aeval (root f)) f = 0

Tactic:
aeval_eq,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ (mk f) f = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_1
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ (aeval (root f)) f * (aeval (root f)) (C f.leadingCoeff⁻¹) = 0

Tactic:
aeval_eq,

Goal state after:
case refine_1
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ (mk f) f * (aeval (root f)) (C f.leadingCoeff⁻¹) = 0
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✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det fun i j ↦ ((e.unitsSMul w).repr (f j)) i) = ↑(∏ i, w i)⁻¹ • Matrix.det fun i j ↦ (e.repr (f j)) i

Tactic:
simp only [e.repr_unitsSMul]

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✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det fun i j ↦ (w i)⁻¹ • (e.repr (f j)) i) = ↑(∏ i, w i)⁻¹ • Matrix.det fun i j ↦ (e.repr (f j)) i
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: K : Type u_5
inst✝ : Field K
f : K[X]
hf : f.Monic
hf' : f ≠ 0
⊢ minpoly K (powerBasis hf').gen = f

Tactic:
minpoly_powerBasis_gen hf',

Goal state after:
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f.Monic
hf' : f ≠ 0
⊢ f * C f.leadingCoeff⁻¹ = f
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
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ a ∈ ((Algebra.lsmul R R M) f).invtSubmodule,
      a ≤ p → ∃ a_2 ≤ p, (∃ (_ : a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule), a ⊓ a_2 = ⊥) ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p

Tactic:
exists_prop,

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
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ a ∈ ((Algebra.lsmul R R M) f).invtSubmodule,
      a ≤ p → ∃ a_2 ≤ p, (a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule ∧ a ⊓ a_2 = ⊥) ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p
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
g : R[X]
pb : PowerBasis R S
h₁ : (aeval (root g)) (minpoly R pb.gen) = 0
h₂ : (aeval pb.gen) g = 0
a✝ : Nontrivial S
f : R[X]
_hf : f.natDegree < pb.dim
⊢ (liftAlgHom g (Algebra.ofId R S) pb.gen h₂) ((aeval (root g)) f) = (aeval pb.gen) f

Tactic:
aeval_eq,

Goal state after:
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
g : R[X]
pb : PowerBasis R S
h₁ : (aeval (root g)) (minpoly R pb.gen) = 0
h₂ : (aeval pb.gen) g = 0
a✝ : Nontrivial S
f : R[X]
_hf : f.natDegree < pb.dim
⊢ (liftAlgHom g (Algebra.ofId R S) pb.gen h₂) ((mk g) f) = (aeval pb.gen) 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
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : (aeval (root g)) (minpoly R pb.gen) = 0
h₂ : (aeval pb.gen) g = 0
a✝ : Nontrivial S
f : R[X]
_hf : f.natDegree < pb.dim
⊢ (liftAlgHom g (Algebra.ofId R S) pb.gen h₂) ((pb.lift (root g) h₁) ((aeval pb.gen) f)) = (aeval pb.gen) f

Tactic:
rw [pb.lift_aeval, aeval_eq, liftAlgHom_mk, Polynomial.aeval_def, Algebra.toRingHom_ofId]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_2
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯).comp
      (liftAlgHom q (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
        (1 ⊗ₜ[R] root p) ⋯) =
    AlgHom.id T (AdjoinRoot q)

Tactic:
ext
    · simp [Algebra.ofId_apply]
    simp

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 g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁴ : Module.Finite K R
this✝³ : Module.Finite R S
this✝² : Module.Finite K S
this✝¹ : IsArtinianRing R
this✝ : IsReduced R
this : IsReduced S
φ : S →ₐ[K] End K M :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
x : End K M
⊢ x ∈ {f, g} → x ∈ ↑φ.range

Tactic:
by
    rintro (hx | hx) <;> rw [hx]
    · exact ⟨AdjoinRoot.of _ (AdjoinRoot.root _), (eval₂_C _ _).trans (aeval_X f)⟩
    · exact ⟨AdjoinRoot.root _, eval₂_X _ _⟩

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
⊢ x ^ m ∣ (x + y) ^ p

Tactic:
h_comm.add_pow'

Goal state after:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
⊢ x ^ m ∣ ∑ m ∈ Finset.antidiagonal p, p.choose m.1 • (x ^ m.1 * y ^ m.2)
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ x ^ m ∣ y ^ p

Tactic:
rw [← sub_add_cancel y x]
  apply (h_comm.symm.sub_left rfl).pow_dvd_add_pow_of_pow_eq_zero_left hp _
  rw [← neg_sub x y, neg_pow, h, mul_zero]

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 : L ⧸ I
x₁ x₂ y₁ y₂ : L
h₁ : x₁ - y₁ ∈ ↑I
h₂ : x₂ - y₂ ∈ ↑I
h : ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ = ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆
⊢ ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ ∈ ↑I

Tactic:
rw [h]

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
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y : L ⧸ I
x₁ x₂ y₁ y₂ : L
h₁ : x₁ - y₁ ∈ ↑I
h₂ : x₂ - y₂ ∈ ↑I
h : ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ = ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆
⊢ ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆ ∈ ↑I
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case add
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x y z : L
hy₁ : y ∈ Submodule.span R₁ S
hz₁ : z ∈ Submodule.span R₁ S
hy₂ : y ∈ Submodule.span R₂ S
hz₂ : z ∈ Submodule.span R₂ S
⊢ y + z ∈ Submodule.span R₂ S

Tactic:
exact Submodule.add_mem _ hy₂ hz₂

Goal state after:
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
H : LieSubalgebra R L
x y z : L
hx : x ∈ H.normalizer
hy : y ∈ R ∙ x ⊔ H.toSubmodule
hz : z ∈ R ∙ x ⊔ H.toSubmodule
⊢ ⁅y, z⁆ ∈ R ∙ x ⊔ H.toSubmodule

Tactic:
rw [Submodule.mem_sup] at hy hz
  obtain ⟨u₁, hu₁, v, hv : v ∈ H, rfl⟩ := hy
  obtain ⟨u₂, hu₂, w, hw : w ∈ H, rfl⟩ := hz
  obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hu₁
  obtain ⟨s, rfl⟩ := Submodule.mem_span_singleton.mp hu₂
  apply Submodule.mem_sup_right
  simp only [LieSubalgebra.mem_toSubmodule, smul_lie, add_lie, zero_add, lie_add, smul_zero,
    lie_smul, lie_self]
  refine H.add_mem (H.smul_mem s ?_) (H.add_mem (H.smul_mem t ?_) (H.lie_mem hv hw))
  exacts [(H.mem_normalizer_iff' x).mp hx v hv, (H.mem_normalizer_iff x).mp hx w hw]

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

Goal state before:
pp: case add
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x y z : M
hy₁ : y ∈ Submodule.span R₁ S
hz₁ : z ∈ Submodule.span R₁ S
hy₂ : y ∈ Submodule.span R₂ S
hz₂ : z ∈ Submodule.span R₂ S
⊢ y + z ∈ Submodule.span R₂ S

Tactic:
exact Submodule.add_mem _ hy₂ hz₂

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
⊢ IsSolvable ↥(radical R L)

Tactic:
have hwf := LieSubmodule.wellFoundedGT_of_noetherian R L L
  rw [← CompleteLattice.isSupClosedCompact_iff_wellFoundedGT] at hwf
  refine hwf { I : LieIdeal R L | IsSolvable I } ⟨⊥, ?_⟩ fun I hI J hJ => ?_
  · exact LieAlgebra.isSolvableBot R L
  · rw [Set.mem_ofPred_eq] at hI hJ ⊢
    apply LieAlgebra.isSolvableAdd R L

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

Goal state before:
pp: case succ
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
k : ℕ
h : 1 < k + 1
hk : nilpotencyLength L M = k + 1
⊢ (match k + 1 with
    | 0 => ⊥
    | k.succ => lowerCentralSeries R L M k) ≤
    lowerCentralSeries R L M 1

Tactic:
exact antitone_lowerCentralSeries _ _ _ (Nat.le_of_lt_succ h)

Goal state after:
Module: Mathlib.FieldTheory.Finiteness

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ IsNoetherian K V ↔ Module.rank K V < ℵ₀

Tactic:
← b.mk_eq_rank'',

Goal state after:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ IsNoetherian K V ↔ #↑(Basis.ofVectorSpaceIndex K V) < ℵ₀
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, lowerCentralSeries R (↥(toEnd R L M).range) M k = ⊥) ↔ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
constructor <;> rintro ⟨k, hk⟩

Goal state after:
case mp
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 : ℕ
hk : lowerCentralSeries R (↥(toEnd R L M).range) M k = ⊥
⊢ ∃ k, lowerCentralSeries R L M k = ⊥

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
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ ∃ k, lowerCentralSeries R (↥(toEnd R L M).range) M k = ⊥
Module: Mathlib.FieldTheory.Tower

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝⁶ : Semiring F
inst✝⁵ : Semiring K
inst✝⁴ : Module F K
inst✝³ : AddCommMonoid A
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : Module.Finite F A
b : Finset A
hb : span F ↑b = ⊤
⊢ ↑b ⊆ ↑(restrictScalars F (span K ↑b))

Tactic:
exact Submodule.subset_span

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 K ↥E
h_le : F ≤ E
h : F = E
⊢ finrank K ↥F = finrank K ↥E

Tactic:
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:
rw [h]

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
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ K.toSubalgebra = (adjoin F S).toSubalgebra

Tactic:
rw [h]

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
⊢ Algebra.adjoin F S = (adjoin F S).toSubalgebra
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case h
G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
g₁ g₂ : G
h : ∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a
⊢ f g₁⁻¹ * f g₂ = 1

Tactic:
map_inv,

Goal state after:
case h
G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
g₁ g₂ : G
h : ∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a
⊢ (f g₁)⁻¹ * f g₂ = 1
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
L : Type u_3
L' : Type u_4
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L
inst✝⁴ : Algebra L E
inst✝³ : Algebra F L'
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
K K' : IntermediateField F E
h : K.toSubfield = K'.toSubfield
x : E
⊢ x ∈ K.toSubfield ↔ x ∈ K'.toSubfield

Tactic:
rw [h]

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
s : Set E
p : (x : E) → x ∈ adjoin F s → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E) x) ⋯
add : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : x ∈ adjoin F s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x * y) ⋯
x✝¹ : E
h✝ : x✝¹ ∈ adjoin F s
x : E
x✝ : x ∈ Subfield.closure (Set.range ⇑(Algebra.algebraMap F E) ∪ s)
h : p x x✝
⊢ p (-x) ⋯

Tactic:
← neg_one_smul F x,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
p : (x : E) → x ∈ adjoin F s → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E) x) ⋯
add : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : x ∈ adjoin F s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x * y) ⋯
x✝¹ : E
h✝ : x✝¹ ∈ adjoin F s
x : E
x✝ : x ∈ Subfield.closure (Set.range ⇑(Algebra.algebraMap F E) ∪ s)
h : p x x✝
⊢ p (-1 • x) ⋯
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
ι : Type u_3
i : ι → E
x : E
⊢ (∃ r ∈ (MvPolynomial.aeval i).range, ∃ s ∈ (MvPolynomial.aeval i).range, x = r / s) ↔
    ∃ r s, x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s

Tactic:
AlgHom.mem_range,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
i : ι → E
x : E
⊢ (∃ r, (∃ x, (MvPolynomial.aeval i) x = r) ∧ ∃ s, (∃ x, (MvPolynomial.aeval i) x = s) ∧ x = r / s) ↔
    ∃ r s, x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹⁶ : Field k
K : Type u
inst✝¹⁵ : Field K
L : Type v
M : Type w
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : Field M
inst✝¹¹ : Algebra K M
inst✝¹⁰ : IsAlgClosed M
inst✝⁹ : Algebra.IsAlgebraic K L
R : Type u
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type v
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
inst✝³ : Algebra R M
inst✝² : IsTorsionFree R S
inst✝¹ : IsTorsionFree R M
inst✝ : Algebra.IsAlgebraic R S
⊢ S →ₐ[R] M

Tactic:
letI : IsDomain R := (FaithfulSMul.algebraMap_injective R S).isDomain _
  letI := FractionRing.liftAlgebra R M
  letI := FractionRing.liftAlgebra R (FractionRing S)
  have := FractionRing.isScalarTower_liftAlgebra R M
  have := FractionRing.isScalarTower_liftAlgebra R (FractionRing S)
  let f : FractionRing S →ₐ[FractionRing R] M := liftAux (FractionRing R) (FractionRing S) M
  exact (f.restrictScalars R).comp ((Algebra.ofId S (FractionRing S)).restrictScalars R)

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
S : Set E
x : E
hx : x ∈ ⨆ i, F⟮↑i⟯
s : Finset ↑S
hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T

Tactic:
refine ⟨s.image Subtype.val, by simp, SetLike.le_def.mp ?_ hx'⟩
  simp_rw [Finset.coe_image, iSup_le_iff, adjoin_le_iff]
  rintro _ h _ rfl
  exact subset_adjoin F _ ⟨_, h, rfl⟩

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
⊢ ⊥ = ⊤ ↔ finrank F E = 1

Tactic:
by
  rw [← IntermediateField.finrank_bot', ← finrank_eq_one_iff_eq_top]

Goal state after:
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
hp : Nat.Prime (finrank F E)
⊢ ∀ (a : IntermediateField F E), a = ⊥ ∨ a = ⊤

Tactic:
· intro K
    simpa [← toSubalgebra_strictMono.apply_eq_bot_iff, ← toSubalgebra_strictMono.apply_eq_top_iff]
      using (Subalgebra.isSimpleOrder_of_finrank_prime _ _ hp).eq_bot_or_eq_top K.toSubalgebra

Goal state after: