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

Goal state before:
pp: case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ (f * C f.leadingCoeff⁻¹).degree ≤ q.degree

Tactic:
rw [degree_eq_natDegree f'_monic.ne_zero, degree_eq_natDegree q_monic.ne_zero,
    Nat.cast_le, natDegree_mul hf, natDegree_C, add_zero]

Goal state after:
case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ f.natDegree ≤ q.natDegree

case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
q_monic : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk 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ˣ
⊢ e.det ⇑(e.unitsSMul w) = ∏ i, ↑(w i)

Tactic:
by
  simp [det_apply]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotQuotEquivComm I f)
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) =
    (Ideal.Quotient.mk (span {(Ideal.Quotient.mk (Ideal.map C I)) f})) ((Ideal.Quotient.mk (Ideal.map C I)) p)

Tactic:
simp only [Polynomial.quotQuotEquivComm, quotientEquiv_mk,
    polynomialQuotientEquivQuotientPolynomial_map_mk]

Goal state after:
Module: Mathlib.Dynamics.Newton

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

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

Tactic:
· convert! dvd_zero _
      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
      rw [derivative_map, eval_map_algebraMap, ← mul_assoc, mul_neg, Ring.mul_inverse_cancel _ this,
        neg_mul, one_mul, add_neg_cancel]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : n₀ ∈ K[n₁ + s₁]
s₀ : End K V
hs₀ : s₀ ∈ K[n₁ + s₁]
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
n s : End K V
hn : IsNilpotent n
hs : s.IsSemisimple
hc : Commute n s
heq : n₁ + s₁ = n + s
hsf : Commute s (n₁ + s₁)
hnf : Commute n (n₁ + s₁)
hnil : IsNilpotent (s - s₀)
hss : (s - s₀).IsSemisimple
⊢ s = s₀

Tactic:
grind [eq_zero_of_isNilpotent_isSemisimple hnil hss]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
h : IsNilpotent a
⊢ IsUnit (exp a)

Tactic:
by
  apply isUnit_iff_exists.2
  use exp (-a)
  exact ⟨exp_mul_exp_neg_self h, exp_neg_mul_exp_self h⟩

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 : L
⊢ x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H

Tactic:
mem_normalizer_iff'

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ (∀ y ∈ H, ⁅y, x⁆ ∈ H) ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H
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
x : L
m : M
k : ℕ
⊢ (⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k

Tactic:
induction k with
  | zero => simp only [Function.iterate_zero, lowerCentralSeries_zero, LieSubmodule.mem_top]
  | succ k ih =>
    simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ',
      toEnd_apply_apply]
    exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
P₁ : AdjoinRoot (minpoly F x)
hP₁ : (Minpoly.toAdjoin F x) P₁ = 0
⊢ P₁ = 0

Tactic:
obtain ⟨P, rfl⟩ := mk_surjective P₁

Goal state after:
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
P : F[X]
hP₁ : (Minpoly.toAdjoin F x) ((AdjoinRoot.mk (minpoly F x)) P) = 0
⊢ (AdjoinRoot.mk (minpoly F x)) P = 0
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case neg
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : Cardinal.aleph0 ≤ Module.rank K ↥E1
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2

Tactic:
have := LinearMap.rank_le_of_injective _ <| Submodule.inclusion_injective <|
    show Subalgebra.toSubmodule E1.toSubalgebra ≤ Subalgebra.toSubmodule (E1 ⊔ E2).toSubalgebra by
      simp

Goal state after:
case neg
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h : Cardinal.aleph0 ≤ Module.rank K ↥E1
this :
  Module.rank K ↥(Subalgebra.toSubmodule E1.toSubalgebra) ≤
    Module.rank K ↥(Subalgebra.toSubmodule (E1 ⊔ E2).toSubalgebra)
⊢ finrank K ↥(E1 ⊔ E2) ≤ finrank K ↥E1 * finrank K ↥E2
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
⊢ finrank K ↥(f.genEigenrange μ₀ ↑(finrank K V)) + finrank K ↥((f.genEigenspace μ₀) ↑(finrank K V)) = finrank K V

Tactic:
rw [Module.End.genEigenspace_nat, Module.End.genEigenrange_nat]

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
⊢ finrank K ↥((f - μ₀ • 1) ^ finrank K V).range + finrank K ↥((f - μ₀ • 1) ^ finrank K V).ker = finrank K V
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
h_dim_add : finrank K ↥ER + finrank K ↥ES = finrank K V
h_dim_ER : finrank K ↥ER < n.succ
ih_ER : ⨆ μ, f'.maxGenEigenspace μ = ⊤
ih_ER' : ⨆ μ, Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
⊢ ER ≤ ⨆ μ, f.maxGenEigenspace μ

Tactic:
← ih_ER'

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
h_dim_add : finrank K ↥ER + finrank K ↥ES = finrank K V
h_dim_ER : finrank K ↥ER < n.succ
ih_ER : ⨆ μ, f'.maxGenEigenspace μ = ⊤
ih_ER' : ⨆ μ, Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
⊢ ⨆ μ, Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ ⨆ μ, f.maxGenEigenspace μ
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_2.inr
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Field K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst✝ : Nonempty ↑c
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := ↥(adjoin F ↑S) →ₐ[F] K
ω : Ω
θ : ↑c → Lifts F E K
ge : ∀ (π : ↑c), θ π ≥ ↑π
hθ : ∀ (π : ↑c), { carrier := adjoin F ↑S, emb := ω } ≤ θ π
eq : ∀ (π : ↑c), (θ π).carrier = adjoin F (↑(↑π).carrier ∪ ↑S)
π₁ π₂ : ↑c
h : π₁ ≤ π₂
x : E
hx : x ∈ ↑S
⊢ ((θ π₂).emb.comp (inclusion ⋯)) ⟨x, ⋯⟩ = (θ π₁).emb ⟨x, ⋯⟩

Tactic:
· change (θ π₂).emb (inclusion (hθ π₂).1 ⟨x, subset_adjoin _ _ hx⟩) =
        (θ π₁).emb (inclusion (hθ π₁).1 ⟨x, subset_adjoin _ _ hx⟩)
      rw [(hθ π₁).2, (hθ π₂).2]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : derivative f = 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ derivative f * g

pp: case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ derivative f * g

Tactic:
· rw [eq_C_of_derivative_eq_zero hdf0]
    simp only [derivative_C, zero_mul, dvd_zero, implies_true]

Goal state after:
case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ derivative f * g
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : eval a f = 0
h0 : 0 < rootMultiplicity a f
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a (derivative f) + rootMultiplicity a g

Tactic:
derivative_rootMultiplicity_of_root haf

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
a : K
haf : eval a f = 0
h0 : 0 < rootMultiplicity a f
⊢ (f.IsRoot a → g.IsRoot a) → rootMultiplicity a f ≤ rootMultiplicity a f - 1 + rootMultiplicity a g
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ S, ∀ τ ≥ y, ¬↑S ⊆ ↑τ.carrier
S : Λ → Finset E
hS : ∀ (σ : Λ), ∀ τ ≥ L σ, ¬↑(S σ) ⊆ ↑τ.carrier
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : α ∈ ↑θ.carrier ∧ ∀ (i : Λ), ↑(S i) ⊆ ↑θ.carrier
⊢ ϕ.carrier ⊔ F⟮α⟯ ≤ θ.carrier

Tactic:
sup_le_iff,

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier
this✝¹ : ⊥.IsExtendible
ϕ : Lifts F E K
hϕ : Maximal (fun x ↦ x ∈ {ϕ | ϕ.IsExtendible}) ϕ
this✝ : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x✝ : Algebra (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := ↥(↥ϕ.carrier)⟮α⟯ →ₐ[↥ϕ.carrier] K
this : FiniteDimensional ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : Λ → Lifts F E K := fun σ ↦ { carrier := restrictScalars F (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max : ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ S, ∀ τ ≥ y, ¬↑S ⊆ ↑τ.carrier
S : Λ → Finset E
hS : ∀ (σ : Λ), ∀ τ ≥ L σ, ¬↑(S σ) ⊆ ↑τ.carrier
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : α ∈ ↑θ.carrier ∧ ∀ (i : Λ), ↑(S i) ⊆ ↑θ.carrier
⊢ ϕ.carrier ≤ θ.carrier ∧ F⟮α⟯ ≤ θ.carrier
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = C f.leadingCoeff * minpoly K x
hi : f ≠ 0
⊢ f.natDegree ∣ finrank K L

Tactic:
rw [key, natDegree_C_mul (leadingCoeff_ne_zero.mpr hi)]

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = C f.leadingCoeff * minpoly K x
hi : f ≠ 0
⊢ (minpoly K x).natDegree ∣ finrank K L
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : minpoly K x = minpoly K y
hy : IsAlgebraic K y
⊢ ((adjoinRootEquivAdjoin K ⋯).symm.trans
        ((AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp).trans (adjoinRootEquivAdjoin K ⋯)))
      (AdjoinSimple.gen K x) =
    AdjoinSimple.gen K y

Tactic:
trans_apply,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : minpoly K x = minpoly K y
hy : IsAlgebraic K y
⊢ ((AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp).trans (adjoinRootEquivAdjoin K ⋯))
      ((adjoinRootEquivAdjoin K ⋯).symm (AdjoinSimple.gen K x)) =
    AdjoinSimple.gen K y
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : minpoly K x = minpoly K y
hy : IsAlgebraic K y
⊢ ((AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp).trans (adjoinRootEquivAdjoin K ⋯))
      (AdjoinRoot.root (minpoly K x)) =
    AdjoinSimple.gen K y

Tactic:
trans_apply,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : minpoly K x = minpoly K y
hy : IsAlgebraic K y
⊢ (adjoinRootEquivAdjoin K ⋯)
      ((AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp) (AdjoinRoot.root (minpoly K x))) =
    AdjoinSimple.gen K y
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ max (Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E) ∪ s)) (Cardinal.lift.{u, v} ℵ₀) ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀

Tactic:
sup_le_iff,

Goal state after:
F : Type u
inst✝² : Field F
E : Type v
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ Cardinal.lift.{u, v} #↑(Set.range ⇑(algebraMap F E) ∪ s) ≤
      max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀ ∧
    Cardinal.lift.{u, v} ℵ₀ ≤ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑s)) ℵ₀
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.mem.inl.inr.inr
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
f x y u v : L
t : IsSl2Triple v u f
__spread✝⁻⁰ : Submodule R L := span R {u, f, v}
⊢ -⁅v, u⁆ ∈ span R {u, f, v}

Tactic:
t.lie_h_e_nsmul,

Goal state after:
case mem.mem.inl.inr.inr
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
f x y u v : L
t : IsSl2Triple v u f
__spread✝⁻⁰ : Submodule R L := span R {u, f, v}
⊢ -(2 • u) ∈ span R {u, f, v}
Module: Mathlib.Algebra.Lie.Sl2

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
h e f : L
t : IsSl2Triple h e f
x y : L
hx : x ∈ (span R {e, f, h}).carrier
hy : y ∈ (span R {e, f, h}).carrier
⊢ ⁅x, y⁆ ∈ (span R {e, f, h}).carrier

Tactic:
by
    simp only [carrier_eq_coe, SetLike.mem_coe] at hx hy ⊢
    induction hx using span_induction with
    | zero => simp
    | add u v hu hv hu' hv' => simpa only [add_lie] using add_mem hu' hv'
    | smul t u hu hu' => simpa only [smul_lie] using smul_mem _ t hu'
    | mem u hu =>
      induction hy using span_induction with
      | zero => simp
      | add u v hu hv hu' hv' => simpa only [lie_add] using add_mem hu' hv'
      | smul t u hv hv' => simpa only [lie_smul] using smul_mem _ t hv'
      | mem v hv =>
        push _ ∈ _ at hu hv
        rcases hu with rfl | rfl | rfl <;>
        rcases hv with rfl | rfl | rfl <;> (try simp only [lie_self, zero_mem])
        · rw [t.lie_e_f]
          apply subset_span
          simp
        · rw [← lie_skew, t.lie_h_e_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp
        · rw [← lie_skew, t.lie_e_f, neg_mem_iff]
          apply subset_span
          simp
        · rw [← lie_skew, t.lie_h_f_nsmul, neg_neg]
          apply nsmul_mem <| subset_span _
          simp
        · rw [t.lie_h_e_nsmul]
          apply nsmul_mem <| subset_span _
          simp
        · rw [t.lie_h_f_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅⟨y, hy⟩, x⁆ = 0

Tactic:
LieSubalgebra.coe_bracket_of_module,

Goal state after:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
hy : y ∈ H
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅↑⟨y, hy⟩, x⁆ = 0
Module: Mathlib.Algebra.Lie.Weights.Cartan

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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
⊢ rootSpace H 0 = H.toLieSubmodule

Tactic:
rw [← LieSubmodule.toSubmodule_inj, ← coe_zeroRootSubalgebra,
    zeroRootSubalgebra_eq_of_is_cartan R L H, LieSubalgebra.coe_toLieSubmodule]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Cartan

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
inst✝² : LieRing.IsNilpotent ↥H
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
this : ⇑H.subtype '' s = {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
⊢ x ∈ corootSpace α ↔ ∃ x_1 ∈ Submodule.span R s, H.subtype x_1 = H.subtype x

Tactic:
rw [← Submodule.mem_map, Submodule.coe_subtype, Submodule.map_span, mem_corootSpace, ← this]

Goal state after: