awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
h_1 : Nontrivial R
i : Fin f.natDegree
⊢ { toFinsupp := Finsupp.mapDomain Fin.val g : R[X] }.degree < f.degree
have h₁ : ∀ (m : ℕ), f.natDegree ≤ m → { toFinsupp := Finsupp.mapDomain Fin.val g : R[X] }.coeff m = 0
Tactic: rw [degree_eq_natDegree h.monic.ne_zero, degree_lt_iff_coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
h_1 : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ { toFinsupp := Finsupp.mapDomain Fin.val g : R[X] }.coeff m = 0
have h₁ : Eq (α := R) ((Finsupp.mapDomain Fin.val g : (a : ℕ) → R) m : R) (0 : R)
Tactic: rw [Polynomial.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
h_1 : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ Eq (α := R) ((Finsupp.mapDomain Fin.val g : (a : ℕ) → R) m : R) (0 : R)
have h₁ : m ∉ Set.range (ι := Fin f.natDegree) Fin.val
Tactic: rw [Finsupp.mapDomain_notin_range]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
h_1 : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ m ∉ Set.range (ι := Fin f.natDegree) Fin.val
have h₁ : ∀ (x : Fin f.natDegree), ¬(↑x : ℕ) = m
Tactic: rw [Set.mem_range, not_exists]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
⊢ 0 < f.natDegree
have rcases : ∀ (i : ℕ) (hi : i < f.natDegree), 0 < f.natDegree
Tactic: rcases h.basis.index_nonempty with ⟨⟨i, hi⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
⊢ (h.basis : (a : Fin f.natDegree) → S) (⟨1, hdeg⟩ : Fin f.natDegree) = h.root
have rw : h.root ^ (↑(⟨1, hdeg⟩ : Fin f.natDegree) : ℕ) = h.root
Tactic: rw [h.basis_apply, Fin.val_mk, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
rw : h.root ^ (↑(⟨1, hdeg⟩ : Fin f.natDegree) : ℕ) = h.root
⊢ (h.basis : (a : Fin f.natDegree) → S) (⟨1, hdeg⟩ : Fin f.natDegree) = h.root
have rw₁ : HPow.hPow (β := ℕ) h.root 1 = h.root
Tactic: rw [h.basis_apply, Fin.val_mk, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
rw : h.root ^ (↑(⟨1, hdeg⟩ : Fin f.natDegree) : ℕ) = h.root
rw₁ : HPow.hPow (β := ℕ) h.root 1 = h.root
⊢ (h.basis : (a : Fin f.natDegree) → S) (⟨1, hdeg⟩ : Fin f.natDegree) = h.root
have rw₂ : h.root = h.root
Tactic: rw [h.basis_apply, Fin.val_mk, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : f.natDegree ≤ i
⊢ Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) z i : R) (0 : R)
have simp : Eq.{u + 1} (α := R) (Polynomial.coeff ((h.modByMonicHom : (a : S) → R[X]) z) i) 0
Tactic: simp only [coeff, liftPolyₗ_apply, LinearMap.coe_mk, AddHom.coe_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : f.natDegree ≤ i
⊢ Eq.{u + 1} (α := R) (Polynomial.coeff ((h.modByMonicHom : (a : S) → R[X]) z) i) 0
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
⊢ Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) z i : R)
    (if hi : i < f.natDegree then
        (((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) z : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
          (⟨i, hi⟩ : Fin f.natDegree)
      else 0 :
      R)
have pos : ∀ (hi : i < f.natDegree),
  Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) z i : R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) z : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
pos :
  ∀ (hi : i < f.natDegree),
    Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) z i : R)
      ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) z : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
          (⟨i, hi⟩ : Fin f.natDegree) :
        R)
⊢ Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) z i : R)
    (if hi : i < f.natDegree then
        (((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) z : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
          (⟨i, hi⟩ : Fin f.natDegree)
      else 0 :
      R)
have neg : ∀ (hi : ¬i < f.natDegree), Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) z i : R) (0 : R)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
⊢ Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) (h.root ^ n) : ℕ → R)
    (Pi.single (M := fun (j : ℕ) ↦ R) n 1 : (j : ℕ) → R)
have h₁ : ∀ (i : ℕ),
  Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) (h.root ^ n) i : R) (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
⊢ Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) (h.root ^ n) i : R) (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
have h₁ : Eq.{u + 1} (α := R)
  (if hi : i < f.natDegree then
      (((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree)
    else 0 :
    R)
  (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
Tactic: rw [coeff_apply]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
⊢ Eq.{u + 1} (α := R)
    (if hi : i < f.natDegree then
        (((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) :
            (a : Fin f.natDegree) → R)
          (⟨i, hi⟩ : Fin f.natDegree)
      else 0 :
      R)
    (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
have pos : ∀ (hi : i < f.natDegree),
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
pos :
  ∀ (hi : i < f.natDegree),
    Eq.{u + 1} (α := R)
      ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) :
            (a : Fin f.natDegree) → R)
          (⟨i, hi⟩ : Fin f.natDegree) :
        R)
      (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
⊢ Eq.{u + 1} (α := R)
    (if hi : i < f.natDegree then
        (((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) :
            (a : Fin f.natDegree) → R)
          (⟨i, hi⟩ : Fin f.natDegree)
      else 0 :
      R)
    (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
have neg : ∀ (hi : ¬i < f.natDegree), Eq.{u + 1} (α := R) (0 : R) (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
⊢ Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
              ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
            Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
have rw : Eq.{u + 1} (α := R)
  ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
      (⟨i, hi⟩ : Fin f.natDegree) :
    R)
  ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ)) :
          Fin f.natDegree →₀ R) :
        (a : Fin f.natDegree) → R)
      (⟨i, hi⟩ : Fin f.natDegree) :
    R)
Tactic: rw [h.basis_apply, Fin.val_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
rw :
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ)) :
            Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
⊢ Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
              ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
            Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
have rw₁ : Eq.{u + 1} (α := R)
  ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
      (⟨i, hi⟩ : Fin f.natDegree) :
    R)
  ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
      (⟨i, hi⟩ : Fin f.natDegree) :
    R)
Tactic: rw [h.basis_apply, Fin.val_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
⊢ Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
              ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
            Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
have rw : Eq.{u + 1} (α := R) ((Finsupp.single ⟨n, hn⟩ 1 : (a : Fin f.natDegree) → R) (⟨i, hi⟩ : Fin f.natDegree) : R)
  (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
Tactic: rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
rw :
  Eq.{u + 1} (α := R) ((Finsupp.single ⟨n, hn⟩ 1 : (a : Fin f.natDegree) → R) (⟨i, hi⟩ : Fin f.natDegree) : R)
    (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
⊢ Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
              ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
            Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
have rw₁ : Eq.{u + 1} (α := R) ((Finsupp.single ⟨n, hn⟩ 1 : (a : Fin f.natDegree) → R) (⟨i, hi⟩ : Fin f.natDegree) : R)
  ((Finsupp.single (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 : (a : ℕ) → (fun (x : ℕ) ↦ R) n)
      (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) :
    (fun (x : ℕ) ↦ R) n)
Tactic: rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
rw :
  Eq.{u + 1} (α := R) ((Finsupp.single ⟨n, hn⟩ 1 : (a : Fin f.natDegree) → R) (⟨i, hi⟩ : Fin f.natDegree) : R)
    (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
rw₁ :
  Eq.{u + 1} (α := R) ((Finsupp.single ⟨n, hn⟩ 1 : (a : Fin f.natDegree) → R) (⟨i, hi⟩ : Fin f.natDegree) : R)
    ((Finsupp.single (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 : (a : ℕ) → (fun (x : ℕ) ↦ R) n)
        (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) :
      (fun (x : ℕ) ↦ R) n)
⊢ Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
              ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
            Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
have rw₂ : Eq.{u + 1} (α := R) ((Finsupp.single ⟨n, hn⟩ 1 : (a : Fin f.natDegree) → R) (⟨i, hi⟩ : Fin f.natDegree) : R)
  ((Finsupp.single ⟨n, hn⟩ 1 : (a : Fin f.natDegree) → (fun (x : ℕ) ↦ R) n) (⟨i, hi⟩ : Fin f.natDegree) :
    (fun (x : ℕ) ↦ R) n)
Tactic: rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
⊢ Eq.{u + 1} (α := R)
    (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
    (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R)
have rw : Eq.{u + 1} (α := R) (Pi.single (M := fun (x : ℕ) ↦ R) n 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
  (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R)
Tactic: rw [Fin.val_mk, Fin.val_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
rw :
  Eq.{u + 1} (α := R) (Pi.single (M := fun (x : ℕ) ↦ R) n 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
    (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R)
⊢ Eq.{u + 1} (α := R)
    (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
    (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R)
have rw₁ : Eq.{u + 1} (α := R) (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R) (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R)
Tactic: rw [Fin.val_mk, Fin.val_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
⊢ Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
have rw : Eq.{u + 1} (α := R)
  ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
      (⟨i, hi⟩ : Fin f.natDegree) :
    R)
  ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
            ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
          Fin f.natDegree →₀ R) :
        (a : Fin f.natDegree) → R)
      (⟨i, hi⟩ : Fin f.natDegree) :
    R)
Tactic: calc
      h.basis.repr (h.root ^ n) ⟨i, _⟩ = h.basis.repr (h.basis ⟨n, hn⟩) ⟨i, hi⟩ := by
        rw [h.basis_apply, Fin.val_mk]
      _ = Pi.single (M := fun _ => R) ((⟨n, hn⟩ : Fin _) : ℕ) (1 : (fun _ => R) n)
        ↑(⟨i, _⟩ : Fin _) := by
        rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
      _ = Pi.single (M := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
rw :
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
              ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
            Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
⊢ Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
have rw₁ : Eq.{u + 1} (α := R)
  ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
            ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
          Fin f.natDegree →₀ R) :
        (a : Fin f.natDegree) → R)
      (⟨i, hi⟩ : Fin f.natDegree) :
    R)
  (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
Tactic: calc
      h.basis.repr (h.root ^ n) ⟨i, _⟩ = h.basis.repr (h.basis ⟨n, hn⟩) ⟨i, hi⟩ := by
        rw [h.basis_apply, Fin.val_mk]
      _ = Pi.single (M := fun _ => R) ((⟨n, hn⟩ : Fin _) : ℕ) (1 : (fun _ => R) n)
        ↑(⟨i, _⟩ : Fin _) := by
        rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
      _ = Pi.single (M := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
rw :
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
              ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
            Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
rw₁ :
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R)
              ((h.basis : (a : Fin f.natDegree) → S) (⟨n, hn⟩ : Fin f.natDegree)) :
            Fin f.natDegree →₀ R) :
          (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
⊢ Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ n) : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R)
        (⟨i, hi⟩ : Fin f.natDegree) :
      R)
    (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
have rw₂ : Eq.{u + 1} (α := R)
  (Pi.single (M := fun (x : ℕ) ↦ R) (↑(⟨n, hn⟩ : Fin f.natDegree) : ℕ) 1 (↑(⟨i, hi⟩ : Fin f.natDegree) : ℕ) : R)
  (Pi.single (M := fun (x : ℕ) ↦ R) n 1 i : R)
Tactic: calc
      h.basis.repr (h.root ^ n) ⟨i, _⟩ = h.basis.repr (h.basis ⟨n, hn⟩) ⟨i, hi⟩ := by
        rw [h.basis_apply, Fin.val_mk]
      _ = Pi.single (M := fun _ => R) ((⟨n, hn⟩ : Fin _) : ℕ) (1 : (fun _ => R) n)
        ↑(⟨i, _⟩ : Fin _) := by
        rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
      _ = Pi.single (M := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : ¬i < f.natDegree
⊢ Eq.{u + 1} (α := R) (0 : R) (Pi.single (M := fun (j : ℕ) ↦ R) n 1 i : R)
have neg : i ≠ n
Tactic: rw [Pi.single_eq_of_ne]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
⊢ Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) 1 : ℕ → R) (Pi.single (M := fun (j : ℕ) ↦ R) 0 1 : (j : ℕ) → R)
have rw : Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) 1 : ℕ → R)
  ((h.coeff : (a : S) → ℕ → R) (HPow.hPow (β := ℕ) h.root 0) : ℕ → R)
Tactic: rw [← h.coeff_root_pow h.deg_pos, pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
rw :
  Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) 1 : ℕ → R)
    ((h.coeff : (a : S) → ℕ → R) (HPow.hPow (β := ℕ) h.root 0) : ℕ → R)
⊢ Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) 1 : ℕ → R) (Pi.single (M := fun (j : ℕ) ↦ R) 0 1 : (j : ℕ) → R)
have rw₁ : Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) 1 : ℕ → R) ((h.coeff : (a : S) → ℕ → R) 1 : ℕ → R)
Tactic: rw [← h.coeff_root_pow h.deg_pos, pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
⊢ Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) h.root : ℕ → R)
    (Pi.single (M := fun (j : ℕ) ↦ R) 1 1 : (j : ℕ) → R)
have rw : Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) h.root : ℕ → R)
  ((h.coeff : (a : S) → ℕ → R) (HPow.hPow (β := ℕ) h.root 1) : ℕ → R)
Tactic: rw [← h.coeff_root_pow hdeg, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
rw :
  Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) h.root : ℕ → R)
    ((h.coeff : (a : S) → ℕ → R) (HPow.hPow (β := ℕ) h.root 1) : ℕ → R)
⊢ Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) h.root : ℕ → R)
    (Pi.single (M := fun (j : ℕ) ↦ R) 1 1 : (j : ℕ) → R)
have rw₁ : Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) h.root : ℕ → R) ((h.coeff : (a : S) → ℕ → R) h.root : ℕ → R)
Tactic: rw [← h.coeff_root_pow hdeg, pow_one]