awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 : natSepDegree (minpoly F x) = 1
n : ℕ
y : F
h : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hx : (algebraMap F E : (a : F) → E) y = x ^ q ^ n
h₁ :
  Polynomial.map (algebraMap F E)
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₂ :
  HSub.hSub (α := E[X]) (Polynomial.map (algebraMap F E) (HPow.hPow (α := F[X]) X (q ^ n)))
      (Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y)) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₃ :
  HPow.hPow (α := E[X]) (Polynomial.map (algebraMap F E : F →+* E) X) (q ^ n) -
      Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₄ :
  HPow.hPow (α := E[X]) X (q ^ n) - Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
⊢ Polynomial.map (algebraMap F E) (minpoly F x) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
have h₅ : HSub.hSub (β := E[X]) (HPow.hPow (α := E[X]) X (q ^ n))
    ((C : (a : E) → E[X]) (((algebraMap F E : F →+* E) : (a : F) → E) y) : E[X]) =
  HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
Tactic: rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 : natSepDegree (minpoly F x) = 1
n : ℕ
y : F
h : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hx : (algebraMap F E : (a : F) → E) y = x ^ q ^ n
h₁ :
  Polynomial.map (algebraMap F E)
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₂ :
  HSub.hSub (α := E[X]) (Polynomial.map (algebraMap F E) (HPow.hPow (α := F[X]) X (q ^ n)))
      (Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y)) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₃ :
  HPow.hPow (α := E[X]) (Polynomial.map (algebraMap F E : F →+* E) X) (q ^ n) -
      Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₄ :
  HPow.hPow (α := E[X]) X (q ^ n) - Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₅ :
  HSub.hSub (β := E[X]) (HPow.hPow (α := E[X]) X (q ^ n))
      ((C : (a : E) → E[X]) (((algebraMap F E : F →+* E) : (a : F) → E) y) : E[X]) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
⊢ Polynomial.map (algebraMap F E) (minpoly F x) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
have h₆ : HSub.hSub (β := E[X]) (HPow.hPow (α := E[X]) X (q ^ n)) ((C : (a : E) → E[X]) (x ^ q ^ n) : E[X]) =
  HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
Tactic: rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 : natSepDegree (minpoly F x) = 1
n : ℕ
y : F
h : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hx : (algebraMap F E : (a : F) → E) y = x ^ q ^ n
h₁ :
  Polynomial.map (algebraMap F E)
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₂ :
  HSub.hSub (α := E[X]) (Polynomial.map (algebraMap F E) (HPow.hPow (α := F[X]) X (q ^ n)))
      (Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y)) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₃ :
  HPow.hPow (α := E[X]) (Polynomial.map (algebraMap F E : F →+* E) X) (q ^ n) -
      Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₄ :
  HPow.hPow (α := E[X]) X (q ^ n) - Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₅ :
  HSub.hSub (β := E[X]) (HPow.hPow (α := E[X]) X (q ^ n))
      ((C : (a : E) → E[X]) (((algebraMap F E : F →+* E) : (a : F) → E) y) : E[X]) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₆ :
  HSub.hSub (β := E[X]) (HPow.hPow (α := E[X]) X (q ^ n)) ((C : (a : E) → E[X]) (x ^ q ^ n) : E[X]) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
⊢ Polynomial.map (algebraMap F E) (minpoly F x) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
have h₇ : HPow.hPow (α := E[X]) X (q ^ n) - HPow.hPow (α := E[X]) ((C : (a : E) → E[X]) x : E[X]) (q ^ n) =
  HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
Tactic: rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 : natSepDegree (minpoly F x) = 1
n : ℕ
y : F
h : minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
hx : (algebraMap F E : (a : F) → E) y = x ^ q ^ n
h₁ :
  Polynomial.map (algebraMap F E)
      (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₂ :
  HSub.hSub (α := E[X]) (Polynomial.map (algebraMap F E) (HPow.hPow (α := F[X]) X (q ^ n)))
      (Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y)) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₃ :
  HPow.hPow (α := E[X]) (Polynomial.map (algebraMap F E : F →+* E) X) (q ^ n) -
      Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₄ :
  HPow.hPow (α := E[X]) X (q ^ n) - Polynomial.map (algebraMap F E : F →+* E) ((C : (a : F) → F[X]) y) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₅ :
  HSub.hSub (β := E[X]) (HPow.hPow (α := E[X]) X (q ^ n))
      ((C : (a : E) → E[X]) (((algebraMap F E : F →+* E) : (a : F) → E) y) : E[X]) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₆ :
  HSub.hSub (β := E[X]) (HPow.hPow (α := E[X]) X (q ^ n)) ((C : (a : E) → E[X]) (x ^ q ^ n) : E[X]) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
h₇ :
  HPow.hPow (α := E[X]) X (q ^ n) - HPow.hPow (α := E[X]) ((C : (a : E) → E[X]) x : E[X]) (q ^ n) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
⊢ Polynomial.map (algebraMap F E) (minpoly F x) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
have h₈ : HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n =
  HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
Tactic: rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow,
      ← sub_pow_expChar_pow_of_commute _ _ (commute_X _)]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h :
  Polynomial.map (algebraMap F E) (minpoly F x) =
    HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have h₁ : Eq (α := E) ((constantCoeff : (a : E[X]) → E) (Polynomial.map (algebraMap F E) (minpoly F x)) : E)
  ((constantCoeff : (a : E[X]) → E) (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n) : E)
Tactic: apply_fun constantCoeff at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h :
  Eq (α := E) ((constantCoeff : (a : E[X]) → E) (Polynomial.map (algebraMap F E) (minpoly F x)) : E)
    ((constantCoeff : (a : E[X]) → E) (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n) : E)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have h₁ : (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = (0 - x) ^ q ^ n
Tactic: simp_rw [map_pow, map_sub, constantCoeff_apply, coeff_map, coeff_X_zero, coeff_C_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h : (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = (0 - x) ^ q ^ n
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have h₁ : (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = -1 * x ^ q ^ n
Tactic: rw [zero_sub, neg_pow, neg_one_pow_expChar_pow] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h : (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = -1 * x ^ q ^ n
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) (-coeff (minpoly F x) 0) = x ^ q ^ n
have rw : -((algebraMap F E : F →+* E) : (a : F) → E) (coeff (minpoly F x) 0) = x ^ q ^ n
Tactic: rw [map_neg, h, neg_mul, one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h : (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = -1 * x ^ q ^ n
rw : -((algebraMap F E : F →+* E) : (a : F) → E) (coeff (minpoly F x) 0) = x ^ q ^ n
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) (-coeff (minpoly F x) 0) = x ^ q ^ n
have rw₁ : -(-1 * x ^ q ^ n) = x ^ q ^ n
Tactic: rw [map_neg, h, neg_mul, one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h : (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = -1 * x ^ q ^ n
rw : -((algebraMap F E : F →+* E) : (a : F) → E) (coeff (minpoly F x) 0) = x ^ q ^ n
rw₁ : -(-1 * x ^ q ^ n) = x ^ q ^ n
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) (-coeff (minpoly F x) 0) = x ^ q ^ n
have rw₂ : - -(1 * x ^ q ^ n) = x ^ q ^ n
Tactic: rw [map_neg, h, neg_mul, one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h : (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = -1 * x ^ q ^ n
rw : -((algebraMap F E : F →+* E) : (a : F) → E) (coeff (minpoly F x) 0) = x ^ q ^ n
rw₁ : -(-1 * x ^ q ^ n) = x ^ q ^ n
rw₂ : - -(1 * x ^ q ^ n) = x ^ q ^ n
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) (-coeff (minpoly F x) 0) = x ^ q ^ n
have rw₃ : - -x ^ q ^ n = x ^ q ^ n
Tactic: rw [map_neg, h, neg_mul, one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this_1 : ExpChar E q
this : ExpChar.{v} E[X] q
h_1 :
  ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
n : ℕ
h : (algebraMap F E : (a : F) → E) (coeff (minpoly F x) 0) = -1 * x ^ q ^ n
rw : -((algebraMap F E : F →+* E) : (a : F) → E) (coeff (minpoly F x) 0) = x ^ q ^ n
rw₁ : -(-1 * x ^ q ^ n) = x ^ q ^ n
rw₂ : - -(1 * x ^ q ^ n) = x ^ q ^ n
rw₃ : - -x ^ q ^ n = x ^ q ^ n
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) (-coeff (minpoly F x) 0) = x ^ q ^ n
have rw₄ : x ^ q ^ n = x ^ q ^ n
Tactic: rw [map_neg, h, neg_mul, one_mul, neg_neg]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = natSepDegree (minpoly F α)
have this : finSepDegree.{u, v} F ↥F⟮α⟯ =
  Nat.card.{v}
    { x : AlgebraicClosure ↥F⟮α⟯ //
      Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x }
Tactic: have : finSepDegree F F⟮α⟯ = _ := Nat.card_congr
    (algHomAdjoinIntegralEquiv F (K := AlgebraicClosure F⟮α⟯) halg.isIntegral)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
this :
  finSepDegree.{u, v} F ↥F⟮α⟯ =
    Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x }
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = natSepDegree (minpoly F α)
have rw : Fintype.card.{v}
    { x : AlgebraicClosure ↥F⟮α⟯ //
      Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
  Fintype.card.{v} ↥(Multiset.toFinset (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)))
Tactic: rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
    ← Fintype.card_coe]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
this :
  finSepDegree.{u, v} F ↥F⟮α⟯ =
    Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x }
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = natSepDegree (minpoly F α)
have rw : Nat.card.{v}
    { x : AlgebraicClosure ↥F⟮α⟯ //
      Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
  natSepDegree (minpoly F α)
Tactic: classical
  rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
    ← Fintype.card_coe]
  simp_rw [Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
this :
  finSepDegree.{u, v} F ↥F⟮α⟯ =
    Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x }
rw :
  Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    natSepDegree (minpoly F α)
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = natSepDegree (minpoly F α)
have rw₁ : Fintype.card.{v}
    { x : AlgebraicClosure ↥F⟮α⟯ //
      Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
  natSepDegree (minpoly F α)
Tactic: classical
  rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
    ← Fintype.card_coe]
  simp_rw [Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
this :
  finSepDegree.{u, v} F ↥F⟮α⟯ =
    Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x }
rw :
  Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    natSepDegree (minpoly F α)
rw₁ :
  Fintype.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    natSepDegree (minpoly F α)
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = natSepDegree (minpoly F α)
have rw₂ : Fintype.card.{v}
    { x : AlgebraicClosure ↥F⟮α⟯ //
      Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
  Finset.card.{v} (α := AlgebraicClosure ↥F⟮α⟯) (Multiset.toFinset (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)))
Tactic: classical
  rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
    ← Fintype.card_coe]
  simp_rw [Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
this :
  finSepDegree.{u, v} F ↥F⟮α⟯ =
    Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x }
rw :
  Nat.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    natSepDegree (minpoly F α)
rw₁ :
  Fintype.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    natSepDegree (minpoly F α)
rw₂ :
  Fintype.card.{v}
      { x : AlgebraicClosure ↥F⟮α⟯ //
        Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
    Finset.card.{v} (α := AlgebraicClosure ↥F⟮α⟯) (Multiset.toFinset (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)))
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = natSepDegree (minpoly F α)
have rw₃ : Fintype.card.{v}
    { x : AlgebraicClosure ↥F⟮α⟯ //
      Membership.mem (γ := Multiset (AlgebraicClosure ↥F⟮α⟯)) (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)) x } =
  Fintype.card.{v} ↥(Multiset.toFinset (aroots (minpoly F α) (AlgebraicClosure ↥F⟮α⟯)))
Tactic: classical
  rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
    ← Fintype.card_coe]
  simp_rw [Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯
have pos : ∀ (halg : IsAlgebraic F α), finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯
Tactic: by_cases halg : IsAlgebraic F α
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
pos : ∀ (halg : IsAlgebraic F α), finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯
have neg : ∀ (halg : ¬IsAlgebraic F α), finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯
Tactic: by_cases halg : IsAlgebraic F α
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯
have pos : natSepDegree (minpoly F α) ∣ natDegree (minpoly F α)
Tactic: rw [finSepDegree_adjoin_simple_eq_natSepDegree F E halg, adjoin.finrank halg.isIntegral]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : ¬IsAlgebraic F α
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯
have this : finrank.{u, v} F ↥F⟮α⟯ = 0
Tactic: have : finrank F F⟮α⟯ = 0 := finrank_of_infinite_dimensional fun _ ↦
    halg ((AdjoinSimple.isIntegral_gen F α).1 (IsIntegral.of_finite F _)).isAlgebraic
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : ¬IsAlgebraic F α
this : finrank.{u, v} F ↥F⟮α⟯ = 0
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ∣ finrank.{u, v} F ↥F⟮α⟯
have neg : finSepDegree.{u, v} F ↥F⟮α⟯ ∣ 0
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ ≤ finrank.{u, v} F ↥F⟮α⟯
have this : FiniteDimensional.{u, v} F ↥F⟮α⟯
Tactic: haveI := adjoin.finiteDimensional halg.isIntegral
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ finSepDegree.{u, v} F ↥F⟮α⟯ = finrank.{u, v} F ↥F⟮α⟯ ↔ IsSeparable F α
have rw : natSepDegree (minpoly F α) = finrank.{u, v} F ↥F⟮α⟯ ↔ IsSeparable F α
Tactic: rw [finSepDegree_adjoin_simple_eq_natSepDegree F E halg, adjoin.finrank halg.isIntegral,
    natSepDegree_eq_natDegree_iff _ (minpoly.ne_zero halg.isIntegral), IsSeparable]