awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
simp_rw : (∑ x_1 : Fin g.natDegree, if (↑x_1 : ℕ) = (↑i : ℕ) then x x_1 else 0) = x i
⊢ ∑ b : Fin g.natDegree, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (x b)) (↑i : ℕ) = x i
have simp_rw₁ : (∑ x_1 : Fin g.natDegree, if x_1 = i then x x_1 else 0) = x i
Tactic: simp_rw [coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
simp_rw : (∑ x_1 : Fin g.natDegree, if (↑x_1 : ℕ) = (↑i : ℕ) then x x_1 else 0) = x i
simp_rw₁ : (∑ x_1 : Fin g.natDegree, if x_1 = i then x x_1 else 0) = x i
⊢ ∑ b : Fin g.natDegree, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (x b)) (↑i : ℕ) = x i
have simp_rw₂ : (if Membership.mem (γ := Finset (Fin g.natDegree)) Finset.univ i then x i else 0) = x i
Tactic: simp_rw [coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
⊢ degree.{u_1} (R := R) (∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (x i)) < g.degree
have simp_rw : degree.{u_1} (R := R)
    (∑ x_1 : Fin g.natDegree,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x x_1) : R[X]) (HPow.hPow (α := R[X]) X (↑x_1 : ℕ))) <
  g.degree
Tactic: simp_rw [← C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ (powerBasisAux' hg : (a : Fin g.natDegree) → AdjoinRoot g) i = root g ^ (↑i : ℕ)
have simp : (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: simp only [powerBasisAux', Basis.coe_ofEquivFun, LinearEquiv.coe_symm_mk]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ (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 : ℕ)
have 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 : ℕ)
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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 : ℕ)
⊢ (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 : ℕ)
have 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])
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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])
⊢ (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 : ℕ)
have 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])
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ (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 : ℕ)
have rw : (mk g : (a : R[X]) → AdjoinRoot g) ((monomial (↑i : ℕ) : (a : R) → R[X]) 1) = root g ^ (↑i : ℕ)
Tactic: rw [Pi.single_eq_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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 : ℕ)
⊢ (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 : ℕ)
have rw₁ : (mk g : (a : R[X]) → AdjoinRoot g) (HPow.hPow (α := R[X]) X (↑i : ℕ)) = root g ^ (↑i : ℕ)
Tactic: rw [Pi.single_eq_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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 : ℕ)
⊢ (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 : ℕ)
have rw₂ : HPow.hPow (α := AdjoinRoot g) ((mk g : (a : R[X]) → AdjoinRoot g) X) (↑i : ℕ) = root g ^ (↑i : ℕ)
Tactic: rw [Pi.single_eq_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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 : ℕ)
⊢ (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 : ℕ)
have rw₃ : root g ^ (↑i : ℕ) = root g ^ (↑i : ℕ)
Tactic: rw [Pi.single_eq_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ 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])
have 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])
Tactic: rw [← monomial_zero_right _, Pi.single_eq_of_ne hj]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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])
⊢ 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])
have rw : ℕ
Tactic: rw [← monomial_zero_right _, Pi.single_eq_of_ne hj]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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 : ℕ
⊢ 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])
have h₁ : Eq.{u_1 + 1} (α := R[X]) ((monomial (↑j : ℕ) : (a : R) → R[X]) 0) ((monomial (↑j : ℕ) : (a : R) → R[X]) 0)
Tactic: rw [← monomial_zero_right _, Pi.single_eq_of_ne hj]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
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
⊢ 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])
have this : Membership.mem (γ := Finset (Fin g.natDegree)) Finset.univ i
Tactic: have := Finset.mem_univ i
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
⊢ minpoly K (root f) = HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
have f'_monic : (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
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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])
have 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)
Tactic: refine (minpoly.unique K _ f'_monic ?_ ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
⊢ minpoly K (root f) = HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
have 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
Tactic: refine (minpoly.unique K _ f'_monic ?_ ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ 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)
have 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
Tactic: rw [map_mul, aeval_eq, mk_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ 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)
have 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
Tactic: rw [map_mul, aeval_eq, mk_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ 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)
have 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
Tactic: rw [map_mul, aeval_eq, mk_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ 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)
have refine_1₃ : Eq.{u_5 + 1} (α := AdjoinRoot f) 0 0
Tactic: rw [map_mul, aeval_eq, mk_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
⊢ (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
    ((((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)
have h₁ : Eq (α := AdjoinRoot f) ((algebraMap K (AdjoinRoot f) : (a : K) → AdjoinRoot f) x : AdjoinRoot f)
  ((of f : (a : K) → AdjoinRoot f) x : AdjoinRoot f)
Tactic: simp only [RingHom.comp_apply, mk_C, lift_of]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
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)
⊢ (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).degree ≤ q.degree
have commutes : (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]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).degree ≤ q.degree
have refine_2 : f.natDegree ≤ q.natDegree
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]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).degree ≤ q.degree
have refine_2₁ : Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
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]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ f.natDegree ≤ q.natDegree
have refine_2 : f ∣ q
Tactic: apply natDegree_le_of_dvd
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ f.natDegree ≤ q.natDegree
have refine_2₁ : q ≠ 0
Tactic: apply natDegree_le_of_dvd
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
have 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)
Tactic: rw [← commutes, RingHom.comp_apply, mk_self, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
⊢ Eq (α := AdjoinRoot f) ((mk f : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
have 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)
Tactic: rw [← commutes, RingHom.comp_apply, mk_self, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
⊢ Eq (α := AdjoinRoot f) ((mk f : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
have rw₂ : Eq (α := AdjoinRoot f) ((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval : (a : AdjoinRoot q) → AdjoinRoot f) 0) 0
Tactic: rw [← commutes, RingHom.comp_apply, mk_self, map_zero]