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
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 (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)⟯) ⊤)
have a : Eq (α := IntermediateField K (AdjoinRoot p))
  (adjoin K
    ((↑⊤ : Set (AdjoinRoot p)) ∪
      singleton (α := AdjoinRoot p) ((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)))
  ⊤
Tactic: rw [restrictScalars_top, adjoin_adjoin_left, Set.union_comm, ← adjoin_adjoin_left,
          adjoin_root_eq_top p, restrictScalars_adjoin]
-- 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
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 =
    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))
have this₁ : 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⟯ ⊤
Tactic: have : K⟮aeval (root p) g⟯⟮root p⟯ = ⊤ := by
        apply restrictScalars_injective K
        rw [restrictScalars_top, adjoin_adjoin_left, Set.union_comm, ← adjoin_adjoin_left,
          adjoin_root_eq_top p, restrictScalars_adjoin]
        simp
-- 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_2 : 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)
this :
  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⟯ ⊤
⊢ 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))
have rw : IsIntegral (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) (root p)
Tactic: rw [← finrank_top', ← this, adjoin.finrank]
-- 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
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)
⊢ p.natDegree = f.natDegree * g.natDegree
have key₂' : finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree
Tactic: have key₂' : finrank K⟮aeval (root p) g⟯ Kx = natDegree g := by
    trans natDegree (minpoly K⟮aeval (root p) g⟯ (root p))
    · have : K⟮aeval (root p) g⟯⟮root p⟯ = ⊤ := by
        apply restrictScalars_injective K
        rw [restrictScalars_top, adjoin_adjoin_left, Set.union_comm, ← adjoin_adjoin_left,
          adjoin_root_eq_top p, restrictScalars_adjoin]
        simp
      rw [← finrank_top', ← this, adjoin.finrank]
      exact IsIntegral.of_finite _ _
    · simp [← 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)
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)
key₂' : finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree
⊢ p.natDegree = f.natDegree * g.natDegree
have this₁ : finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ *
    finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
  finrank K Kx
Tactic: have := Module.finrank_mul_finrank K K⟮aeval (root p) g⟯ Kx
-- 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_2 : 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)
key₂' : finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree
this :
  finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ *
      finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
    finrank K Kx
⊢ p.natDegree = f.natDegree * g.natDegree
have rwa : ∀
  (this :
    f.natDegree * finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = finrank K Kx),
  p.natDegree = f.natDegree * g.natDegree
Tactic: rwa [key₁', key₂', (AdjoinRoot.powerBasis hp₁.ne_zero).finrank, powerBasis_dim, eq_comm] at this
Cleared hypotheses: this
-- 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_2 : 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)
key₂' : finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree
this :
  finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ *
      finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
    finrank K Kx
rwa :
  ∀
    (this :
      f.natDegree * finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = finrank K Kx),
    p.natDegree = f.natDegree * g.natDegree
⊢ p.natDegree = f.natDegree * g.natDegree
have rwa₁ : ∀ (this : f.natDegree * g.natDegree = finrank K Kx), p.natDegree = f.natDegree * g.natDegree
Tactic: rwa [key₁', key₂', (AdjoinRoot.powerBasis hp₁.ne_zero).finrank, powerBasis_dim, eq_comm] at this
Cleared hypotheses: this
-- 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_2 : 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)
key₂' : finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree
this :
  finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ *
      finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
    finrank K Kx
rwa :
  ∀
    (this :
      f.natDegree * finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = finrank K Kx),
    p.natDegree = f.natDegree * g.natDegree
rwa₁ : ∀ (this : f.natDegree * g.natDegree = finrank K Kx), p.natDegree = f.natDegree * g.natDegree
⊢ p.natDegree = f.natDegree * g.natDegree
have rwa₂ : ∀ (this : f.natDegree * g.natDegree = (powerBasis sorry).dim), p.natDegree = f.natDegree * g.natDegree
Tactic: rwa [key₁', key₂', (AdjoinRoot.powerBasis hp₁.ne_zero).finrank, powerBasis_dim, eq_comm] at this
Cleared hypotheses: this
-- 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_2 : 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)
key₂' : finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree
this :
  finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ *
      finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
    finrank K Kx
rwa :
  ∀
    (this :
      f.natDegree * finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = finrank K Kx),
    p.natDegree = f.natDegree * g.natDegree
rwa₁ : ∀ (this : f.natDegree * g.natDegree = finrank K Kx), p.natDegree = f.natDegree * g.natDegree
rwa₂ : ∀ (this : f.natDegree * g.natDegree = (powerBasis ⋯).dim), p.natDegree = f.natDegree * g.natDegree
⊢ p.natDegree = f.natDegree * g.natDegree
have rwa₃ : ∀ (this : f.natDegree * g.natDegree = p.natDegree), p.natDegree = f.natDegree * g.natDegree
Tactic: rwa [key₁', key₂', (AdjoinRoot.powerBasis hp₁.ne_zero).finrank, powerBasis_dim, eq_comm] at this
Cleared hypotheses: this
-- 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_2 : 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)
key₂' : finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = g.natDegree
this :
  finrank K ↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯ *
      finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx =
    finrank K Kx
rwa :
  ∀
    (this :
      f.natDegree * finrank (↥K⟮((aeval (root p) : (a : K[X]) → AdjoinRoot p) g : AdjoinRoot p)⟯) Kx = finrank K Kx),
    p.natDegree = f.natDegree * g.natDegree
rwa₁ : ∀ (this : f.natDegree * g.natDegree = finrank K Kx), p.natDegree = f.natDegree * g.natDegree
rwa₂ : ∀ (this : f.natDegree * g.natDegree = (powerBasis ⋯).dim), p.natDegree = f.natDegree * g.natDegree
rwa₃ : ∀ (this : f.natDegree * g.natDegree = p.natDegree), p.natDegree = f.natDegree * g.natDegree
⊢ p.natDegree = f.natDegree * g.natDegree
have rwa₄ : ∀ (this : p.natDegree = f.natDegree * g.natDegree), p.natDegree = f.natDegree * g.natDegree
Tactic: rwa [key₁', key₂', (AdjoinRoot.powerBasis hp₁.ne_zero).finrank, powerBasis_dim, eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : Eq (α := K[X]) (minpoly K x) (minpoly K y)
⊢ ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯
have hy : IsAlgebraic K y
Tactic: have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
hx : IsAlgebraic K x
h_mp : Eq (α := K[X]) (minpoly K x) (minpoly K y)
⊢ Eq (α := ↥K⟮y⟯) ((algEquiv hx h_mp : (a : ↥K⟮x⟯) → ↥K⟮y⟯) (AdjoinSimple.gen K x) : ↥K⟮y⟯)
    (AdjoinSimple.gen K y : ↥K⟮y⟯)
have hy : IsAlgebraic K y
Tactic: have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩