awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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])
have rw : Irreducible
  (HSub.hSub (α := (↥K⟮root f⟯)[X]) (β := (↥K⟮root f⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮root f⟯) g)
    ((C : (a : ↥K⟮root f⟯) → (↥K⟮root f⟯)[X]) (AdjoinSimple.gen K (root f)) : (↥K⟮root f⟯)[X]))
Tactic: rw [RingHom.map_sub, coeff_map, ← map_C, ← eq_C_of_natDegree_eq_zero e]
-- 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
⊢ Irreducible
    (HSub.hSub (α := (↥K⟮root f⟯)[X]) (β := (↥K⟮root f⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮root f⟯) g)
      ((C : (a : ↥K⟮root f⟯) → (↥K⟮root f⟯)[X]) (AdjoinSimple.gen K (root f)) : (↥K⟮root f⟯)[X]))
have x : minpoly K (root f) = f
Tactic: apply hg (AdjoinRoot f)
-- 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
⊢ minpoly K (root f) = f
have x : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
Tactic: rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]
-- 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
x : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
⊢ minpoly K (root f) = f
have x₁ : f * (C : (a : K) → K[X]) 1⁻¹ = f
Tactic: rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]
-- 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
x : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
x₁ : f * (C : (a : K) → K[X]) 1⁻¹ = f
⊢ minpoly K (root f) = f
have x₂ : f * (C : (a : K) → K[X]) 1 = f
Tactic: rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]
-- 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
x : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
x₁ : f * (C : (a : K) → K[X]) 1⁻¹ = f
x₂ : f * (C : (a : K) → K[X]) 1 = f
⊢ minpoly K (root f) = f
have x₃ : f * 1 = f
Tactic: rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]
-- 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
x : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
x₁ : f * (C : (a : K) → K[X]) 1⁻¹ = f
x₂ : f * (C : (a : K) → K[X]) 1 = f
x₃ : f * 1 = f
⊢ minpoly K (root f) = f
have x₄ : f = f
Tactic: rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]
-- 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
⊢ Irreducible (f.comp g)
have hg' : g.natDegree ≠ 0
Tactic: have hg' : natDegree g ≠ 0 := by
    have := Fact.mk hf
    intro e
    apply not_irreducible_C ((g.map (algebraMap _ _)).coeff 0 - AdjoinSimple.gen K (root f))
    -- Needed to specialize `map_sub` to avoid a timeout https://github.com/leanprover-community/mathlib4/pull/8386
    rw [RingHom.map_sub, coeff_map, ← map_C, ← eq_C_of_natDegree_eq_zero e]
    apply hg (AdjoinRoot f)
    rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]
-- 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
hg' : g.natDegree ≠ 0
⊢ Irreducible (f.comp g)
have H₁ : f.comp g ≠ 0
Tactic: have H₁ : f.comp g ≠ 0 := fun h ↦ by simpa [hf', hg', natDegree_comp] using congr_arg natDegree h
-- 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
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
⊢ Irreducible (f.comp g)
have H₂ : ¬IsUnit (f.comp g)
Tactic: have H₂ : ¬ IsUnit (f.comp g) := fun h ↦
    by simpa [hf', hg', natDegree_comp] using natDegree_eq_zero_of_isUnit h
-- 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
hg' : g.natDegree ≠ 0
H₁ : f.comp g ≠ 0
H₂ : ¬IsUnit (f.comp g)
⊢ Irreducible (f.comp g)
have have : ∀ (p : K[X]) (hp₁ : Irreducible p) (hp₂ : p ∣ f.comp g), Irreducible (f.comp g)
Tactic: have ⟨p, hp₁, hp₂⟩ := WfDvdMonoid.exists_irreducible_factor H₂ H₁
-- 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
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
⊢ Irreducible (f.comp g)
have suffices : p.natDegree = f.natDegree * g.natDegree
Tactic: suffices natDegree p = natDegree f * natDegree g from (associated_of_dvd_of_natDegree_le hp₂ H₁
    (this.trans natDegree_comp.symm).ge).irreducible hp₁
-- 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
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
⊢ p.natDegree = f.natDegree * g.natDegree
have this : Fact (Irreducible p)
Tactic: have := Fact.mk hp₁
-- 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
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_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
⊢ f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
have refine : Eq (α := AdjoinRoot p)
  (((aeval ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g) : K[X] →ₐ[K] AdjoinRoot p) : (a : K[X]) → AdjoinRoot p) f :
    AdjoinRoot p)
  (0 : AdjoinRoot p)
Tactic: refine minpoly.eq_of_irreducible_of_monic hf ?_ hfm
-- 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
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_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
⊢ Eq (α := AdjoinRoot p)
    (((aeval ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g) : K[X] →ₐ[K] AdjoinRoot p) : (a : K[X]) → AdjoinRoot p)
        f :
      AdjoinRoot p)
    (0 : AdjoinRoot p)
have rw : Eq (α := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) (f.comp g) : AdjoinRoot p) (0 : AdjoinRoot p)
Tactic: rw [← aeval_comp]
-- 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
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_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
⊢ p.natDegree = f.natDegree * g.natDegree
have key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
Tactic: have key₁ : f = minpoly K (aeval (root p) g) := by
    refine minpoly.eq_of_irreducible_of_monic hf ?_ hfm
    rw [← aeval_comp]
    exact aeval_eq_zero_of_dvd_aeval_eq_zero hp₂ (AdjoinRoot.eval₂_root p)
-- 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
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_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
⊢ finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree
have rw : IsIntegral K (A := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
Tactic: rw [adjoin.finrank, ← key₁]
-- 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
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_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
⊢ p.natDegree = f.natDegree * g.natDegree
have key₁' : finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree
Tactic: have key₁' : finrank K K⟮aeval (root p) g⟯ = natDegree f := by
    rw [adjoin.finrank, ← key₁]
    exact IsIntegral.of_finite _ _
-- 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
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_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
key₁' : finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree
⊢ p.natDegree = f.natDegree * g.natDegree
have key₂ : HSub.hSub (α := (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) (β :=
    (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X])
    (Polynomial.map (algebraMap K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) g)
    ((C :
          (a : ↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯) →
            (↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯)[X])
        (AdjoinSimple.gen K ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g)) :
      (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) =
  minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p)
Tactic: have key₂ : g.map (algebraMap _ _) - C (AdjoinSimple.gen K (aeval (root p) g)) =
      minpoly K⟮aeval (root p) g⟯ (root p) :=
    minpoly.eq_of_irreducible_of_monic (hg _ _ key₁.symm) (by simp [AdjoinSimple.gen])
      (Monic.sub_of_left (hgm.map _) (degree_lt_degree (by simpa [Nat.pos_iff_ne_zero] using hg')))
-- 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
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_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
key₁' : finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree
key₂ :
  HSub.hSub (α := (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) (β :=
      (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X])
      (Polynomial.map (algebraMap K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) g)
      ((C :
            (a : ↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯) →
              (↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯)[X])
          (AdjoinSimple.gen K ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g)) :
        (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) =
    minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p)
⊢ finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree
have trans : finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
  natDegree (R := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
    (minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p))
Tactic: trans natDegree (minpoly K⟮aeval (root p) g⟯ (root p))
-- 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
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_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
key₁' : finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree
key₂ :
  HSub.hSub (α := (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) (β :=
      (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X])
      (Polynomial.map (algebraMap K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) g)
      ((C :
            (a : ↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯) →
              (↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯)[X])
          (AdjoinSimple.gen K ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g)) :
        (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) =
    minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p)
trans :
  finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
    natDegree (R := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
      (minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p))
⊢ finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree
have trans₁ : natDegree (R := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
    (minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p)) =
  g.natDegree
Tactic: trans natDegree (minpoly K⟮aeval (root p) g⟯ (root p))
-- 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
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_1 : Fact (Irreducible p)
Kx : Type u := AdjoinRoot p
this : Module.Finite K (AdjoinRoot p) := ⋯
key₁ : f = minpoly K (B := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)
key₁' : finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ = f.natDegree
key₂ :
  HSub.hSub (α := (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) (β :=
      (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X])
      (Polynomial.map (algebraMap K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) g)
      ((C :
            (a : ↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯) →
              (↥K⟮(aeval (root p) : (a : K[X]) → AdjoinRoot p) g⟯)[X])
          (AdjoinSimple.gen K ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g)) :
        (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)[X]) =
    minpoly (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p)
⊢ Eq (α := IntermediateField (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (AdjoinRoot p))
    (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)⟮root p⟯ ⊤
have a : Eq (α := IntermediateField K (AdjoinRoot p))
  (restrictScalars K (L' := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)
    (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯)⟮root p⟯)
  (restrictScalars K (L' := ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) ⊤)
Tactic: apply restrictScalars_injective K