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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
⊢ (mk g) (∑ i_1, (monomial ↑i_1) (Pi.single i 1 i_1)) = root g ^ ↑i

Tactic:
Finset.sum_eq_single i

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
g : R[X]
hg : g.Monic
i : Fin g.natDegree
⊢ (mk g) ((monomial ↑i) (Pi.single i 1 i)) = root g ^ ↑i

case h₀
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial ↑b) (Pi.single i 1 b) = 0

case h₁
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
⊢ i ∉ Finset.univ → (monomial ↑i) (Pi.single i 1 i) = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → ι → R
⊢ (basisFun R ι).det v = (of v).det

Tactic:
by
  rw [Pi.basisFun_det]
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inl
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
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
k : ι
⊢ e.det v * ((Basis.mk hli hsp).coord k) (v k) = ↑e.det (update v k (v k))

Tactic:
rw [mk_coord_apply_eq, mul_one, update_eq_self]
    congr

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

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

Tactic:
simp_rw [isFinitelySemisimple_iff, mem_invtSubmodule, this]

Goal state after:
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
D : LieDerivation R L L
hD : ∀ (x : L), ⁅x, D⁆ = 0
x : L
⊢ (ad R L) (D x) = 0

Tactic:
simp [ad_apply_lieDerivation, hD]

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

Goal state before:
pp: R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst✝¹⁷ : LieRing L
inst✝¹⁶ : LieAlgebra R L
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : LieRingModule L M
inst✝¹² : LieModule R L M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x : L
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ ((AlgebraTensorModule.curry ((↑(lift.equiv (RingHom.id R) M N P)).toFun ⁅x, f⁆)) m) n =
    ((AlgebraTensorModule.curry ⁅x, (↑(lift.equiv (RingHom.id R) M N P)).toFun f⁆) m) n

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe,
        AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars,
        lift.equiv_apply, LieHom.lie_apply, LinearMap.sub_apply, lie_tmul_right, map_add]

Goal state after:
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst✝¹⁷ : LieRing L
inst✝¹⁶ : LieAlgebra R L
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : LieRingModule L M
inst✝¹² : LieModule R L M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
x : L
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ ⁅x, (f m) n⁆ - (f m) ⁅x, n⁆ - (f ⁅x, m⁆) n = ⁅x, (f m) n⁆ - ((f ⁅x, m⁆) n + (f m) ⁅x, n⁆)
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
n : ℕ
ih : derivedSeriesOfIdeal R L (n + 1) ⊤ = ⊤ ↔ derivedSeriesOfIdeal R L 1 ⊤ = ⊤
h : derivedSeriesOfIdeal R L 1 ⊤ = ⊤
⊢ ⁅derivedSeriesOfIdeal R L (n + 1) ⊤, derivedSeriesOfIdeal R L (n + 1) ⊤⁆ = ⊤

Tactic:
by rwa [ih.mpr h]

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

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L L) x) x = 0 → ((bracket' R A L L) y) y = 0 → ((bracket' R A L L) (x + y)) (x + y) = 0

Tactic:
· intro z₁ z₂ h₁ h₂
    suffices bracket' R A L L z₁ z₂ + bracket' R A L L z₂ z₁ = 0 by
      rw [map_add, map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂,
        zero_add, add_zero, add_comm, this]
    refine z₁.induction_on ?_ ?_ ?_
    · simp only [map_zero, add_zero, LinearMap.zero_apply]
    · intro a₁ l₁; refine z₂.induction_on ?_ ?_ ?_
      · simp only [map_zero, add_zero, LinearMap.zero_apply]
      · intro a₂ l₂
        simp only [← lie_skew l₂ l₁, mul_comm a₁ a₂, TensorProduct.tmul_neg, bracket'_tmul,
          add_neg_cancel]
      · intro y₁ y₂ hy₁ hy₂
        simp only [hy₁, hy₂, add_add_add_comm, add_zero, LinearMap.add_apply, map_add]
    · intro y₁ y₂ hy₁ hy₂
      simp only [add_add_add_comm, hy₁, hy₂, add_zero, LinearMap.add_apply, map_add]

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

Goal state before:
pp: case h
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 z : L
⊢ ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆

Tactic:
apply add_lie

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
⊢ H.normalizer = H ↔ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule) = ⊥

Tactic:
by
  rw [LieSubmodule.eq_bot_iff]
  refine ⟨fun h => ?_, fun h => le_antisymm ?_ H.le_normalizer⟩
  · rintro ⟨x⟩ hx
    suffices x ∈ H by rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
      coe_toLieSubmodule, mem_toSubmodule]
    rw [← h, H.mem_normalizer_iff']
    intro y hy
    replace hx : ⁅_, LieSubmodule.Quotient.mk' _ x⁆ = 0 := hx ⟨y, hy⟩
    rwa [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero] at hx
  · intro x hx
    let y := LieSubmodule.Quotient.mk' H.toLieSubmodule x
    have hy : y ∈ LieModule.maxTrivSubmodule R H (L ⧸ H.toLieSubmodule) := by
      rintro ⟨z, hz⟩
      rw [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero, coe_bracket_of_module,
        Submodule.coe_mk, mem_toLieSubmodule]
      exact (H.mem_normalizer_iff' x).mp hx z hz
    simpa [y] using h y hy

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✝ : LieModule R L M
k : ℕ
ih : ↑↑(lowerCentralSeries R L M k) = ↑↑(lowerCentralSeries ℤ L M k)
⊢ ↑↑⁅⊤, lowerCentralSeries R L M k⁆ = ↑↑(lowerCentralSeries ℤ L M (k + 1))

Tactic:
lowerCentralSeries_succ

Goal state after:
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✝ : LieModule R L M
k : ℕ
ih : ↑↑(lowerCentralSeries R L M k) = ↑↑(lowerCentralSeries ℤ L M k)
⊢ ↑↑⁅⊤, lowerCentralSeries R L M k⁆ = ↑↑⁅⊤, lowerCentralSeries ℤ L M k⁆
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ.inl
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
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ k + 1
hk : l ≤ k
⊢ lowerCentralSeries R L M (k + 1) ≤ lowerCentralSeries R L M l

Tactic:
lowerCentralSeries_succ

Goal state after:
case succ.inl
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
k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ k + 1
hk : l ≤ k
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ ≤ lowerCentralSeries R L M l
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆ ≤ lowerCentralSeries R L L (k + 1)

Tactic:
lowerCentralSeries_succ

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆ ≤ ⁅⊤, lowerCentralSeries R L L k⁆
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
⊢ LieModule.IsNilpotent L M

Tactic:
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R I M

Goal state after:
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
⊢ LieModule.IsNilpotent L M
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
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ (∃ k, lowerCentralSeries R L (M ⧸ N) k = ⊥) ↔ ∃ k, lowerCentralSeries R L M k ≤ N

Tactic:
refine exists_congr fun k ↦ ?_

Goal state after:
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
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lowerCentralSeries R L (M ⧸ N) k = ⊥ ↔ lowerCentralSeries R L M k ≤ N
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✝ : LieModule R L M
k : ℕ
h : lowerCentralSeries R L M (k + 1) = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥
⊢ ⁅⊤,
      match k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k⁆ =
    ⊥

Tactic:
lowerCentralSeries_succ

Goal state after:
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✝ : LieModule R L M
k : ℕ
h : ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥
⊢ ⁅⊤,
      match k + 1 with
      | 0 => ⊥
      | k.succ => lowerCentralSeries R L M k⁆ =
    ⊥
Module: Mathlib.FieldTheory.Finiteness

Goal state before:
pp: case mpr
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
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
⊢ IsNoetherian K ↥⊤

Tactic:
refine isNoetherian_of_fg_of_noetherian _ ⟨Set.Finite.toFinset hbfinite, ?_⟩

Goal state after:
case mpr
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
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
⊢ span K ↑hbfinite.toFinset = ⊤
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
this : ∀ i ∈ s, l i ∈ subfield G F
⊢ False

Tactic:
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:
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
⊢ restrictNormalHom K = MonoidHom.id Gal(K/F)

Tactic:
by
  ext f x
  dsimp only [restrictNormalHom, MonoidHom.mk'_apply, MonoidHom.id_apply]
  apply (algebraMap K K).injective
  rw [AlgEquiv.restrictNormal_commutes]
  simp only [Algebra.algebraMap_self, RingHom.id_apply]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
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
⊢ f = 1 ∨ g = 1

Tactic:
have := eval₂ G F x

Goal state after:
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 (minpoly G F x) = 0
⊢ f = 1 ∨ g = 1
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : (Polynomial.map (algebraMap K L) p).Splits
hF : ∀ x ∈ p.rootSet L, x ∈ F
⊢ (Polynomial.map (algebraMap K ↥F) p).Splits

Tactic:
classical
  have := Splits.of_splits_map (f := p.map (algebraMap K F)) (algebraMap F L)
  rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq] at this
  exact this h (by simpa [rootSet_def] using hF)

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
x : E
⊢ (∃ y ∈ (Algebra.adjoin F S).toSubring, ∃ z ∈ (Algebra.adjoin F S).toSubring, y / z = x) ↔
    ∃ r ∈ Algebra.adjoin F S, ∃ s ∈ Algebra.adjoin F S, x = r / s

Tactic:
Subalgebra.mem_toSubring,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
⊢ (∃ y ∈ Algebra.adjoin F S, ∃ z ∈ Algebra.adjoin F S, y / z = x) ↔
    ∃ r ∈ Algebra.adjoin F S, ∃ s ∈ Algebra.adjoin F S, x = r / 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
S T : Set E
⊢ restrictScalars F (adjoin (↥(adjoin F S)) T) = restrictScalars F (adjoin (↥(adjoin F T)) S)

Tactic:
by
  rw [adjoin_adjoin_left, adjoin_adjoin_left, Set.union_comm]

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

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 (restrictScalars F (↥(adjoin F ↑x✝²))⟮x✝³⟯)
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ p.roots
r_nu : ¬IsUnit (a - ↑ₐ r)
⊢ r ∈ σ a

Tactic:
mem_iff,

Goal state after:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ p.roots
r_nu : ¬IsUnit (a - ↑ₐ r)
⊢ ¬IsUnit (↑ₐ r - a)
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := C (eval k p) - p
hroot : (C k - X) * -(q / (X - C k)) = q
aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q
⊢ (fun x ↦ eval x p) k ∈ σ ((aeval a) p)

Tactic:
mem_iff,

Goal state after:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := C (eval k p) - p
hroot : (C k - X) * -(q / (X - C k)) = q
aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q
⊢ ¬IsUnit (↑ₐ ((fun x ↦ eval x p) k) - (aeval a) p)
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := C (eval k p) - p
hroot : (C k - X) * -(q / (X - C k)) = q
aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q
⊢ ¬IsUnit ((aeval a) ((C k - X) * -(q / (X - C k))))

Tactic:
aeval_mul

Goal state after:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := C (eval k p) - p
hroot : (C k - X) * -(q / (X - C k)) = q
aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q
⊢ ¬IsUnit ((aeval a) (C k - X) * (aeval a) (-(q / (X - C k))))
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : k ∈ σ ((aeval a) p)
hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) (C k - p).roots).prod
h_ne : C k - p ≠ 0
lead_ne : (C k - p).leadingCoeff ≠ 0
lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))
p_a_eq : (aeval a) (C k - p) = ↑ₐ k - (aeval a) p
⊢ k ∈ (fun x ↦ eval x p) '' σ a

Tactic:
mem_iff,

Goal state after:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : ¬IsUnit (↑ₐ k - (aeval a) p)
hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) (C k - p).roots).prod
h_ne : C k - p ≠ 0
lead_ne : (C k - p).leadingCoeff ≠ 0
lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))
p_a_eq : (aeval a) (C k - p) = ↑ₐ k - (aeval a) p
⊢ k ∈ (fun x ↦ eval x p) '' σ a
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
⊢ IsAlgClosed k'

Tactic:
by
  apply IsAlgClosed.of_exists_root
  intro p hmp hp
  have hpe : degree (p.map e.symm.toRingHom) ≠ 0 := by
    rw [degree_map]
    exact ne_of_gt (degree_pos_of_irreducible hp)
  rcases IsAlgClosed.exists_root (k := k) (p.map e.symm.toRingHom) hpe with ⟨x, hx⟩
  use e x
  rw [IsRoot] at hx
  apply e.symm.injective
  rw [map_zero, ← hx]
  clear hx hpe hp hmp
  induction p using Polynomial.induction_on <;> simp_all

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case insert
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst✝ : ∀ (i : ι), FiniteDimensional K ↥(t i)
x✝ : Set ι
a✝¹ : ι
s✝ : Set ι
s : a✝¹ ∉ s✝
hs : s✝.Finite
a✝ : FiniteDimensional K ↥(⨆ x ∈ s✝, t x)
⊢ FiniteDimensional K ↥(⨆ x ∈ insert a✝¹ s✝, t x)

Tactic:
rw [iSup_insert]
    exact IntermediateField.finiteDimensional_sup _ _

Goal state after:
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
x : L
hx : IsIntegral K x
⊢ Module.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree

Tactic:
rw [PowerBasis.finrank (adjoin.powerBasis hx :)]

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ (powerBasis hx).dim = (minpoly K x).natDegree
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
K : Type u
inst✝³ : Field K
inst✝² : Algebra F K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ ∀ (x : L), IsAlgebraic (↥⊤) x

Tactic:
by
    intro x
    let xt : (⊤ : IntermediateField K L) := ⟨x, mem_top⟩
    exact isAlgebraic_algebraMap xt

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

Goal state before:
pp: case insert.refine_2
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : ι → End R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
⊢ ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈ ↑(s.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
· rw [map_add, hk, zero_add]
    suffices (s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i))).map (g ^ k) ≤
        s.sup fun χ ↦ (⨅ i, (f i).maxGenEigenspace (χ i)) from
      this (Submodule.mem_map_of_mem hz)
    simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := ι → R), Submodule.map_iSup (ι := _ ∈ s)]
    refine iSup₂_mono fun χ _ ↦ ?_
    rintro - ⟨u, hu, rfl⟩
    refine aux (f l) (χ₂ l) k (⨅ i, (f i).maxGenEigenspace (χ i)) ?_ hu
    simp only [Submodule.coe_iInf]
    exact h l χ

Goal state after: