awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮x⟯
h : ¬n + 1 < finrank.{u_1, u_2} F ↥L'
⊢ False
have h1 : L = L'
Tactic: have h1 : L = L' := eq_of_le_of_finrank_le le_sup_left ((not_lt.1 h).trans hn)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮x⟯
h : ¬n + 1 < finrank.{u_1, u_2} F ↥L'
h1 : L = L'
⊢ False
have h2 : F⟮x⟯ ≤ L'
Tactic: have h2 : F⟮x⟯ ≤ L' := le_sup_right
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
⊢ ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ n < finrank.{u_1, u_2} F ↥L
have zero : ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ 0 < finrank.{u_1, u_2} F ↥L
Tactic: induction n with
  | zero => exact ⟨⊥, Subalgebra.finite_bot, finrank_pos⟩
  | succ n ih =>
    obtain ⟨L, fin, hn⟩ := ih
    obtain ⟨x, hx⟩ : ∃ x : E, x ∉ L := by
      contrapose! hnfd
      rw [show L = ⊤ from eq_top_iff.2 fun x _ ↦ hnfd x] at fin
      exact topEquiv.toLinearEquiv.finiteDimensional
    let L' := L ⊔ F⟮x⟯
    haveI := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) x)
    refine ⟨L', inferInstance, by_contra fun h ↦ ?_⟩
    have h1 : L = L' := eq_of_le_of_finrank_le le_sup_left ((not_lt.1 h).trans hn)
    have h2 : F⟮x⟯ ≤ L' := le_sup_right
    exact hx <| (h1.symm ▸ h2) <| mem_adjoin_simple_self F x
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
zero : ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ 0 < finrank.{u_1, u_2} F ↥L
⊢ ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ n < finrank.{u_1, u_2} F ↥L
have succ : ∀ (n : ℕ) (ih : ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ n < finrank.{u_1, u_2} F ↥L),
  ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ n + 1 < finrank.{u_1, u_2} F ↥L
Tactic: induction n with
  | zero => exact ⟨⊥, Subalgebra.finite_bot, finrank_pos⟩
  | succ n ih =>
    obtain ⟨L, fin, hn⟩ := ih
    obtain ⟨x, hx⟩ : ∃ x : E, x ∉ L := by
      contrapose! hnfd
      rw [show L = ⊤ from eq_top_iff.2 fun x _ ↦ hnfd x] at fin
      exact topEquiv.toLinearEquiv.finiteDimensional
    let L' := L ⊔ F⟮x⟯
    haveI := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) x)
    refine ⟨L', inferInstance, by_contra fun h ↦ ?_⟩
    have h1 : L = L' := eq_of_le_of_finrank_le le_sup_left ((not_lt.1 h).trans hn)
    have h2 : F⟮x⟯ ≤ L' := le_sup_right
    exact hx <| (h1.symm ▸ h2) <| mem_adjoin_simple_self F x
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
⊢ natDegree (minpoly K x) ∣ finrank K L
have rw : ∃ (c : ℕ), finrank K L = c * finrank.{u, u_3} K ↥K⟮x⟯
Tactic: rw [dvd_iff_exists_eq_mul_left, ← IntermediateField.adjoin.finrank hx]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
⊢ ∃ (c : ℕ), finrank K L = c * finrank.{u, u_3} K ↥K⟮x⟯
have h : finrank K L = finrank (↥K⟮x⟯) L * finrank.{u, u_3} K ↥K⟮x⟯
Tactic: use finrank K⟮x⟯ L
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
⊢ finrank K L = finrank (↥K⟮x⟯) L * finrank.{u, u_3} K ↥K⟮x⟯
have h : finrank K L = finrank.{u, u_3} K ↥K⟮x⟯ * finrank (↥K⟮x⟯) L
Tactic: rw [mul_comm, finrank_mul_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
h : finrank K L = finrank.{u, u_3} K ↥K⟮x⟯ * finrank (↥K⟮x⟯) L
⊢ finrank K L = finrank (↥K⟮x⟯) L * finrank.{u, u_3} K ↥K⟮x⟯
have h₁ : finrank K L = finrank K L
Tactic: rw [mul_comm, finrank_mul_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
⊢ f.natDegree ∣ finrank K L
have this : f.degree ≠ 0
Tactic: have := hi.degree_pos.ne'
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
this : f.degree ≠ 0
⊢ f.natDegree ∣ finrank K L
have this₁ : degree (Polynomial.map (algebraMap K L) f) ≠ 0
Tactic: rw [← f.degree_map (algebraMap K L)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
⊢ f.natDegree ∣ finrank K L
have obtain : ∀ (x : L) (hx : eval x (Polynomial.map (algebraMap K L) f) = 0), f.natDegree ∣ finrank K L
Tactic: obtain ⟨x, hx⟩ := hs.exists_eval_eq_zero this
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : eval x (Polynomial.map (algebraMap K L) f) = 0
⊢ f.natDegree ∣ finrank K L
have hx₁ : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
Tactic: rw [eval_map_algebraMap] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
⊢ f.natDegree ∣ finrank K L
have key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
Tactic: have key := minpoly.Irreducible.eq_minpoly hi hx
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
⊢ f.natDegree ∣ finrank K L
have hi₁ : f ≠ 0
Tactic: replace hi := hi.ne_zero
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
hi : f ≠ 0
⊢ f.natDegree ∣ finrank K L
have rw : natDegree (minpoly K x) ∣ finrank K L
Tactic: rw [key, natDegree_C_mul (leadingCoeff_ne_zero.mpr hi)]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
hi : f ≠ 0
⊢ natDegree (minpoly K x) ∣ finrank K L
have hx₁ : IsIntegral K x
Tactic: apply minpoly.degree_dvd
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
hi : f ≠ 0
⊢ IsIntegral K x
have hx₁ : Ne (α := K[X]) (minpoly K x) 0
Tactic: rw [← minpoly.ne_zero_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
hi : f ≠ 0
⊢ Ne (α := K[X]) (minpoly K x) 0
have hx₁ : ∀ (hi : Eq (α := K[X]) (minpoly K x) 0), f = 0
Tactic: contrapose hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
hi : Eq (α := K[X]) (minpoly K x) 0
⊢ f = 0
have hx₁ : ∀ (key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (0 : K[X]))
  (hi : Eq (α := K[X]) (minpoly K x) 0), f = 0
Tactic: rwa [hi, mul_zero] at key
Cleared hypotheses: key, hi
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
hi : Eq (α := K[X]) (minpoly K x) 0
hx₁ :
  ∀ (key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (0 : K[X]))
    (hi : Eq (α := K[X]) (minpoly K x) 0), f = 0
⊢ f = 0
have hx₂ : ∀ (key : f = 0) (hi : Eq (α := K[X]) (minpoly K x) 0), f = 0
Tactic: rwa [hi, mul_zero] at key
Cleared hypotheses: key, hi
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic.{u, u_3} K ↥(t i)
⊢ Algebra.IsAlgebraic.{u, u_3} K ↥(⨆ (i : ι), t i)
have isAlgebraic : ∀ (x : ↥(⨆ (i : ι), t i)), IsAlgebraic K x
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic.{u, u_3} K ↥(t i)
x : L
hx : Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x
⊢ IsAlgebraic K (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x) x hx)
have isAlgebraic : ∀ (s : Finset ((i : ι) × ↥(t i)))
  (hx_1 : Membership.mem (γ := IntermediateField K L) (⨆ i ∈ s, K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯) x),
  IsAlgebraic K (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x) x hx)
Tactic: obtain ⟨s, hx⟩ := exists_finset_of_mem_supr' hx
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic.{u, u_3} K ↥(t i)
x : L
hx_1 : Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x
s : Finset ((i : ι) × ↥(t i))
hx : Membership.mem (γ := IntermediateField K L) (⨆ i ∈ s, K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯) x
⊢ IsAlgebraic K (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x) x hx_1)
have isAlgebraic : IsAlgebraic K
  (Subtype.mk (p := fun (x : L) ↦
    Membership.mem (γ := IntermediateField K L) (⨆ i ∈ s, K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯) x) x hx)
Tactic: rw [isAlgebraic_iff, Subtype.coe_mk, ← Subtype.coe_mk (p := (· ∈ _)) x hx, ← isAlgebraic_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic.{u, u_3} K ↥(t i)
x : L
hx_1 : Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x
s : Finset ((i : ι) × ↥(t i))
hx : Membership.mem (γ := IntermediateField K L) (⨆ i ∈ s, K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯) x
⊢ IsAlgebraic K
    (Subtype.mk (p := fun (x : L) ↦
      Membership.mem (γ := IntermediateField K L) (⨆ i ∈ s, K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯) x) x hx)
have this : ∀ (i : (i : ι) × ↥(t i)), FiniteDimensional.{u, u_3} K ↥K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯
Tactic: haveI : ∀ i : Σ i, t i, FiniteDimensional K K⟮(i.2 : L)⟯ := fun ⟨i, x⟩ ↦
    adjoin.finiteDimensional (isIntegral_iff.1 (Algebra.IsIntegral.isIntegral x))
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
S : Set L
hS : ∀ x ∈ S, IsIntegral K x
⊢ Algebra.IsAlgebraic.{u, u_3} K ↥(adjoin K S)
have rw : Algebra.IsAlgebraic.{u, u_3} K ↥(⨆ (i : (↑S : Type u_3)), K⟮(↑i : L)⟯)
Tactic: rw [← biSup_adjoin_simple, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
S : Set L
inst_3 : Finite.{u_3 + 1} (↑S : Type u_3)
hS : ∀ x ∈ S, IsIntegral K x
⊢ FiniteDimensional.{u, u_3} K ↥(adjoin K S)
have rw : FiniteDimensional.{u, u_3} K ↥(⨆ (i : (↑S : Type u_3)), K⟮(↑i : L)⟯)
Tactic: rw [← biSup_adjoin_simple, ← iSup_subtype'']
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
S : Set L
inst_3 : Finite.{u_3 + 1} (↑S : Type u_3)
hS : ∀ x ∈ S, IsIntegral K x
⊢ FiniteDimensional.{u, u_3} K ↥(⨆ (i : (↑S : Type u_3)), K⟮(↑i : L)⟯)
have this : ∀ (x : (↑S : Type u_3)), FiniteDimensional.{u, u_3} K ↥K⟮(↑x : L)⟯
Tactic: haveI (x : S) := adjoin.finiteDimensional (hS x.1 x.2)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
x : K
⊢ x ∈ aroots (minpoly F (adjoin.powerBasis h).gen) K ↔
    Membership.mem (α := K) (aroots (minpoly F α) K) ((Equiv.refl K : (a : K) → K) x : K)
have rw : x ∈ aroots (minpoly F (B := ↥F⟮α⟯) (AdjoinSimple.gen F α)) K ↔
  Membership.mem (α := K) (aroots (minpoly F α) K) ((Equiv.refl K : (a : K) → K) x : K)
Tactic: rw [adjoin.powerBasis_gen, minpoly_gen, Equiv.refl_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
x : K
rw :
  x ∈ aroots (minpoly F (B := ↥F⟮α⟯) (AdjoinSimple.gen F α)) K ↔
    Membership.mem (α := K) (aroots (minpoly F α) K) ((Equiv.refl K : (a : K) → K) x : K)
⊢ x ∈ aroots (minpoly F (adjoin.powerBasis h).gen) K ↔
    Membership.mem (α := K) (aroots (minpoly F α) K) ((Equiv.refl K : (a : K) → K) x : K)
have rw₁ : x ∈ aroots (minpoly F α) K ↔ Membership.mem (α := K) (aroots (minpoly F α) K) ((Equiv.refl K : (a : K) → K) x : K)
Tactic: rw [adjoin.powerBasis_gen, minpoly_gen, Equiv.refl_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
x : K
rw :
  x ∈ aroots (minpoly F (B := ↥F⟮α⟯) (AdjoinSimple.gen F α)) K ↔
    Membership.mem (α := K) (aroots (minpoly F α) K) ((Equiv.refl K : (a : K) → K) x : K)
rw₁ : x ∈ aroots (minpoly F α) K ↔ Membership.mem (α := K) (aroots (minpoly F α) K) ((Equiv.refl K : (a : K) → K) x : K)
⊢ x ∈ aroots (minpoly F (adjoin.powerBasis h).gen) K ↔
    Membership.mem (α := K) (aroots (minpoly F α) K) ((Equiv.refl K : (a : K) → K) x : K)
have rw₂ : x ∈ aroots (minpoly F α) K ↔ x ∈ aroots (minpoly F α) K
Tactic: rw [adjoin.powerBasis_gen, minpoly_gen, Equiv.refl_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
x : { x : K // x ∈ aroots (minpoly F α) K }
⊢ Eq.{u + 1} (α := K) ((aeval (↑x : K) : (a : F[X]) → K) (minpoly F (adjoin.powerBasis h).gen) : K) (0 : K)
have rw : Eq.{u + 1} (α := K) ((aeval (↑x : K) : (a : F[X]) → K) (minpoly F α) : K) (0 : K)
Tactic: rw [adjoin.powerBasis_gen, minpoly_gen]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Splits (Polynomial.map (algebraMap F K) (minpoly F α))
x : Fintype (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ Nat.card (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) = natDegree (minpoly F α)
have rw : (adjoin.powerBasis h).dim = natDegree (minpoly F α)
Tactic: rw [Nat.card_eq_fintype_card, AlgHom.card_of_powerBasis]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Splits (Polynomial.map (algebraMap F K) (minpoly F α))
x : Fintype (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) := fintypeOfAlgHomAdjoinIntegral F h
rw : (adjoin.powerBasis h).dim = natDegree (minpoly F α)
⊢ Nat.card (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) = natDegree (minpoly F α)
have h_sep₁ : IsSeparable F (adjoin.powerBasis h).gen
Tactic: rw [Nat.card_eq_fintype_card, AlgHom.card_of_powerBasis]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Splits (Polynomial.map (algebraMap F K) (minpoly F α))
x : Fintype (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) := fintypeOfAlgHomAdjoinIntegral F h
rw : (adjoin.powerBasis h).dim = natDegree (minpoly F α)
h_sep₁ : IsSeparable F (adjoin.powerBasis h).gen
⊢ Nat.card (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) = natDegree (minpoly F α)
have h_splits₁ : Splits (Polynomial.map (algebraMap F K) (minpoly F (adjoin.powerBasis h).gen))
Tactic: rw [Nat.card_eq_fintype_card, AlgHom.card_of_powerBasis]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Splits (Polynomial.map (algebraMap F K) (minpoly F α))
x : Fintype (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ IsSeparable F (adjoin.powerBasis h).gen
have h_sep₁ : Separable (minpoly F α)
Tactic: simp only [IsSeparable, adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen, h_splits]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
⊢ Irreducible (f.comp g)
have hf' : f.natDegree ≠ 0
Tactic: have hf' : natDegree f ≠ 0 :=
    fun e ↦ not_irreducible_C (f.coeff 0) (eq_C_of_natDegree_eq_zero e ▸ hf)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
⊢ g.natDegree ≠ 0
have this : Fact (Irreducible f)
Tactic: have := Fact.mk hf
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
this : Fact (Irreducible f)
e : g.natDegree = 0
⊢ False
have apply : Irreducible (M := (↥K⟮root f⟯)[X])
  ((C : (a : ↥K⟮root f⟯) → (↥K⟮root f⟯)[X])
      (HSub.hSub (α := ↥K⟮root f⟯) (coeff (Polynomial.map (algebraMap K ↥K⟮root f⟯) g) 0)
        (AdjoinSimple.gen K (root f))) :
    (↥K⟮root f⟯)[X])
Tactic: apply not_irreducible_C ((g.map (algebraMap _ _)).coeff 0 - AdjoinSimple.gen K (root f))