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

Goal state before:
pp: 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
⊢ False

Tactic:
suffices ∀ i ∈ s, l i ∈ FixedPoints.subfield G F by
    replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
    simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
    refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)
    change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
    exact Submodule.smul_mem _ _ <| Submodule.subset_span <| by simpa

Goal state after:
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 ∈ s, l i ∈ subfield G F
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
f : ↥(Algebra.adjoin F ↑s) →ₐ[F] L
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Algebra.adjoin F ({a} ∪ ↑s)) →ₐ[F] L)

Tactic:
Set.union_comm,

Goal state after:
case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
f : ↥(Algebra.adjoin F ↑s) →ₐ[F] L
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Algebra.adjoin F (↑s ∪ {a})) →ₐ[F] L)
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
f : ↥(Algebra.adjoin F ↑s) →ₐ[F] L
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, (map (algebraMap F L) (minpoly F x)).Splits
⊢ Nonempty (↥(Subalgebra.restrictScalars F (↥(Algebra.adjoin F ↑s))[a]) →ₐ[F] L)

Tactic:
set Ks := Algebra.adjoin F (s : Set K)

Goal state after:
case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, (map (algebraMap F L) (minpoly F x)).Splits
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
⊢ Nonempty (↥(Subalgebra.restrictScalars F (↥Ks)[a]) →ₐ[F] L)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: case e'_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ + x✝², ⋯⟩ = φ₁ ⟨x✝³, x✝¹⟩ + φ₁ ⟨x✝², x✝⟩

Tactic:
← map_add

Goal state after:
case e'_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ + x✝², ⋯⟩ = φ₁ (⟨x✝³, x✝¹⟩ + ⟨x✝², x✝⟩)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: case e'_3
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ + x✝², ⋯⟩ = φ₂ ⟨x✝³, x✝¹⟩ + φ₂ ⟨x✝², x✝⟩

Tactic:
← map_add

Goal state after:
case e'_3
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ + x✝², ⋯⟩ = φ₂ (⟨x✝³, x✝¹⟩ + ⟨x✝², x✝⟩)
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
x✝³ : E
x✝² : Finset E
ha : x✝³ ∈ S
x✝¹ : x✝² ⊆ S
x✝ : x✝³ ∉ x✝²
h : P (adjoin F ↑x✝²)
⊢ P (adjoin F ({x✝³} ∪ ↑x✝²))

Tactic:
Set.union_comm,

Goal state after:
case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
x✝³ : E
x✝² : Finset E
ha : x✝³ ∈ S
x✝¹ : x✝² ⊆ S
x✝ : x✝³ ∉ x✝²
h : P (adjoin F ↑x✝²)
⊢ P (adjoin F (↑x✝² ∪ {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
⊢ ⊥ = ⊤ ↔ finrank F E = 1

Tactic:
← IntermediateField.finrank_bot',

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ⊥ = ⊤ ↔ finrank (↥⊥) E = 1
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
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
⊢ adjoin F ↑(Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)).coeffs = K

Tactic:
by
  set g := (minpoly K α).map (algebraMap K E)
  set K' : IntermediateField F E := adjoin F g.coeffs
  have hsub : K' ≤ K := by
    refine adjoin_le_iff.mpr fun x ↦ ?_
    rw [Finset.mem_coe, mem_coeffs_iff]
    rintro ⟨n, -, rfl⟩
    rw [coeff_map]
    apply Subtype.mem
  have dvd_g : minpoly K' α ∣ g.toSubring K'.toSubring (subset_adjoin F _) := by
    apply minpoly.dvd
    rw [aeval_def, eval₂_eq_eval_map]
    erw [g.map_toSubring K'.toSubring]
    rw [eval_map_algebraMap]
    exact minpoly.aeval K α
  have finrank_eq : ∀ K : IntermediateField F E, finrank K E = natDegree (minpoly K α) := by
    intro K
    have := adjoin.finrank (.of_finite K α)
    rw [adjoin_eq_top_of_adjoin_eq_top F hprim] at this
    simp_all
  refine eq_of_le_of_finrank_le' hsub ?_
  simp_rw [finrank_eq]
  convert!
    natDegree_le_of_dvd dvd_g
      ((g.monic_toSubring _ _).mpr <| (minpoly.monic <| .of_finite K α).map _).ne_zero using 1
  rw [natDegree_toSubring, natDegree_map]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

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

Tactic:
intro μ'

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

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := ⋯
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
this✝ : iSupIndep fun x ↦ (f.genEigenspace x) k
aux : ∀ μ' ∈ m.support.erase μ, (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k
this : (m.support.erase μ).SupIndep fun x ↦ (f.genEigenspace x) k
⊢ ∀ x ∈ m.support.erase μ, LinearMap.ker ((f - (algebraMap K (End K V)) x) ^ l₀) ≤ (f.genEigenspace x) k

Tactic:
intro μ'

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

Goal state before:
pp: K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree
key₂ :
  Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) =
    minpoly (↥K⟮(aeval (root p)) g⟯) (root p)
⊢ adjoin K ({(aeval (root p)) g} ∪ {root p}) = ⊤

Tactic:
Set.union_comm,

Goal state after:
K : Type u
inst✝ : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))
hf' : f.natDegree ≠ 0
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
p : K[X]
hp₁ : Irreducible p
hp₂ : p ∣ f.comp g
this✝ : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))
key₁ : f = minpoly K ((aeval (root p)) g)
key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree
key₂ :
  Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) =
    minpoly (↥K⟮(aeval (root p)) g⟯) (root p)
⊢ adjoin K ({root p} ∪ {(aeval (root p)) g}) = ⊤
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : h ≠ 0
⊢ e ≠ 0

Tactic:
contrapose this

Goal state after:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : e = 0
⊢ h = 0
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : h ≠ 0
⊢ f ≠ 0

Tactic:
contrapose this

Goal state after:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : f = 0
⊢ h = 0
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
⊢ H.normalizer.toSubmodule = ↑H.toLieSubmodule

Tactic:
IsCartanSubalgebra.self_normalizing,

Goal state after:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
⊢ H.toSubmodule = ↑H.toLieSubmodule
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case add
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
x✝ y✝ : L
hx✝ : x✝ ∈ ⨆ i ∈ s, rootSpace H i
hy✝ : y✝ ∈ ⨆ i ∈ s, rootSpace H i
hu : ⁅x✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
hv : ⁅y✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅x✝ + y✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
rw [add_lie]; exact add_mem hu hv

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

Goal state before:
pp: R : 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✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
this : ⨅ x, genWeightSpaceOf M (χ x) x ≠ ⊥
⊢ genWeightSpaceOf M (χ x) x ≠ ⊥

Tactic:
contrapose this

Goal state after:
R : 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✝ : LieRing.IsNilpotent L
χ : Weight R L M
x : L
this : genWeightSpaceOf M (χ x) x = ⊥
⊢ ⨅ x, genWeightSpaceOf M (χ x) x = ⊥
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : 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✝¹ : LieRing.IsNilpotent L
inst✝ : IsNilpotent L M
⊢ genWeightSpace M 0 = ⊤

Tactic:
by
  simp [genWeightSpace, genWeightSpaceOf]

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
⊢ H ≤ zeroRootSubalgebra R L H

Tactic:
by
  rw [← LieSubalgebra.toSubmodule_le_toSubmodule, ← H.coe_toLieSubmodule,
    coe_zeroRootSubalgebra, LieSubmodule.toSubmodule_le_toSubmodule]
  exact toLieSubmodule_le_rootSpace_zero R L H

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
⊢ (zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H

Tactic:
by
  refine le_antisymm ?_ (LieSubalgebra.le_normalizer _)
  intro x hx
  rw [LieSubalgebra.mem_normalizer_iff] at hx
  rw [mem_zeroRootSubalgebra]
  rintro ⟨y, hy⟩
  specialize hx y (le_zeroRootSubalgebra R L H hy)
  rw [mem_zeroRootSubalgebra] at hx
  obtain ⟨k, hk⟩ := hx ⟨y, hy⟩
  rw [← lie_skew, map_neg, neg_eq_zero] at hk
  use k + 1
  rw [Module.End.iterate_succ, LinearMap.coe_comp, Function.comp_apply, toEnd_apply_apply,
    LieSubalgebra.coe_bracket_of_module, Submodule.coe_mk, hk]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Hom

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B₁ B₂ : BilinForm R M'
l r : M →ₗ[R] M'
hₗ : Function.Surjective ⇑l
hᵣ : Function.Surjective ⇑r
h : B₁.comp l r = B₂.comp l r
x' y' : M
⊢ (B₁ (l x')) (r y') = (B₂ (l x')) (r y')

Tactic:
rw [← comp_apply, ← comp_apply, h]

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

Goal state before:
pp: case mem.add
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x y : L
i : ι
v w : L
hx✝ : v ∈ Submodule.span R (range b.h)
hy✝ : w ∈ Submodule.span R (range b.h)
hv : ⁅v, b.e i⁆ ∈ lieSpan R L (range b.e)
hw : ⁅w, b.e i⁆ ∈ lieSpan R L (range b.e)
⊢ ⁅v + w, b.e i⁆ ∈ lieSpan R L (range b.e)

Tactic:
simpa using add_mem hv hw

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
x : ↥I
y : ↥I
z : L
⊢ (Φ ⁅↑x, ↑y⁆) z = 0

Tactic:
hΦ_inv,

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
Φ : LinearMap.BilinForm R L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal R L
hI : IsAtom I
contra : I ≤ orthogonal Φ hΦ_inv I
x : ↥I
y : ↥I
z : L
⊢ -(Φ ↑y) ⁅↑x, z⁆ = 0
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : ∀ n ∈ W, (B n) x = 0
⊢ x ∈ (domRestrict B W).range.dualCoannihilator

Tactic:
rw [Submodule.mem_dualCoannihilator]

Goal state after:
case mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : ∀ n ∈ W, (B n) x = 0
⊢ ∀ φ ∈ (domRestrict B W).range, φ x = 0
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ ((Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod -
          (Multiset.map (fun x ↦ X - C x) (map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).roots).prod).coeff
      n =
    0

Tactic:
sub_self,

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ coeff 0 n = 0
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
⊢ IsNilpotent f ↔ ∀ (m : M), ∃ n, (f ^ n) m = 0

Tactic:
by
  refine ⟨fun ⟨n, hn⟩ m ↦ ⟨n, by simp [hn]⟩, fun h ↦ ?_⟩
  rcases Module.Finite.fg_top (R := R) (M := M) with ⟨S, hS⟩
  choose g hg using h
  use Finset.sup S g
  ext m
  have hm : m ∈ Submodule.span R S := by simp [hS]
  induction hm using Submodule.span_induction with
  | mem x hx => exact pow_map_zero_of_le (Finset.le_sup hx) (hg x)
  | zero => simp
  | add => simp_all
  | smul => simp_all

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x : L
hx : x ∈ ⊤
⊢ x ∈ lieSpan R L (range b.e ∪ range b.f)

Tactic:
simp [b.span_ef]

Goal state after: