awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pmin :
  ∀ (q : A[X]),
    q.Monic → Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) (0 : B) → p.degree ≤ q.degree
hx : IsIntegral A x
hnz : ¬minpoly A x - p = 0
h : 1 = p.leadingCoeff
⊢ leadingCoeff (minpoly A x) = p.leadingCoeff
have h₁ : Eq.{u_1 + 1} (α := A) 1 1
Tactic: rw [(monic hx).leadingCoeff, pmonic.leadingCoeff]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
⊢ minpoly A x ∣ p
have pos : ∀ (hp0 : p = 0), minpoly A x ∣ p
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
pos : ∀ (hp0 : p = 0), minpoly A x ∣ p
⊢ minpoly A x ∣ p
have neg : ∀ (hp0 : ¬p = 0), minpoly A x ∣ p
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp0 : ¬p = 0
⊢ minpoly A x ∣ p
have hx : IsIntegral A x
Tactic: have hx : IsIntegral A x := IsAlgebraic.isIntegral ⟨p, hp0, hp⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ minpoly A x ∣ p
have neg : p %ₘ minpoly A x = 0
Tactic: rw [← modByMonic_eq_zero_iff_dvd (monic hx)]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp0 : ¬p = 0
hx : IsIntegral A x
⊢ p %ₘ minpoly A x = 0
have neg : ∀ (hnz : ¬p %ₘ minpoly A x = 0), False
Tactic: by_contra hnz
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
hp : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
hp0 : ¬p = 0
hx : IsIntegral A x
hnz : ¬p %ₘ minpoly A x = 0
⊢ False
have neg : (p %ₘ minpoly A x).degree < degree (minpoly A x)
Tactic: apply degree_le_of_ne_zero A x hnz
    ((aeval_modByMonic_eq_self_of_root (aeval _ _)).trans hp) |>.not_gt
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
h : minpoly A x ∣ p
q : A[X]
hq : p = minpoly A x * q
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
have rw : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x * q) : B) (0 : B)
Tactic: rw [hq, map_mul, aeval, zero_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
h : minpoly A x ∣ p
q : A[X]
hq : p = minpoly A x * q
rw : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x * q) : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
have rw₁ : HMul.hMul (α := B) (β := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B)
    ((Polynomial.aeval x : (a : A[X]) → B) q : B) =
  0
Tactic: rw [hq, map_mul, aeval, zero_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
h : minpoly A x ∣ p
q : A[X]
hq : p = minpoly A x * q
rw : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x * q) : B) (0 : B)
rw₁ :
  HMul.hMul (α := B) (β := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B)
      ((Polynomial.aeval x : (a : A[X]) → B) q : B) =
    0
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
have rw₂ : HMul.hMul (α := B) (β := B) (0 : B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) = 0
Tactic: rw [hq, map_mul, aeval, zero_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
p : A[X]
h : minpoly A x ∣ p
q : A[X]
hq : p = minpoly A x * q
rw : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x * q) : B) (0 : B)
rw₁ :
  HMul.hMul (α := B) (β := B) ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B)
      ((Polynomial.aeval x : (a : A[X]) → B) q : B) =
    0
rw₂ : HMul.hMul (α := B) (β := B) (0 : B) ((Polynomial.aeval x : (a : A[X]) → B) q : B) = 0
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
have rw₃ : Eq.{u_2 + 1} (α := B) 0 0
Tactic: rw [hq, map_mul, aeval, zero_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsReduced B
n : ℕ
p : A[X]
dvd : minpoly A x ∣ p ^ n
⊢ minpoly A x ∣ p
have rw : ∀ (dvd : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (p ^ n) : B) (0 : B)),
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
Tactic: rw [dvd_iff] at dvd ⊢
Cleared hypotheses: dvd
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsReduced B
n : ℕ
p : A[X]
dvd : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (p ^ n) : B) (0 : B)
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
have dvd₁ : HPow.hPow (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) n = 0
Tactic: rw [map_pow] at dvd
Cleared hypotheses: dvd
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_3
K : Type u_4
R : Type u_5
inst : CommRing A
inst_1 : Field K
inst_2 : Ring R
inst_3 : Algebra A K
inst_4 : Algebra A R
inst_5 : Algebra K R
inst_6 : IsScalarTower A K R
x : R
⊢ Dvd.dvd (α := K[X]) (minpoly K x) (map (algebraMap A K) (minpoly A x))
have refine : Eq.{u_5 + 1} (α := R) ((Polynomial.aeval x : (a : K[X]) → R) (map (algebraMap A K) (minpoly A x)) : R) (0 : R)
Tactic: refine minpoly.dvd K x ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_3
K : Type u_4
R : Type u_5
inst : CommRing A
inst_1 : Field K
inst_2 : Ring R
inst_3 : Algebra A K
inst_4 : Algebra A R
inst_5 : Algebra K R
inst_6 : IsScalarTower A K R
x : R
⊢ Eq.{u_5 + 1} (α := R) ((Polynomial.aeval x : (a : K[X]) → R) (map (algebraMap A K) (minpoly A x)) : R) (0 : R)
have rw : Eq.{u_5 + 1} (α := R) ((Polynomial.aeval x : (a : A[X]) → R) (minpoly A x) : R) (0 : R)
Tactic: rw [aeval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
A : Type u_3
K : Type u_4
R : Type u_5
inst : CommRing A
inst_1 : Field K
inst_2 : Ring R
inst_3 : Algebra A K
inst_4 : Algebra A R
inst_5 : Algebra K R
inst_6 : IsScalarTower A K R
x : R
rw : Eq.{u_5 + 1} (α := R) ((Polynomial.aeval x : (a : A[X]) → R) (minpoly A x) : R) (0 : R)
⊢ Eq.{u_5 + 1} (α := R) ((Polynomial.aeval x : (a : K[X]) → R) (map (algebraMap A K) (minpoly A x)) : R) (0 : R)
have rw₁ : Eq.{u_5 + 1} (α := R) 0 0
Tactic: rw [aeval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : Ring L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra S L
inst_7 : Algebra K L
inst_8 : Algebra R L
inst_9 : IsScalarTower R K L
inst_10 : IsScalarTower R S L
s : S
⊢ Dvd.dvd (α := K[X]) (minpoly.{u_5, u_6} K (B := L) ((algebraMap S L : (a : S) → L) s : L))
    (map (algebraMap R K) (minpoly R s))
have apply : Eq.{u_6 + 1} (α := L)
  (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
      (map (algebraMap R K) (minpoly R s)) :
    L)
  (0 : L)
Tactic: apply minpoly.dvd K (algebraMap S L s)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : Ring L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra S L
inst_7 : Algebra K L
inst_8 : Algebra R L
inst_9 : IsScalarTower R K L
inst_10 : IsScalarTower R S L
s : S
⊢ Eq.{u_6 + 1} (α := L)
    (((Polynomial.aeval ((algebraMap S L : (a : S) → L) s) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        (map (algebraMap R K) (minpoly R s)) :
      L)
    (0 : L)
have h : Eq (α := R →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
Tactic: rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : Ring L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra S L
inst_7 : Algebra K L
inst_8 : Algebra R L
inst_9 : IsScalarTower R K L
inst_10 : IsScalarTower R S L
s : S
⊢ Eq (α := R →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
have h : Eq (α := R →+* L) (algebraMap R L)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
Tactic: rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
R : Type u_3
S : Type u_4
K : Type u_5
L : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : Ring L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra S L
inst_7 : Algebra K L
inst_8 : Algebra R L
inst_9 : IsScalarTower R K L
inst_10 : IsScalarTower R S L
s : S
h :
  Eq (α := R →+* L) (algebraMap R L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
⊢ Eq (α := R →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
have h₁ : Eq (α := R →+* L) (algebraMap R L) (algebraMap R L)
Tactic: rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
⊢ Eq (α := E[X]) (map (algebraMap F E) (minpoly F a)) (minpoly E a)
have refine : natDegree (map (algebraMap F E) (minpoly F a)) ≤ natDegree (minpoly E a)
Tactic: refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic ha.tower_top)
    ((algebraMap F E).injective.monic_map_iff.mp <| minpoly.monic ha)
    (minpoly.dvd E a (by simp)) ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
⊢ natDegree (map (algebraMap F E) (minpoly F a)) ≤ natDegree (minpoly E a)
have obtain : ∀ (g : F[X]) (hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a))
  (hgdeg : g.natDegree = natDegree (minpoly E a)) (hgmon : g.Monic),
  natDegree (map (algebraMap F E) (minpoly F a)) ≤ natDegree (minpoly E a)
Tactic: obtain ⟨g, hg, hgdeg, hgmon⟩ := lifts_and_natDegree_eq_and_monic h (minpoly.monic ha.tower_top)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
⊢ natDegree (map (algebraMap F E) (minpoly F a)) ≤ natDegree (minpoly E a)
have rw : natDegree (minpoly F a) ≤ g.natDegree
Tactic: rw [natDegree_map, ← hgdeg]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
⊢ natDegree (minpoly F a) ≤ g.natDegree
have refine : Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : F[X]) → A) g : A) (0 : A)
Tactic: refine natDegree_le_of_dvd (minpoly.dvd F a ?_) hgmon.ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
⊢ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : F[X]) → A) g : A) (0 : A)
have rw : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap F A) g) : A) (0 : A)
Tactic: rw [← aeval_map_algebraMap A, IsScalarTower.algebraMap_eq F E A, ← coe_mapRingHom,
    ← mapRingHom_comp, RingHom.comp_apply, coe_mapRingHom, coe_mapRingHom, hg,
    aeval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
rw : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap F A) g) : A) (0 : A)
⊢ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : F[X]) → A) g : A) (0 : A)
have rw₁ : Eq (α := A)
  ((Polynomial.aeval a : (a : A[X]) → A)
      (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap E A) (algebraMap F E)) g) :
    A)
  (0 : A)
Tactic: rw [← aeval_map_algebraMap A, IsScalarTower.algebraMap_eq F E A, ← coe_mapRingHom,
    ← mapRingHom_comp, RingHom.comp_apply, coe_mapRingHom, coe_mapRingHom, hg,
    aeval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
rw : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap F A) g) : A) (0 : A)
rw₁ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap E A) (algebraMap F E)) g) :
      A)
    (0 : A)
⊢ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : F[X]) → A) g : A) (0 : A)
have rw₂ : Eq (α := A)
  ((Polynomial.aeval a : (a : A[X]) → A)
      (((mapRingHom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap E A) (algebraMap F E)) :
              RingHom.{u_3, u_5} F[X] A[X]) :
            (a : F[X]) → A[X])
          g :
        A[X]) :
    A)
  (0 : A)
Tactic: rw [← aeval_map_algebraMap A, IsScalarTower.algebraMap_eq F E A, ← coe_mapRingHom,
    ← mapRingHom_comp, RingHom.comp_apply, coe_mapRingHom, coe_mapRingHom, hg,
    aeval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
rw : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap F A) g) : A) (0 : A)
rw₁ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap E A) (algebraMap F E)) g) :
      A)
    (0 : A)
rw₂ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (((mapRingHom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap E A) (algebraMap F E)) :
                RingHom.{u_3, u_5} F[X] A[X]) :
              (a : F[X]) → A[X])
            g :
          A[X]) :
      A)
    (0 : A)
⊢ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : F[X]) → A) g : A) (0 : A)
have rw₃ : Eq (α := A)
  ((Polynomial.aeval a : (a : A[X]) → A)
      (((RingHom.comp (β := E[X]) (mapRingHom (algebraMap E A)) (mapRingHom (algebraMap F E)) :
              RingHom.{u_3, u_5} F[X] A[X]) :
            (a : F[X]) → A[X])
          g :
        A[X]) :
    A)
  (0 : A)
Tactic: rw [← aeval_map_algebraMap A, IsScalarTower.algebraMap_eq F E A, ← coe_mapRingHom,
    ← mapRingHom_comp, RingHom.comp_apply, coe_mapRingHom, coe_mapRingHom, hg,
    aeval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
rw : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap F A) g) : A) (0 : A)
rw₁ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap E A) (algebraMap F E)) g) :
      A)
    (0 : A)
rw₂ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (((mapRingHom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap E A) (algebraMap F E)) :
                RingHom.{u_3, u_5} F[X] A[X]) :
              (a : F[X]) → A[X])
            g :
          A[X]) :
      A)
    (0 : A)
rw₃ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (((RingHom.comp (β := E[X]) (mapRingHom (algebraMap E A)) (mapRingHom (algebraMap F E)) :
                RingHom.{u_3, u_5} F[X] A[X]) :
              (a : F[X]) → A[X])
            g :
          A[X]) :
      A)
    (0 : A)
⊢ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : F[X]) → A) g : A) (0 : A)
have rw₄ : Eq (α := A)
  ((Polynomial.aeval a : (a : A[X]) → A)
      (((mapRingHom (algebraMap E A) : RingHom.{u_4, u_5} E[X] A[X]) : (a : E[X]) → A[X])
          (((mapRingHom (algebraMap F E) : RingHom.{u_3, u_4} F[X] E[X]) : (a : F[X]) → E[X]) g) :
        A[X]) :
    A)
  (0 : A)
Tactic: rw [← aeval_map_algebraMap A, IsScalarTower.algebraMap_eq F E A, ← coe_mapRingHom,
    ← mapRingHom_comp, RingHom.comp_apply, coe_mapRingHom, coe_mapRingHom, hg,
    aeval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Field (goal)
Goal:
F : Type u_3
E : Type u_4
A : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : CommRing A
inst_3 : Algebra F E
inst_4 : Algebra E A
inst_5 : Algebra F A
inst_6 : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : Membership.mem (γ := Subsemiring E[X]) (lifts (algebraMap F E)) (minpoly E a)
g : F[X]
hg : Eq (α := E[X]) (map (algebraMap F E) g) (minpoly E a)
hgdeg : g.natDegree = natDegree (minpoly E a)
hgmon : g.Monic
rw : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap F A) g) : A) (0 : A)
rw₁ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap E A) (algebraMap F E)) g) :
      A)
    (0 : A)
rw₂ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (((mapRingHom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap E A) (algebraMap F E)) :
                RingHom.{u_3, u_5} F[X] A[X]) :
              (a : F[X]) → A[X])
            g :
          A[X]) :
      A)
    (0 : A)
rw₃ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (((RingHom.comp (β := E[X]) (mapRingHom (algebraMap E A)) (mapRingHom (algebraMap F E)) :
                RingHom.{u_3, u_5} F[X] A[X]) :
              (a : F[X]) → A[X])
            g :
          A[X]) :
      A)
    (0 : A)
rw₄ :
  Eq (α := A)
    ((Polynomial.aeval a : (a : A[X]) → A)
        (((mapRingHom (algebraMap E A) : RingHom.{u_4, u_5} E[X] A[X]) : (a : E[X]) → A[X])
            (((mapRingHom (algebraMap F E) : RingHom.{u_3, u_4} F[X] E[X]) : (a : F[X]) → E[X]) g) :
          A[X]) :
      A)
    (0 : A)
⊢ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : F[X]) → A) g : A) (0 : A)
have rw₅ : Eq (α := A)
  ((Polynomial.aeval a : (a : A[X]) → A)
      (map (algebraMap E A) (((mapRingHom (algebraMap F E) : RingHom.{u_3, u_4} F[X] E[X]) : (a : F[X]) → E[X]) g)) :
    A)
  (0 : A)
Tactic: rw [← aeval_map_algebraMap A, IsScalarTower.algebraMap_eq F E A, ← coe_mapRingHom,
    ← mapRingHom_comp, RingHom.comp_apply, coe_mapRingHom, coe_mapRingHom, hg,
    aeval_map_algebraMap, minpoly.aeval]