awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
x : S
h_1 : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
hl : Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ f, map_add' := ⋯ } : (a : S) → R[X]) x) i) 0
⊢ i ∉ (↑(Finsupp.support.{0, u} (M := R) (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) : Set ℕ)

Tactic:
simp only [Polynomial.toFinsupp_apply, Classical.not_not, Finsupp.mem_support_iff, Ne,
      modByMonicHom, LinearMap.coe_mk, Finset.mem_coe]

Premises used: Finsupp.mem_support_iff, LinearMap.coe_mk, Classical.not_not, Ne, Polynomial.toFinsupp_apply, Finset.mem_coe, IsAdjoinRootMonic.modByMonicHom
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
x : S
h_1 : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
hl :
  ∀ (h : IsAdjoinRootMonic.{u, v} (R := R) S 1) (hi : natDegree.{u} (R := R) 1 ≤ i),
    Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ 1, map_add' := ⋯ } : (a : S) → R[X]) x) i) 0
hl₁ :
  ∀ (hf : f ≠ 1),
    Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ f, map_add' := ⋯ } : (a : S) → R[X]) x) i) 0
⊢ Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ f, map_add' := ⋯ } : (a : S) → R[X]) x) i) 0

Tactic:
obtain rfl | hf := eq_or_ne f 1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
x : S
h_1 : Nontrivial R
i : ℕ
h : IsAdjoinRootMonic.{u, v} (R := R) S 1
hi : natDegree.{u} (R := R) 1 ≤ i
⊢ Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ 1, map_add' := ⋯ } : (a : S) → R[X]) x) i) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
x : S
h_1 : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
hf : f ≠ 1
⊢ Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ f, map_add' := ⋯ } : (a : S) → R[X]) x) i) 0

Tactic:
coeff_eq_zero_of_natDegree_lt <| (natDegree_modByMonic_lt _ h.monic hf).trans_le hi

Premises used: Polynomial.natDegree_modByMonic_lt, LT.lt.trans_le, Polynomial.coeff_eq_zero_of_natDegree_lt, IsAdjoinRootMonic.monic
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
x : S
h_1 : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
hf : f ≠ 1
⊢ Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ f, map_add' := ⋯ } : (a : S) → R[X]) x) i) 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt <| (natDegree_modByMonic_lt _ h.monic hf).trans_le hi

Premises used: Polynomial.natDegree_modByMonic_lt, LT.lt.trans_le, Polynomial.coeff_eq_zero_of_natDegree_lt, IsAdjoinRootMonic.monic
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
h₁ :
  ∀ (i : Fin f.natDegree),
    Eq (α := R)
      (((fun (x : S) ↦
                (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x)))
                    ⋯ :
                  Fin f.natDegree →₀ R))
              ((fun (g : Fin f.natDegree →₀ R) ↦
                  ((h.map : (a : R[X]) → S)
                      { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) : R[X] } :
                    S))
                g) :
            (a : Fin f.natDegree) → R)
          i :
        R)
      ((g : (a : Fin f.natDegree) → R) i : R)
⊢ (fun (x : S) ↦
        (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) ⋯ :
          Fin f.natDegree →₀ R))
      ((fun (g : Fin f.natDegree →₀ R) ↦
          ((h.map : (a : R[X]) → S) { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) : R[X] } : S))
        g) =
    g

Tactic:
ext i
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
h₁ : ({ toFinsupp := Finsupp.mapDomain Fin.val g : R[X] } %ₘ f).coeff (↑i : ℕ) = (g : (a : Fin f.natDegree) → R) i
⊢ Eq (α := R)
    (((fun (x : S) ↦
              (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x)))
                  ⋯ :
                Fin f.natDegree →₀ R))
            ((fun (g : Fin f.natDegree →₀ R) ↦
                ((h.map : (a : R[X]) → S)
                    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) : R[X] } :
                  S))
              g) :
          (a : Fin f.natDegree) → R)
        i :
      R)
    ((g : (a : Fin f.natDegree) → R) i : R)

Tactic:
simp only [AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff, h.modByMonicHom_map,
      Finsupp.comapDomain_apply, Polynomial.toFinsupp_apply]

Premises used: IsAdjoinRootMonic.modByMonicHom_map, AddMonoidAlgebra.coeff, Finsupp.comapDomain_apply, AddMonoidAlgebra.ofCoeff, Polynomial.toFinsupp_apply
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
h₁ : Eq (α := R) ((Finsupp.mapDomain Fin.val g : (a : ℕ) → R) (↑i : ℕ) : R) ((g : (a : Fin f.natDegree) → R) i : R)
h₂ : { toFinsupp := Finsupp.mapDomain Fin.val g : R[X] }.degree < f.degree
⊢ ({ toFinsupp := Finsupp.mapDomain Fin.val g : R[X] } %ₘ f).coeff (↑i : ℕ) = (g : (a : Fin f.natDegree) → R) i

Tactic:
rw [(Polynomial.modByMonic_eq_self_iff h.monic).mpr, Polynomial.coeff]

Premises used: Polynomial.modByMonic_eq_self_iff, Iff.mpr, Polynomial.coeff, IsAdjoinRootMonic.monic
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
h₁ h₂ : Eq (α := R) ((g : (a : Fin f.natDegree) → R) i : R) ((g : (a : Fin f.natDegree) → R) i : R)
⊢ Eq (α := R) ((Finsupp.mapDomain Fin.val g : (a : ℕ) → R) (↑i : ℕ) : R) ((g : (a : Fin f.natDegree) → R) i : R)

Tactic:
rw [Finsupp.mapDomain_apply Fin.val_injective]

Premises used: Finsupp.mapDomain_apply, Fin.val_injective
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
h₁ : ∀ (m : ℕ), f.natDegree ≤ m → { toFinsupp := Finsupp.mapDomain Fin.val g : R[X] }.coeff m = 0
⊢ { toFinsupp := Finsupp.mapDomain Fin.val g : R[X] }.degree < f.degree

Tactic:
rw [degree_eq_natDegree h.monic.ne_zero, degree_lt_iff_coeff_zero]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.degree_lt_iff_coeff_zero, Polynomial.Monic.ne_zero, IsAdjoinRootMonic.monic
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
h₁ : Eq (α := R) ((Finsupp.mapDomain Fin.val g : (a : ℕ) → R) m : R) (0 : R)
⊢ { toFinsupp := Finsupp.mapDomain Fin.val g : R[X] }.coeff m = 0

Tactic:
rw [Polynomial.coeff]

Premises used: Polynomial.coeff
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
h₁ : m ∉ Set.range (ι := Fin f.natDegree) Fin.val
⊢ Eq (α := R) ((Finsupp.mapDomain Fin.val g : (a : ℕ) → R) m : R) (0 : R)

Tactic:
rw [Finsupp.mapDomain_notin_range]

Premises used: Finsupp.mapDomain_notin_range
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
h₁ : ∀ (x : Fin f.natDegree), ¬(↑x : ℕ) = m
⊢ m ∉ Set.range (ι := Fin f.natDegree) Fin.val

Tactic:
rw [Set.mem_range, not_exists]

Premises used: Set.mem_range, not_exists
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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_1 i : Fin f.natDegree
hm : f.natDegree ≤ (↑i : ℕ)
⊢ False

Tactic:
i.prop.not_ge hm

Premises used: Fin.prop, LT.lt.not_ge
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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_1 i : Fin f.natDegree
hm : f.natDegree ≤ (↑i : ℕ)
⊢ False

Tactic:
exact i.prop.not_ge hm

Premises used: Fin.prop, LT.lt.not_ge
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
i : Fin f.natDegree
⊢ Eq.{max 1 (u + 1)} (α := Fin f.natDegree →₀ R)
    ((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) (h.root ^ (↑i : ℕ)) : Fin f.natDegree →₀ R)
    (Finsupp.single i 1 : Fin f.natDegree →₀ R)

Tactic:
simp [AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff, IsAdjoinRootMonic.basis]

Premises used: AddMonoidAlgebra.coeff, IsAdjoinRootMonic.basis, AddMonoidAlgebra.ofCoeff
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
rcases : ∀ (i : ℕ) (hi : i < f.natDegree), 0 < f.natDegree
⊢ 0 < f.natDegree

Tactic:
rcases h.basis.index_nonempty with ⟨⟨i, hi⟩⟩

Premises used: Module.Basis.index_nonempty, IsAdjoinRootMonic.basis
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
i : ℕ
hi : i < f.natDegree
⊢ 0 < f.natDegree

Tactic:
Nat.zero_lt_of_lt hi

Premises used: Nat.zero_lt_of_lt
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
i : ℕ
hi : i < f.natDegree
⊢ 0 < f.natDegree

Tactic:
exact Nat.zero_lt_of_lt hi

Premises used: Nat.zero_lt_of_lt
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
⊢ f.natDegree ≠ 0

Tactic:
h.deg_pos.ne'

Premises used: LT.lt.ne', IsAdjoinRootMonic.deg_pos
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
x : S
i : Fin f.natDegree
⊢ Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) x : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R) i : R)
    (coeff ((h.modByMonicHom : (a : S) → R[X]) x) (↑i : ℕ) : R)

Tactic:
simp [IsAdjoinRootMonic.basis, AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff, toFinsupp_apply]

Premises used: AddMonoidAlgebra.coeff, IsAdjoinRootMonic.basis, AddMonoidAlgebra.ofCoeff, Polynomial.toFinsupp_apply
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
rw₂ rw₃ : h.root = h.root
⊢ (h.basis : (a : Fin f.natDegree) → S) (⟨1, hdeg⟩ : Fin f.natDegree) = h.root

Tactic:
rw [h.basis_apply, Fin.val_mk, pow_one]

Premises used: Fin.val_mk, pow_one, IsAdjoinRootMonic.basis_apply
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
⊢ Module.Finite R S

Tactic:
(powerBasis h).finite

Premises used: PowerBasis.finite, IsAdjoinRootMonic.powerBasis
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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 : StrongRankCondition R
⊢ Module.finrank R S = f.natDegree

Tactic:
(powerBasis h).finrank

Premises used: PowerBasis.finrank, WithBot.recBotCoe, Polynomial.natDegree, IsAdjoinRootMonic.powerBasis, WithBot.unbotD
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
inst : CommRing R
f : R[X]
inst_1 : StrongRankCondition R
hf : f.Monic
⊢ Module.finrank R (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.span {f})) = f.natDegree

Tactic:
(AdjoinRoot.isAdjoinRootMonic _ hf).finrank

Premises used: IsAdjoinRootMonic.finrank, AdjoinRoot, AdjoinRoot.isAdjoinRootMonic
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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 : 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:
simp [coeff]

Premises used: IsAdjoinRootMonic.coeff
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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 : Fin 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 : R)

Tactic:
h.coeff_apply_lt z i i.prop

Premises used: Fin.prop, Fin.val, IsAdjoinRootMonic.coeff_apply_lt
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
simp : Eq.{u + 1} (α := R) (Polynomial.coeff ((h.modByMonicHom : (a : S) → R[X]) z) i) 0
⊢ Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) z i : R) (0 : R)

Tactic:
simp only [coeff, liftPolyₗ_apply, LinearMap.coe_mk, AddHom.coe_mk]

Premises used: LinearMap.coe_mk, IsAdjoinRootMonic.coeff, AddHom.coe_mk, IsAdjoinRootMonic.liftPolyₗ_apply
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
h_1 : Nontrivial R
⊢ Eq.{u + 1} (α := R) (Polynomial.coeff ((h.modByMonicHom : (a : S) → R[X]) z) i) 0

Tactic:
Polynomial.coeff_eq_zero_of_degree_lt
      ((degree_modByMonic_lt _ h.monic).trans_le (Polynomial.degree_le_of_natDegree_le hi))

Premises used: Polynomial.degree_le_of_natDegree_le, LT.lt.trans_le, Polynomial.degree_modByMonic_lt, Polynomial.coeff_eq_zero_of_degree_lt, IsAdjoinRootMonic.monic
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
h_1 : Nontrivial R
⊢ Eq.{u + 1} (α := R) (Polynomial.coeff ((h.modByMonicHom : (a : S) → R[X]) z) i) 0

Tactic:
exact
    Polynomial.coeff_eq_zero_of_degree_lt
      ((degree_modByMonic_lt _ h.monic).trans_le (Polynomial.degree_le_of_natDegree_le hi))

Premises used: Polynomial.degree_le_of_natDegree_le, LT.lt.trans_le, Polynomial.degree_modByMonic_lt, Polynomial.coeff_eq_zero_of_degree_lt, IsAdjoinRootMonic.monic
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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)
neg : ∀ (hi : ¬i < f.natDegree), Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) z i : R) (0 : 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)

Tactic:
split_ifs with hi
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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 : 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:
h.coeff_apply_lt z i hi

Premises used: IsAdjoinRootMonic.coeff_apply_lt
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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 : 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:
exact h.coeff_apply_lt z i hi

Premises used: IsAdjoinRootMonic.coeff_apply_lt
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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 : ¬i < f.natDegree
⊢ Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) z i : R) (0 : R)

Tactic:
h.coeff_apply_le z i (le_of_not_gt hi)

Premises used: le_of_not_gt, IsAdjoinRootMonic.coeff_apply_le
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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 : ¬i < f.natDegree
⊢ Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) z i : R) (0 : R)

Tactic:
exact h.coeff_apply_le z i (le_of_not_gt hi)

Premises used: le_of_not_gt, IsAdjoinRootMonic.coeff_apply_le
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
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)
⊢ Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) (h.root ^ n) : ℕ → R)
    (Pi.single (M := fun (j : ℕ) ↦ R) n 1 : (j : ℕ) → R)

Tactic:
ext i
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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 : ℕ
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)
⊢ 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:
rw [coeff_apply]

Premises used: IsAdjoinRootMonic.coeff_apply
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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)
neg : ∀ (hi : ¬i < f.natDegree), Eq.{u + 1} (α := R) (0 : 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)

Tactic:
split_ifs with hi
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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)
rw₁ 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)
⊢ 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:
rw [h.basis_apply, Fin.val_mk]

Premises used: Fin.val_mk, IsAdjoinRootMonic.basis_apply
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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)
rw₂ 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)
⊢ 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:
rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]

Premises used: Finsupp.single_apply_left, Fin.val_injective, IsAdjoinRootMonic.basis, Finsupp.single_eq_pi_single, Module.Basis.repr_self