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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : K
hx : x ∈ adjoin F S
E : IntermediateField F L := ⨆ x, adjoin F ((minpoly F ↑x).rootSet L)
normal : Normal F ↥E
⊢ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits

Tactic:
have : ∀ x ∈ S, ((minpoly F x).map (algebraMap F E)).Splits := fun x hx ↦ splits_of_splits
    (splits x hx).2 fun y hy ↦ (le_iSup _ ⟨x, hx⟩ : _ ≤ E) (subset_adjoin F _ <| by exact hy)

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : K
hx : x ∈ adjoin F S
E : IntermediateField F L := ⨆ x, adjoin F ((minpoly F ↑x).rootSet L)
normal : Normal F ↥E
this : ∀ x ∈ S, (Polynomial.map (algebraMap F ↥E) (minpoly F x)).Splits
⊢ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = ιEE' β
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)

Tactic:
← eq_X_sub_C_of_separable_of_root_eq h_sep h_root h_splits h_roots

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = ιEE' β
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = h
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: F✝ : Type u_1
K✝ : Type u_2
inst✝¹² : Field F✝
inst✝¹¹ : Field K✝
inst✝¹⁰ : Algebra F✝ K✝
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝⁹ : Field K₁
inst✝⁸ : Field K₂
inst✝⁷ : Field K₃
inst✝⁶ : Algebra F✝ K₁
inst✝⁵ : Algebra F✝ K₂
inst✝⁴ : Algebra F✝ K₃
ϕ : K₁ →ₐ[F✝] K₂
χ : K₁ ≃ₐ[F✝] K₂
ψ : K₂ →ₐ[F✝] K₃
ω : K₂ ≃ₐ[F✝] K₃
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
x : K
h : (minpoly F x).natDegree < 2
⊢ (minpoly F x).natDegree ≤ 1

Tactic:
Nat.le_iff_lt_add_one

Goal state after:
F✝ : Type u_1
K✝ : Type u_2
inst✝¹² : Field F✝
inst✝¹¹ : Field K✝
inst✝¹⁰ : Algebra F✝ K✝
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝⁹ : Field K₁
inst✝⁸ : Field K₂
inst✝⁷ : Field K₃
inst✝⁶ : Algebra F✝ K₁
inst✝⁵ : Algebra F✝ K₂
inst✝⁴ : Algebra F✝ K₃
ϕ : K₁ →ₐ[F✝] K₂
χ : K₁ ≃ₐ[F✝] K₂
ψ : K₂ →ₐ[F✝] K₃
ω : K₂ ≃ₐ[F✝] K₃
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
x : K
h : (minpoly F x).natDegree < 2
⊢ (minpoly F x).natDegree < 1 + 1
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
x : ↥↑I
⊢ ∑ x_1, ↑x * r ↑x_1 • a x_1 * b x_1 = ↑(LinearMap.id x)

Tactic:
mul_assoc,

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
x : ↥↑I
⊢ ∑ x_1, ↑x * (r ↑x_1 • a x_1 * b x_1) = ↑(LinearMap.id x)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
⊢ I ∈ (Units.map ↑(spanSingleton R)).range

Tactic:
have e' := (mk_eq_one_iff.mp (inv_mem h)).some.symm

Goal state after:
case mp
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
⊢ I ∈ (Units.map ↑(spanSingleton R)).range
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G := fun K ↦ ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩
K K' : IntermediateField F E
heq : g K = g K'
⊢ K = K'

Tactic:
rw [Subtype.mk.injEq] at heq
    apply_fun fun f : E[X] ↦ adjoin F (f.coeffs : Set E) at heq
    simpa only [adjoin_minpoly_coeff_of_exists_primitive_element F hprim] using heq

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
⊢ M = loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅

Tactic:
simp only [ext_iff_indep, loopyOn_ground, loopyOn_indep_iff, and_congr_right_iff]

Goal state after:
α : Type u_1
M : Matroid α
E : Set α
⊢ M.E = E → ((∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = f '' B₀) → Maximal (M.map f hf).Indep B

Tactic:
rintro ⟨B, hB, rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
⊢ Maximal (M.map f hf).Indep (f '' B)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf)✶ = M✶.map f hf

Tactic:
apply ext_isBase (by simp)
  simp only [dual_ground, map_ground, subset_image_iff, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, dual_isBase_iff']
  intro B hB
  simp_rw [← hf.image_sdiff_subset hB, map_image_isBase_iff sdiff_subset,
    map_image_isBase_iff (show B ⊆ M✶.E from hB), dual_isBase_iff hB, and_iff_left_iff_imp]
  exact fun _ ↦ ⟨B, hB, rfl⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) → M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ range ⇑f

Tactic:
rintro ⟨B, hB, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set α
hB : M.IsBase B
⊢ M.IsBase (⇑f ⁻¹' ⇑f '' B) ∧ ⇑f '' B ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ ¬M.Indep {e} ↔ M.IsLoop e

Tactic:
rw [← singleton_dep, ← not_indep_iff]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.IsBasis' I X
⊢ M.eRk X ≤ n

Tactic:
← hI.encard_eq_eRk

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.IsBasis' I X
⊢ I.encard ≤ n
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
⊢ M.IsNonloop (f e) ∧ InjOn f {e} ↔ M.IsNonloop (f e)

Tactic:
and_iff_left (injOn_singleton _ _)

Goal state after:
α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
⊢ M.IsNonloop (f e) ↔ M.IsNonloop (f e)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X ∩ (M.E \ M.loops)) = M.closure X

Tactic:
← inter_sdiff_assoc,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure ((X ∩ M.E) \ M.loops) = M.closure X
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_5
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ i, C i) \ range x, M.IsCircuit C' ∧ z ∈ C'

Tactic:
obtain ⟨C', hC'ss, hC', hzC'⟩ := hwin

Goal state after:
case refine_5
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ i, C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
I : Set α
inst✝ : M.RankFinite
h : M.eRk I = I.encard
hinf : I.Infinite
⊢ M.Indep I

Tactic:
rw [hinf.encard_eq] at h

Goal state after:
case inr
α : Type u_1
M : Matroid α
I : Set α
inst✝ : M.RankFinite
h : M.eRk I = ⊤
hinf : I.Infinite
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X : Set α
⊢ (M.comap f).eRk X = M.eRk (f '' X)

Tactic:
obtain ⟨I, hI⟩ := (M.comap f).exists_isBasis' X

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X I : Set α
hI : (M.comap f).IsBasis' I X
⊢ (M.comap f).eRk X = M.eRk (f '' X)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hIX : M.IsBasis' I X
⊢ X ∩ M.coloops ⊆ I

Tactic:
by
  intro e ⟨heX, (heI : M.IsColoop e)⟩
  rwa [← heI.mem_closure_iff_mem, hIX.isBasis_closure_right.closure_eq_right,
    heI.mem_closure_iff_mem]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X K : Set α
hXK : Disjoint X K
hK : K ⊆ M.coloops
⊢ X ∩ K = ∅

Tactic:
← disjoint_iff_inter_eq_empty

Goal state after:
α : Type u_1
M : Matroid α
X K : Set α
hXK : Disjoint X K
hK : K ⊆ M.coloops
⊢ Disjoint X K
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hIX : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ #↑I ≤ M.cRk Y

Tactic:
exact (mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cRk

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X : Set α
⊢ (M.comap f).closure X = f ⁻¹' M.closure (f '' X)

Tactic:
obtain ⟨I, hI⟩ := (M.comap f).exists_isBasis' X

Goal state after:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
⊢ (M.comap f).closure X = f ⁻¹' M.closure (f '' X)
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
⊢ h • (fixedBy α g)ᶜ = (fixedBy α g)ᶜ

Tactic:
Set.smul_set_compl,

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
⊢ (h • fixedBy α g)ᶜ = (fixedBy α g)ᶜ
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case pos
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : Injective ⇑(algebraMap R A)
this : IsDomain A
⊢ trdeg R A ≤ #↑s

Tactic:
have := (faithfulSMul_iff_algebraMap_injective R A).mpr h

Goal state after:
case pos
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : Injective ⇑(algebraMap R A)
this✝ : IsDomain A
this : FaithfulSMul R A
⊢ trdeg R A ≤ #↑s
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
this : (f.aroots f.SplittingField).card ≤ f.natDegree
⊢ f.natSepDegree ≤ f.natDegree

Tactic:
classical
  exact (f.aroots f.SplittingField).toFinset_card_le.trans this

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ 0 = g.natSepDegree ↔ 0 = 0 ∧ g = 0 ∨ IsUnit g

Tactic:
isUnit_iff,

Goal state after:
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ 0 = g.natSepDegree ↔ 0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ U ∈ 𝓝 1

Tactic:
by
  rw [B.nhds_one_hasBasis.mem_iff]
  exact ⟨U, hU, rfl.subset⟩

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
this : IsTopologicalGroup G
⊢ closure[t] {1} = {1} ↔ ⋂₀ F.sets = {1}

Tactic:
R0Space.closure_singleton,

Goal state after:
G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
this : IsTopologicalGroup G
⊢ (𝓝 1).ker = {1} ↔ ⋂₀ F.sets = {1}
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
K L : IntermediateField F E
le : K ≤ L
x : E
hx : x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) K
⊢ x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) L

Tactic:
let _ := (inclusion le).toAlgebra
    have : IsScalarTower K L E := .of_algebraMap_eq' rfl
    exact hx.tower_top _

Goal state after:
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional K ↥K⟮x⟯
⊢ τ ∈ (σ • ↑E.fixingSubgroup)ᶜ

Tactic:
simp only [Set.mem_compl_iff, mem_leftCoset_iff, SetLike.mem_coe,
    IntermediateField.mem_fixingSubgroup_iff, not_forall]

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional K ↥K⟮x⟯
⊢ ∃ x, ∃ (_ : x ∈ E), ¬(σ⁻¹ * τ) x = x
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g' : R[X]
hg' : map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
⊢ g * C g.leadingCoeff⁻¹ * C g.leadingCoeff = g

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g' : R[X]
hg' : map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
⊢ g * (C g.leadingCoeff⁻¹ * C g.leadingCoeff) = g
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: case a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i, f i • b i ∈ Submodule.span R (Set.range ⇑b)
j : ι
⊢ (algebraMap R S) (f j) • (B ((B.dualBasis hB b) i)) (b j) ∈ 1

Tactic:
apply_dualBasis_left

Goal state after:
case a
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
i : ι
f : ι → R
hy : ∑ i, f i • b i ∈ Submodule.span R (Set.range ⇑b)
j : ι
⊢ ((algebraMap R S) (f j) • if j = i then 1 else 0) ∈ 1
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x✝ : Algebra K L := FractionRing.liftAlgebra R L
this : minpoly K ((algebraMap S L) s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)
⊢ minpoly R s ∣ p

Tactic:
rw [isIntegrallyClosed_eq_field_fractions _ _ hs,
    map_dvd_map (algebraMap R K) (IsFractionRing.injective R K) (minpoly.monic hs)] at this

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x✝ : Algebra K L := FractionRing.liftAlgebra R L
this : minpoly R s ∣ p %ₘ minpoly R s
⊢ minpoly R s ∣ p
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H :
  Polynomial.map (algebraMap R K) p =
    Polynomial.map (algebraMap R K) a' * C a.leadingCoeff * (C b.leadingCoeff * Polynomial.map (algebraMap R K) b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H :
  Polynomial.map (algebraMap R K) p =
    Polynomial.map (algebraMap R K) a' * (C a.leadingCoeff * (C b.leadingCoeff * Polynomial.map (algebraMap R K) b'))
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree + 1 = (minpoly R x).natDegree

Tactic:
by
  rw [← (minpoly.monic hx).natDegree_map (algebraMap R S), ← minpolyDiv_spec, natDegree_mul']
  · simp
  · simpa using minpolyDiv_ne_zero hx

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case hu.inr
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
con : ↑u = 0
⊢ False

Tactic:
apply Units.ne_zero _ con

Goal state after:
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
H : (ClosedSubgroup Gal(K/k))ᵒᵈ
⊢ (fun L ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ }) ((fun H ↦ IntermediateField.fixedField ↑H) H) = H

Tactic:
simp_rw [fixingSubgroup_fixedField H]
    rfl

Goal state after: