awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
rw :
  (mk g : (a : R[X]) → AdjoinRoot g)
      ((monomial (↑i : ℕ) : (a : R) → R[X]) (Pi.single (M := fun (a : Fin g.natDegree) ↦ R) i 1 i)) =
    root g ^ (↑i : ℕ)
h₀ :
  ∀ (b : Fin g.natDegree),
    Membership.mem (γ := Finset (Fin g.natDegree)) Finset.univ b →
      b ≠ i →
        Eq.{u_1 + 1} (α := R[X])
          ((monomial (↑b : ℕ) : (a : R) → R[X]) (Pi.single (M := fun (a : Fin g.natDegree) ↦ R) i 1 b) : R[X])
          (0 : R[X])
h₁ :
  i ∉ Finset.univ →
    Eq.{u_1 + 1} (α := R[X])
      ((monomial (↑i : ℕ) : (a : R) → R[X]) (Pi.single (M := fun (a : Fin g.natDegree) ↦ R) i 1 i) : R[X]) (0 : R[X])
⊢ (mk g : (a : R[X]) → AdjoinRoot g)
      (∑ i_1 : Fin g.natDegree,
        (monomial (↑i_1 : ℕ) : (a : R) → R[X]) (Pi.single (M := fun (a : Fin g.natDegree) ↦ R) i 1 i_1)) =
    root g ^ (↑i : ℕ)

Tactic:
rw [Finset.sum_eq_single i]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
rw : (mk g : (a : R[X]) → AdjoinRoot g) ((monomial (↑i : ℕ) : (a : R) → R[X]) 1) = root g ^ (↑i : ℕ)
rw₁ : (mk g : (a : R[X]) → AdjoinRoot g) (HPow.hPow (α := R[X]) X (↑i : ℕ)) = root g ^ (↑i : ℕ)
rw₂ : HPow.hPow (α := AdjoinRoot g) ((mk g : (a : R[X]) → AdjoinRoot g) X) (↑i : ℕ) = root g ^ (↑i : ℕ)
rw₃ rw₄ : root g ^ (↑i : ℕ) = root g ^ (↑i : ℕ)
⊢ (mk g : (a : R[X]) → AdjoinRoot g)
      ((monomial (↑i : ℕ) : (a : R) → R[X]) (Pi.single (M := fun (a : Fin g.natDegree) ↦ R) i 1 i)) =
    root g ^ (↑i : ℕ)

Tactic:
rw [Pi.single_eq_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X]

Premises used: AdjoinRoot.mk, AdjoinRoot.mk_X, Polynomial.monomial_one_right_eq_X_pow, Pi.single_eq_same, RingHom.map_pow
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
i j : Fin g.natDegree
h₀ :
  Membership.mem (γ := Finset (Fin g.natDegree)) Finset.univ j →
    j ≠ i →
      Eq.{u_1 + 1} (α := R[X])
        ((monomial (↑j : ℕ) : (a : R) → R[X]) (Pi.single (M := fun (a : Fin g.natDegree) ↦ R) i 1 j) : R[X]) (0 : R[X])
⊢ Membership.mem (γ := Finset (Fin g.natDegree)) Finset.univ j →
    j ≠ i →
      Eq.{u_1 + 1} (α := R[X])
        ((monomial (↑j : ℕ) : (a : R) → R[X]) (Pi.single (M := fun (a : Fin g.natDegree) ↦ R) i 1 j) : R[X]) (0 : R[X])

Tactic:
_
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
i j : Fin g.natDegree
h : Membership.mem (γ := Finset (Fin g.natDegree)) Finset.univ j
hj : j ≠ i
h₀ :
  Eq.{u_1 + 1} (α := R[X])
    ((monomial (↑j : ℕ) : (a : R) → R[X]) (Pi.single (M := fun (a : Fin g.natDegree) ↦ R) i 1 j) : R[X])
    ((monomial (↑j : ℕ) : (a : R) → R[X]) 0 : R[X])
rw : ℕ
h₁ : Eq.{u_1 + 1} (α := R[X]) ((monomial (↑j : ℕ) : (a : R) → R[X]) 0) ((monomial (↑j : ℕ) : (a : R) → R[X]) 0)
rw₁ : ℕ
h₂ : Eq.{u_1 + 1} (α := R[X]) ((monomial (↑j : ℕ) : (a : R) → R[X]) 0) ((monomial (↑j : ℕ) : (a : R) → R[X]) 0)
rw₂ : ℕ
⊢ Eq.{u_1 + 1} (α := R[X])
    ((monomial (↑j : ℕ) : (a : R) → R[X]) (Pi.single (M := fun (a : Fin g.natDegree) ↦ R) i 1 j) : R[X]) (0 : R[X])

Tactic:
rw [← monomial_zero_right _, Pi.single_eq_of_ne hj]

Premises used: Pi.single_eq_of_ne, Polynomial.monomial_zero_right
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
h : i ∉ Finset.univ
⊢ Membership.mem (γ := Finset (Fin g.natDegree)) Finset.univ i

Tactic:
have := Finset.mem_univ i
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
h : i ∉ Finset.univ
this : Membership.mem (γ := Finset (Fin g.natDegree)) Finset.univ i
⊢ Eq.{u_1 + 1} (α := R[X])
    ((monomial (↑i : ℕ) : (a : R) → R[X]) (Pi.single (M := fun (a : Fin g.natDegree) ↦ R) i 1 i) : R[X]) (0 : R[X])

Tactic:
contradiction
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
⊢ Free R (AdjoinRoot g)

Tactic:
.of_basis (powerBasis' hg).basis

Premises used: PowerBasis.basis, Module.Free.of_basis, AdjoinRoot.powerBasis'
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
⊢ Module.Finite R (AdjoinRoot g)

Tactic:
.of_basis (powerBasis' hg).basis

Premises used: PowerBasis.basis, Module.Finite.of_basis, AdjoinRoot.powerBasis'
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
⊢ Free R (HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {g}))

Tactic:
hg.free_adjoinRoot

Premises used: AdjoinRoot, Polynomial.Monic.free_adjoinRoot
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
⊢ Module.Finite R (HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {g}))

Tactic:
hg.finite_adjoinRoot

Premises used: AdjoinRoot, Polynomial.Monic.finite_adjoinRoot
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
⊢ IsIntegral K (root f)

Tactic:
(isAlgebraic_root hf).isIntegral

Premises used: AdjoinRoot.isAlgebraic_root, IsAlgebraic.isIntegral
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
⊢ (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic

Tactic:
have f'_monic : Monic _ := monic_mul_leadingCoeff_inv hf
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
⊢ minpoly K (root f) = HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])

Tactic:
(minpoly.unique K _ f'_monic ?_ ?_).symm

Premises used: minpoly.unique, Eq.symm
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
refine_1 :
  Eq (α := AdjoinRoot f)
    ((aeval (root f) : (a : K[X]) → AdjoinRoot f)
        (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])) :
      AdjoinRoot f)
    (0 : AdjoinRoot f)
refine_2 :
  ∀ (q : K[X]),
    q.Monic →
      Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f) →
        (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).degree ≤ q.degree
⊢ minpoly K (root f) = HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])

Tactic:
refine (minpoly.unique K _ f'_monic ?_ ?_).symm

Premises used: minpoly.unique, Eq.symm
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
refine_1 :
  HMul.hMul (α := AdjoinRoot f) (β := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) f)
      ((aeval (root f) : (a : K[X]) → AdjoinRoot f) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹) : AdjoinRoot f) =
    0
refine_1₁ :
  HMul.hMul (α := AdjoinRoot f) (β := AdjoinRoot f) ((mk f : (a : K[X]) → AdjoinRoot f) f)
      ((aeval (root f) : (a : K[X]) → AdjoinRoot f) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹) : AdjoinRoot f) =
    0
refine_1₂ :
  HMul.hMul (α := AdjoinRoot f) (β := AdjoinRoot f) (0 : AdjoinRoot f)
      ((aeval (root f) : (a : K[X]) → AdjoinRoot f) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹) : AdjoinRoot f) =
    0
refine_1₃ refine_1₄ : Eq.{u_5 + 1} (α := AdjoinRoot f) 0 0
⊢ Eq (α := AdjoinRoot f)
    ((aeval (root f) : (a : K[X]) → AdjoinRoot f)
        (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])) :
      AdjoinRoot f)
    (0 : AdjoinRoot f)

Tactic:
rw [map_mul, aeval_eq, mk_self, zero_mul]

Premises used: MulZeroClass.zero_mul, map_mul, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
h₁ :
  ∀ (x : K),
    Eq (α := AdjoinRoot f)
      ((((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q)).comp C : (a : K) → AdjoinRoot f) x :
        AdjoinRoot f)
      (((mk f).comp C : (a : K) → AdjoinRoot f) x : AdjoinRoot f)
h₂ :
  Eq (α := AdjoinRoot f)
    (((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) : (a : K[X]) → AdjoinRoot f) X)
    ((mk f : (a : K[X]) → AdjoinRoot f) X)
⊢ (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f

Tactic:
ext
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
x : K
h₁ :
  Eq (α := AdjoinRoot f) ((algebraMap K (AdjoinRoot f) : (a : K) → AdjoinRoot f) x : AdjoinRoot f)
    ((of f : (a : K) → AdjoinRoot f) x : AdjoinRoot f)
⊢ Eq (α := AdjoinRoot f)
    ((((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q)).comp C : (a : K) → AdjoinRoot f) x :
      AdjoinRoot f)
    (((mk f).comp C : (a : K) → AdjoinRoot f) x : AdjoinRoot f)

Tactic:
simp only [RingHom.comp_apply, mk_C, lift_of]

Premises used: AdjoinRoot.lift_of, RingHom.comp_apply, AdjoinRoot.mk_C
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
x : K
⊢ Eq (α := AdjoinRoot f) ((algebraMap K (AdjoinRoot f) : (a : K) → AdjoinRoot f) x : AdjoinRoot f)
    ((of f : (a : K) → AdjoinRoot f) x : AdjoinRoot f)

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
⊢ Eq (α := AdjoinRoot f)
    (((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) : (a : K[X]) → AdjoinRoot f) X)
    ((mk f : (a : K[X]) → AdjoinRoot f) X)

Tactic:
simp only [RingHom.comp_apply, mk_X, lift_root]

Premises used: AdjoinRoot.mk_X, RingHom.comp_apply, AdjoinRoot.lift_root
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
⊢ (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f

Tactic:
have commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f := by
    ext
    · simp only [RingHom.comp_apply, mk_C, lift_of]
      rfl
    · simp only [RingHom.comp_apply, mk_X, lift_root]
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
refine_2 : f.natDegree ≤ q.natDegree
refine_2₁ : Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
⊢ (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).degree ≤ q.degree

Tactic:
rw [degree_eq_natDegree f'_monic.ne_zero, degree_eq_natDegree q_monic.ne_zero,
    Nat.cast_le, natDegree_mul hf, natDegree_C, add_zero]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.natDegree_mul, Polynomial.natDegree_C, Nat.cast_le, add_zero, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
refine_2 : f ∣ q
refine_2₁ : q ≠ 0
⊢ f.natDegree ≤ q.natDegree

Tactic:
apply natDegree_le_of_dvd

Premises used: Polynomial.natDegree_le_of_dvd
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
rw :
  Eq (α := AdjoinRoot f)
    (((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f)
    (0 : AdjoinRoot f)
rw₁ :
  Eq (α := AdjoinRoot f)
    ((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval : (a : AdjoinRoot q) → AdjoinRoot f)
        ((mk q : (a : K[X]) → AdjoinRoot q) q) :
      AdjoinRoot f)
    (0 : AdjoinRoot f)
rw₂ :
  Eq (α := AdjoinRoot f) ((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval : (a : AdjoinRoot q) → AdjoinRoot f) 0) 0
rw₃ rw₄ : Eq.{u_5 + 1} (α := AdjoinRoot f) 0 0
⊢ Eq (α := AdjoinRoot f) ((mk f : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)

Tactic:
rw [← commutes, RingHom.comp_apply, mk_self, map_zero]

Premises used: map_zero, RingHom.comp_apply, AdjoinRoot.mk_self
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ Eq (α := AdjoinRoot f) ((mk f : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)

Tactic:
have : mk f q = 0 := by rw [← commutes, RingHom.comp_apply, mk_self, map_zero]
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
this : Eq (α := AdjoinRoot f) ((mk f : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
⊢ f ∣ q

Tactic:
mk_eq_zero.1 this

Premises used: AdjoinRoot.mk_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
this : Eq (α := AdjoinRoot f) ((mk f : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
⊢ f ∣ q

Tactic:
exact mk_eq_zero.1 this

Premises used: AdjoinRoot.mk_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ q ≠ 0

Tactic:
q_monic.ne_zero

Premises used: Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ q ≠ 0

Tactic:
exact q_monic.ne_zero

Premises used: Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
refine_2 : ¬Eq (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
refine_2₁ : ¬f.leadingCoeff⁻¹ = 0
refine_2₂ : ¬f.leadingCoeff = 0
refine_2₃ refine_2₄ refine_2₅ refine_2₆ : ¬f = 0
⊢ Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])

Tactic:
rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]

Premises used: inv_eq_zero, Polynomial.C_eq_zero, Ne, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
rw : Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
⊢ f'.natDegree = f.natDegree

Tactic:
rw [natDegree_mul hf, natDegree_C, add_zero]

Premises used: Polynomial.natDegree_mul, Polynomial.natDegree_C, add_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
rwa : ¬Eq (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
rwa₁ : ¬f.leadingCoeff⁻¹ = 0
rwa₂ : ¬f.leadingCoeff = 0
rwa₃ rwa₄ rwa₅ rwa₆ : ¬f = 0
⊢ Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])

Tactic:
rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]

Premises used: inv_eq_zero, Polynomial.C_eq_zero, Ne, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
⊢ f'.natDegree = f.natDegree

Tactic:
have deg_f' : f'.natDegree = f.natDegree := by
    rw [natDegree_mul hf, natDegree_C, add_zero]
    · rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
⊢ minpoly K (root f) = f'

Tactic:
have minpoly_eq : minpoly K (root f) = f' := minpoly_root hf
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
hli : LinearIndependent K (M := AdjoinRoot f) fun (i : Fin f.natDegree) ↦ root f ^ (↑i : ℕ)
hsp :
  LE.le (α := Submodule K (AdjoinRoot f)) ⊤ (Submodule.span K (Set.range fun (i : Fin f.natDegree) ↦ root f ^ (↑i : ℕ)))
⊢ Basis (Fin f.natDegree) K (AdjoinRoot f)

Tactic:
apply Basis.mk (v := fun i : Fin f.natDegree ↦ root f ^ i.val)

Premises used: Module.Basis.mk
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
hli : LinearIndependent K (M := AdjoinRoot f) fun (i : Fin (natDegree (minpoly K (root f)))) ↦ root f ^ (↑i : ℕ)
⊢ LinearIndependent K (M := AdjoinRoot f) fun (i : Fin f.natDegree) ↦ root f ^ (↑i : ℕ)

Tactic:
rw [← deg_f', ← minpoly_eq]
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
⊢ LinearIndependent K (M := AdjoinRoot f) fun (i : Fin (natDegree (minpoly K (root f)))) ↦ root f ^ (↑i : ℕ)

Tactic:
linearIndependent_pow (root f)

Premises used: AdjoinRoot.root, linearIndependent_pow
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
⊢ LinearIndependent K (M := AdjoinRoot f) fun (i : Fin (natDegree (minpoly K (root f)))) ↦ root f ^ (↑i : ℕ)

Tactic:
exact linearIndependent_pow (root f)

Premises used: AdjoinRoot.root, linearIndependent_pow
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
hsp :
  Membership.mem (γ := Submodule K (AdjoinRoot f))
    (Submodule.span K (Set.range fun (i : Fin (natDegree (minpoly K (root f)))) ↦ root f ^ (↑i : ℕ))) y
⊢ Membership.mem (γ := Submodule K (AdjoinRoot f))
    (Submodule.span K (Set.range fun (i : Fin f.natDegree) ↦ root f ^ (↑i : ℕ))) y

Tactic:
rw [← deg_f', ← minpoly_eq]
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
hsp : ∃ (f_1 : K[X]), y = (aeval (root f) : (a : K[X]) → AdjoinRoot f) f_1
⊢ Membership.mem (γ := Submodule K (AdjoinRoot f))
    (Submodule.span K (Set.range fun (i : Fin (natDegree (minpoly K (root f)))) ↦ root f ^ (↑i : ℕ))) y

Tactic:
apply (isIntegral_root hf).mem_span_pow

Premises used: IsIntegral.mem_span_pow, AdjoinRoot.isIntegral_root
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
hsp :
  ∀ (g : K[X]),
    ∃ (f_1 : K[X]),
      Eq (α := AdjoinRoot f) (Quot.mk (⇑(Submodule.quotientRel (span {f})) : K[X] → K[X] → Prop) g)
        ((aeval (root f) : (a : K[X]) → AdjoinRoot f) f_1)
⊢ ∃ (f_1 : K[X]), y = (aeval (root f) : (a : K[X]) → AdjoinRoot f) f_1

Tactic:
obtain ⟨g⟩ := y