awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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) (map (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)
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)
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)
rw₆ : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap E A) (map (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) (map (algebraMap E A) (minpoly E a)) : 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)
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)
rw₆ : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap E A) (map (algebraMap F E) g)) : A) (0 : A)
rw₇ : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap E A) (minpoly E a)) : A) (0 : A)
⊢ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : F[X]) → A) g : A) (0 : A)
have rw₈ : Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : E[X]) → A) (minpoly E a) : 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)
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)
rw₆ : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap E A) (map (algebraMap F E) g)) : A) (0 : A)
rw₇ : Eq (α := A) ((Polynomial.aeval a : (a : A[X]) → A) (map (algebraMap E A) (minpoly E a)) : A) (0 : A)
rw₈ : Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : E[X]) → A) (minpoly E a) : A) (0 : A)
⊢ Eq.{u_5 + 1} (α := A) ((Polynomial.aeval a : (a : F[X]) → A) g : A) (0 : A)
have rw₉ : Eq.{u_5 + 1} (α := A) 0 0
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:
A : Type u_1
B : Type u_2
inst : Field A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
⊢ Eq (α := Ideal A[X]) (RingHom.ker (F := A[X] →ₐ[A] B) (Polynomial.aeval x)) (A[X] ∙ minpoly A x)
have h : ∀ (p : A[X]),
  Membership.mem (γ := Ideal A[X]) (RingHom.ker (F := A[X] →ₐ[A] B) (Polynomial.aeval x)) p ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
Tactic: ext p
-- 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]
⊢ Membership.mem (γ := Ideal A[X]) (RingHom.ker (F := A[X] →ₐ[A] B) (Polynomial.aeval x)) p ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
have h : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B) ↔
  Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
Tactic: simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton,
    dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)]
-- 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 :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B) ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
⊢ Membership.mem (γ := Ideal A[X]) (RingHom.ker (F := A[X] →ₐ[A] B) (Polynomial.aeval x)) p ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
have h₁ : minpoly A x ∣ p ↔ Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
Tactic: simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton,
    dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)]
-- 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 :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B) ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
h₁ : minpoly A x ∣ p ↔ Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
⊢ Membership.mem (γ := Ideal A[X]) (RingHom.ker (F := A[X] →ₐ[A] B) (Polynomial.aeval x)) p ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
have h₂ : minpoly A x ∣ p ↔ ∃ (a : A[X]), HSMul.hSMul (β := A[X]) a (minpoly A x) = p
Tactic: simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton,
    dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)]
-- 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 :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B) ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
h₁ : minpoly A x ∣ p ↔ Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
h₂ : minpoly A x ∣ p ↔ ∃ (a : A[X]), HSMul.hSMul (β := A[X]) a (minpoly A x) = p
⊢ Membership.mem (γ := Ideal A[X]) (RingHom.ker (F := A[X] →ₐ[A] B) (Polynomial.aeval x)) p ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
have h₃ : (∃ (c : A[X]), p = c * minpoly A x) ↔ ∃ (a : A[X]), HSMul.hSMul (β := A[X]) a (minpoly A x) = p
Tactic: simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton,
    dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)]
-- 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 :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B) ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
h₁ : minpoly A x ∣ p ↔ Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
h₂ : minpoly A x ∣ p ↔ ∃ (a : A[X]), HSMul.hSMul (β := A[X]) a (minpoly A x) = p
h₃ : (∃ (c : A[X]), p = c * minpoly A x) ↔ ∃ (a : A[X]), HSMul.hSMul (β := A[X]) a (minpoly A x) = p
⊢ Membership.mem (γ := Ideal A[X]) (RingHom.ker (F := A[X] →ₐ[A] B) (Polynomial.aeval x)) p ↔
    Membership.mem (γ := Ideal A[X]) (A[X] ∙ minpoly A x) p
have h₄ : (∃ (c : A[X]), p = c * minpoly A x) ↔ ∃ (a : A[X]), a * minpoly A x = p
Tactic: simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton,
    dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)]
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
⊢ HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) = minpoly A x
have this : p.leadingCoeff ≠ 0
Tactic: have : p.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hp1.ne_zero
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
⊢ HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) = minpoly A x
have hp1₁ : Irreducible (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
Tactic: apply eq_of_irreducible_of_monic
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
hp1₁ : Irreducible (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
⊢ HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) = minpoly A x
have hp2₁ : Eq.{u_2 + 1} (α := B)
  ((Polynomial.aeval x : (a : A[X]) → B) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])) : B)
  (0 : B)
Tactic: apply eq_of_irreducible_of_monic
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
hp1₁ : Irreducible (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]))
hp2₁ :
  Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])) : B)
    (0 : B)
⊢ HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) = minpoly A x
have hp3 : (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).Monic
Tactic: apply eq_of_irreducible_of_monic
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
⊢ HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])
      ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) =
    1
have rwa : Eq (α := A[X]) ((C : (a : A) → A[X]) (p.leadingCoeff⁻¹ * p.leadingCoeff) : A[X]) (1 : A[X])
Tactic: rwa [← C_mul, inv_mul_cancel₀, C_1]
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
rwa : Eq (α := A[X]) ((C : (a : A) → A[X]) (p.leadingCoeff⁻¹ * p.leadingCoeff) : A[X]) (1 : A[X])
⊢ HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])
      ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) =
    1
have rwa₁ : Eq.{u_1 + 1} (α := A[X]) ((C : (a : A) → A[X]) 1) 1
Tactic: rwa [← C_mul, inv_mul_cancel₀, C_1]
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
rwa : Eq (α := A[X]) ((C : (a : A) → A[X]) (p.leadingCoeff⁻¹ * p.leadingCoeff) : A[X]) (1 : A[X])
rwa₁ : Eq.{u_1 + 1} (α := A[X]) ((C : (a : A) → A[X]) 1) 1
rwa₂ : p.leadingCoeff ≠ 0
⊢ HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])
      ((C : (a : A) → A[X]) p.leadingCoeff : A[X]) =
    1
have rwa₃ : Eq.{u_1 + 1} (α := A[X]) 1 1
Tactic: rwa [← C_mul, inv_mul_cancel₀, C_1]
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
⊢ HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
      ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) =
    1
have rwa : Eq (α := A[X]) ((C : (a : A) → A[X]) (p.leadingCoeff * p.leadingCoeff⁻¹) : A[X]) (1 : A[X])
Tactic: rwa [← C_mul, mul_inv_cancel₀, C_1]
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
rwa : Eq (α := A[X]) ((C : (a : A) → A[X]) (p.leadingCoeff * p.leadingCoeff⁻¹) : A[X]) (1 : A[X])
⊢ HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
      ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) =
    1
have rwa₁ : Eq.{u_1 + 1} (α := A[X]) ((C : (a : A) → A[X]) 1) 1
Tactic: rwa [← C_mul, mul_inv_cancel₀, C_1]
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
rwa : Eq (α := A[X]) ((C : (a : A) → A[X]) (p.leadingCoeff * p.leadingCoeff⁻¹) : A[X]) (1 : A[X])
rwa₁ : Eq.{u_1 + 1} (α := A[X]) ((C : (a : A) → A[X]) 1) 1
rwa₂ : p.leadingCoeff ≠ 0
⊢ HMul.hMul (α := A[X]) (β := A[X]) ((C : (a : A) → A[X]) p.leadingCoeff : A[X])
      ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) =
    1
have rwa₃ : Eq.{u_1 + 1} (α := A[X]) 1 1
Tactic: rwa [← C_mul, mul_inv_cancel₀, C_1]
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
⊢ Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])) : B)
    (0 : B)
have hp2₁ : HMul.hMul (α := B) (β := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B)
    ((Polynomial.aeval x : (a : A[X]) → B) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) : B) =
  0
Tactic: rw [aeval_mul, hp2, 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
hp2₁ :
  HMul.hMul (α := B) (β := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B)
      ((Polynomial.aeval x : (a : A[X]) → B) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) : B) =
    0
⊢ Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])) : B)
    (0 : B)
have hp2₂ : HMul.hMul (α := B) (β := B) (0 : B)
    ((Polynomial.aeval x : (a : A[X]) → B) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) : B) =
  0
Tactic: rw [aeval_mul, hp2, 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
hp2₁ :
  HMul.hMul (α := B) (β := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B)
      ((Polynomial.aeval x : (a : A[X]) → B) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) : B) =
    0
hp2₂ :
  HMul.hMul (α := B) (β := B) (0 : B)
      ((Polynomial.aeval x : (a : A[X]) → B) ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X]) : B) =
    0
⊢ Eq.{u_2 + 1} (α := B)
    ((Polynomial.aeval x : (a : A[X]) → B) (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])) : B)
    (0 : B)
have hp2₃ : Eq.{u_2 + 1} (α := B) 0 0
Tactic: rw [aeval_mul, hp2, 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
⊢ (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).Monic
have hp3 : (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).leadingCoeff = 1
Tactic: rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel₀]
-- 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 : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) p : B) (0 : B)
this : p.leadingCoeff ≠ 0
hp3 : (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).leadingCoeff = 1
⊢ (HMul.hMul (β := A[X]) p ((C : (a : A) → A[X]) p.leadingCoeff⁻¹ : A[X])).Monic
have hp3₁ : p.leadingCoeff * leadingCoeff ((C : (a : A) → A[X]) p.leadingCoeff⁻¹) = 1
Tactic: rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel₀]