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

Goal state before:
pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin ↥(Algebra.adjoin F ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) f).roots.toFinset)
        ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).roots.toFinset) =
    ⊤

Tactic:
← map_map,

Goal state after:
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin
        ↥(Algebra.adjoin F ↑(Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) f)).roots.toFinset)
        ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).roots.toFinset) =
    ⊤
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin K ↑(Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).roots.toFinset) =
    ⊤

Tactic:
← map_map,

Goal state after:
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin K ↑(Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) g)).roots.toFinset) =
    ⊤
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: 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
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
H5 : IsIntegral (↥Ks) a
⊢ map (algebraMap (↥Ks) L) (minpoly (↥Ks) a) ∣ map ((algebraMap (↥Ks) L).comp (algebraMap F ↥Ks)) (minpoly F a)

Tactic:
← map_map,

Goal state after:
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
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
H5 : IsIntegral (↥Ks) a
⊢ map (algebraMap (↥Ks) L) (minpoly (↥Ks) a) ∣ map (algebraMap (↥Ks) L) (map (algebraMap F ↥Ks) (minpoly F a))
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : CommRing M
inst✝³ : Algebra R K
inst✝² : Algebra R M
inst✝¹ : Algebra K M
inst✝ : IsScalarTower R K M
x : M
int : IsIntegral R x
f : K →+* L
h : (Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)).Splits
⊢ Polynomial.map f (minpoly K x) ∣ Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)

Tactic:
← map_map,

Goal state after:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : CommRing M
inst✝³ : Algebra R K
inst✝² : Algebra R M
inst✝¹ : Algebra K M
inst✝ : IsScalarTower R K M
x : M
int : IsIntegral R x
f : K →+* L
h : (Polynomial.map (f.comp (algebraMap R K)) (minpoly R x)).Splits
⊢ Polynomial.map f (minpoly K x) ∣ Polynomial.map f (Polynomial.map (algebraMap R K) (minpoly R x))
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))
⊢ k ∈ (fun x ↦ eval x p) '' σ a

Tactic:
have p_a_eq : aeval a (C k - p) = ↑ₐ k - aeval a p := by
    simp only [aeval_C, map_sub]

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 : 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: case refine_2
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
x : k[X]
hu : x ∈ nonunits k[X]
h0 : x ≠ 0
w✝¹ w✝ : k[X]
h : ∀ (a : K), (aeval a) (x * w✝¹) ≠ 0 ∨ (aeval a) (x * w✝) ≠ 0
⊢ False

Tactic:
obtain ⟨a, ha : _ = _⟩ := IsAlgClosed.exists_root (x.map <| algebraMap k K) <| by
      simpa only [degree_map] using (ne_of_lt <| degree_pos_of_ne_zero_of_nonunit h0 hu).symm

Goal state after:
case refine_2
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Algebra k K
x : k[X]
hu : x ∈ nonunits k[X]
h0 : x ≠ 0
w✝¹ w✝ : k[X]
h : ∀ (a : K), (aeval a) (x * w✝¹) ≠ 0 ∨ (aeval a) (x * w✝) ≠ 0
a : K
ha : eval a (map (algebraMap k K) x) = 0
⊢ False
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
s : IntermediateField F E
⊢ ∀ x ∈ (fun x ↦ F⟮x⟯) '' ↑s, IsCompactElement x

Tactic:
rintro t ⟨x, _, rfl⟩

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
s : IntermediateField F E
x : E
left✝ : x ∈ ↑s
⊢ IsCompactElement ((fun x ↦ 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
α : E
inst✝ : FiniteDimensional F E
hprim : F⟮α⟯ = ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F ↑g.coeffs
hsub : K' ≤ K
⊢ (aeval α) (minpoly (↥K) α) = 0

Tactic:
exact minpoly.aeval K α

Goal state after:
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
⊢ (C (AdjoinSimple.gen K ((aeval (root p)) g))).natDegree <
    (Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g).natDegree

Tactic:
by simpa [Nat.pos_iff_ne_zero] using hg'

Goal state after:
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.toLieSubmodule.normalizer = ↑H.toLieSubmodule

Tactic:
coe_normalizer_eq_normalizer,

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.normalizer.toSubmodule = ↑H.toLieSubmodule
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
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
hk' : H.toLieSubmodule.normalizer = H.toLieSubmodule
⊢ ↑H.toLieSubmodule = H.toSubmodule

Tactic:
LieSubalgebra.coe_toLieSubmodule

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
hk' : H.toLieSubmodule.normalizer = H.toLieSubmodule
⊢ H.toSubmodule = H.toSubmodule
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case pos
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 χ
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
⊢ ⁅u, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
induction hm using LieSubmodule.iSup_induction' with
    | zero => simp
    | add _ _ _ _ hv hw => rw [lie_add]; exact add_mem hv hw
    | mem χ₂ v hv =>
      by_cases hχ₂ : χ₂ ∈ s; swap
      · simp_all
      apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)
      simp_all [lie_mem_genWeightSpace_of_mem_genWeightSpace]

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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
α χ : ↥H → R
x : L
hx : x ∈ rootSpace H α
m : M
hm : m ∈ ↑(genWeightSpace M χ)
⊢ ((toEnd R L M) x) m ∈ ↑(genWeightSpace M (α + χ))

Tactic:
let x' : rootSpace H α := ⟨x, hx⟩

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
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
α χ : ↥H → R
x : L
hx : x ∈ rootSpace H α
m : M
hm : m ∈ ↑(genWeightSpace M χ)
x' : ↥(rootSpace H α) := ⟨x, hx⟩
⊢ ((toEnd R L M) x) m ∈ ↑(genWeightSpace M (α + χ))
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
x : L
hx : x ∈ H.toLieSubmodule
⊢ x ∈ rootSpace H 0

Tactic:
simp only [LieSubalgebra.mem_toLieSubmodule] at hx

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
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ H
⊢ x ∈ rootSpace H 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
⊢ H.toSubmodule = ↑H.toLieSubmodule

Tactic:
LieSubalgebra.coe_toLieSubmodule

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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
⊢ H.toSubmodule = H.toSubmodule
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
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Nontrivial M
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ : ((toEnd R L M) h).HasEigenvalue μ₀
m₀ : M
hm₀ : ((toEnd R L M) h).HasEigenvector μ₀ m₀
evals : ℕ → R := fun n ↦ μ₀ + 2 * ↑n
e_vecs : ℕ → M := fun n ↦ ((toEnd R L M) e ^ n) m₀
h_exists_zero : ∃ k, e_vecs k = 0
n : ℕ
hn_ne : ¬e_vecs n = 0
hn_zero : e_vecs (n + 1) = 0
⊢ ⁅e, e_vecs n⁆ = 0

Tactic:
lie_e_pow_toEnd_e n

Goal state after:
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
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Nontrivial M
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ : ((toEnd R L M) h).HasEigenvalue μ₀
m₀ : M
hm₀ : ((toEnd R L M) h).HasEigenvector μ₀ m₀
evals : ℕ → R := fun n ↦ μ₀ + 2 * ↑n
e_vecs : ℕ → M := fun n ↦ ((toEnd R L M) e ^ n) m₀
h_exists_zero : ∃ k, e_vecs k = 0
n : ℕ
hn_ne : ¬e_vecs n = 0
hn_zero : e_vecs (n + 1) = 0
⊢ ((toEnd R L M) e ^ (n + 1)) m₀ = 0
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
x : L
χ : L → R
⊢ LieSubmodule.map (genWeightSpaceOf M (χ x) x).incl (genWeightSpace (↥(genWeightSpaceOf M (χ x) x)) χ) =
    genWeightSpace M χ

Tactic:
simpa [map_genWeightSpace_eq_of_injective (genWeightSpaceOf M (χ x) x).injective_incl]
    using genWeightSpace_le_genWeightSpaceOf M x χ

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
i j : ι
⊢ -⁅b.h j, b.f i⁆ = b.A i j • b.f i

Tactic:
b.lie_h_f i j,

Goal state after:
ι : 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
i j : ι
⊢ -(-b.A i j • b.f i) = b.A i j • b.f i
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : (B.restrict p) ⟨z, hz⟩ = 0
⊢ B z = 0

Tactic:
ext w
    obtain ⟨x, y, hx, hy, rfl⟩ := Submodule.codisjoint_iff_exists_add_eq.mp hpq w
    simpa [hB z hz y hy] using LinearMap.congr_fun h ⟨x, hx⟩

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
n : ℕ
hfn : f.natDegree = n + 1
⊢ f.removeFactor.natDegree = n

Tactic:
by rw [natDegree_removeFactor, hfn, n.add_sub_cancel]

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih : ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → (map (algebraMap K (SplittingFieldAux n f)) f).Splits
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
⊢ (map ((algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).comp (AdjoinRoot.of f.factor)) f).Splits

Tactic:
← map_map,

Goal state after:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih : ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → (map (algebraMap K (SplittingFieldAux n f)) f).Splits
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
⊢ (map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (map (AdjoinRoot.of f.factor) f)).Splits
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 : map ((algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).comp (AdjoinRoot.of f.factor)) f ≠ 0
⊢ Algebra.adjoin K
      ↑(map ((algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)).comp (AdjoinRoot.of f.factor))
              f).roots.toFinset =
    ⊤

Tactic:
← map_map,

Goal state after:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Algebra.adjoin K (f.rootSet (SplittingFieldAux n f)) = ⊤
K : Type u
x✝ : Field K
f : K[X]
hfn : f.natDegree = n.succ
hndf : f.natDegree ≠ 0
hfn0 : f ≠ 0
hmf0 : map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) (map (AdjoinRoot.of f.factor) f) ≠ 0
⊢ Algebra.adjoin K
      ↑(map (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
              (map (AdjoinRoot.of f.factor) f)).roots.toFinset =
    ⊤
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 : ℕ
⊢ (toSplittingField s) ((subProdXSubC f).coeff n) = 0

Tactic:
simp_rw [← AlgHom.coe_toRingHom, ← coeff_map, subProdXSubC, Polynomial.map_sub,
    Polynomial.map_prod, Polynomial.map_sub, map_X, map_C, toSplittingField,
    AlgHom.coe_toRingHom, MvPolynomial.aeval_X, dif_pos h,
    ← (finEquivRoots (Monics.splits_finsetProd h)).symm.prod_comp, Equiv.apply_symm_apply]

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(MvPolynomial.aeval fun fi ↦ if hf : fi.fst ∈ s then (↑((finEquivRoots ⋯) fi.snd)).1 else 37))
            (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          ∏ x, (X - C (↑x).1)).coeff
      n =
    0
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map ((Ideal.Quotient.mk (maxIdeal k)).comp (algebraMap k (MvPolynomial (Vars k) k))) ↑f).coeff n✝ =
    (∏ i, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))).coeff n✝

Tactic:
← map_map,

Goal state after:
k : Type u
inst✝ : Field k
f : Monics k
n✝ : ℕ
⊢ (map (Ideal.Quotient.mk (maxIdeal k)) (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f)).coeff n✝ =
    (∏ i, map (Ideal.Quotient.mk (maxIdeal k)) (X - C (MvPolynomial.X ⟨f, i⟩))).coeff n✝
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ IsSymm (B₁.tmul B₂)

Tactic:
LinearMap.isSymm_iff_eq_flip

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ B₁.tmul B₂ = LinearMap.flip (B₁.tmul B₂)
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ) ↑l
hm : m ∈ p
h₁ : MapsTo ⇑g ↑p ↑p
h₂ : MapsTo ⇑(g - (algebraMap R (End R M)) μ) ↑p ↑p
h₃ : MapsTo ⇑(f - g) ↑p ↑p
h₄ : MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑p ↑p
hfg : Commute (f - (algebraMap R (End R M)) μ) (f - g)
this : IsNilpotent (LinearMap.restrict (g - (algebraMap R (End R M)) μ) h₂)
⊢ IsFinitelySemisimple (LinearMap.restrict g h₁ - (algebraMap R (End R ↥p)) μ)

Tactic:
by simpa using hss.restrict _

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ 0 < Nat.find ⋯

Tactic:
zero_lt_iff

Goal state after:
R : Type u_1
L : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ Nat.find ⋯ ≠ 0
Module: Mathlib.Algebra.Lie.Weights.Killing

Goal state before:
pp: case mem
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0
y✝ : L
β : ↥H → K
y : L
hy : y ∈ rootSpace H β
⊢ ((killingForm K L) x) y = 0 y

Tactic:
by_cases hαβ : α + β = 0
    · exact hx' _ (add_eq_zero_iff_neg_eq.mp hαβ ▸ hy)
    · exact killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero K L H hx hy hαβ

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
⊢ S ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, S z⁆

Tactic:
aux hz,

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
x : L
hx : x ∈ H
N S : End K L
hN : _root_.IsNilpotent ((ad K L) x - S)
hS : S.IsSemisimple
hSN : (ad K L) x = N + S
hS₀ : Commute ((ad K L) x) S
x' : ↥H := ⟨x, hx⟩
aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y
y z : L
α β : ↥H → K
hy : y ∈ rootSpace H α
hz : z ∈ rootSpace H β
hyz : ⁅y, z⁆ ∈ rootSpace H (α + β)
⊢ S ⁅y, z⁆ = ⁅α x' • y, z⁆ + ⁅y, β x' • z⁆