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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
rw : eval₂ i x (h.repr z) - eval₂ i x w = 0
rw₁ : eval₂ i x (h.repr z - w) = 0
rw₂ : eval₂ i x (f * y) = 0
rw₃ : eval₂ i x f * eval₂ i x y = 0
rw₄ : 0 * eval₂ i x y = 0
rw₅ rw₆ : Eq.{u_1 + 1} (α := T) 0 0
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Tactic:
rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_mul]

Premises used: sub_eq_zero, MulZeroClass.zero_mul, Polynomial.eval₂_sub, Polynomial.eval₂_mul
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx_1 hx : eval₂ i x f = 0
⊢ eval₂ i x (h.repr 1) = 1

Tactic:
simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ (map_one _)]

Premises used: map_one, IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx_1 hx : eval₂ i x f = 0
z w : S
⊢ eval₂ i x (h.repr (z * w)) = eval₂ i x (h.repr z) * eval₂ i x (h.repr w)

Tactic:
simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z * h.repr w)]

Premises used: HMul.hMul, IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq, IsAdjoinRoot.repr
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx_1 hx : eval₂ i x f = 0
⊢ eval₂ i x (h.repr 0) = 0

Tactic:
simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ (map_zero _)]

Premises used: map_zero, IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx_1 hx : eval₂ i x f = 0
z w : S
⊢ eval₂ i x (h.repr (z + w)) = eval₂ i x (h.repr z) + eval₂ i x (h.repr w)

Tactic:
simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z + h.repr w)]

Premises used: HAdd.hAdd, IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq, IsAdjoinRoot.repr
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : R[X]
⊢ (h.lift i x hx : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) = eval₂ i x z

Tactic:
simp [lift, h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ rfl]

Premises used: IsAdjoinRoot.lift, IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq, rfl
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
rw : (h.lift i x hx : (a : S) → T) ((h.map : (a : R[X]) → S) X : S) = x
rw₁ : eval₂ i x X = x
rw₂ rw₃ : x = x
⊢ (h.lift i x hx : (a : S) → T) h.root = x

Tactic:
rw [← h.map_X, lift_map, eval₂_X]

Premises used: IsAdjoinRoot.map_X, IsAdjoinRoot.lift_map, Polynomial.eval₂_X
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
a : R
⊢ Eq.{u_1 + 1} (α := T) ((h.lift i x hx : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T)
    ((i : (a : R) → T) a : T)

Tactic:
simp [h.algebraMap_apply]

Premises used: IsAdjoinRoot.algebraMap_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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
g : S →+* T
hmap :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := T) ((g : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T) ((i : (a : R) → T) a : T)
hroot : (g : (a : S) → T) h.root = x
a : S
rw :
  Eq.{u_1 + 1} (α := T)
    ((g : (a : S) → T)
        ((h.map : (a : R[X]) → S)
            (∑ i ∈ Finset.range ((h.repr a).natDegree + 1),
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((h.repr a).coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)) :
          S) :
      T)
    ((h.lift i x hx : (a : S) → T)
        ((h.map : (a : R[X]) → S)
            (∑ i ∈ Finset.range ((h.repr a).natDegree + 1),
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((h.repr a).coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)) :
          S) :
      T)
⊢ Eq.{u_1 + 1} (α := T) ((g : (a : S) → T) a : T) ((h.lift i x hx : (a : S) → T) a : T)

Tactic:
rw [← h.map_repr a, Polynomial.as_sum_range_C_mul_X_pow (h.repr a)]

Premises used: IsAdjoinRoot.map_repr, Polynomial.as_sum_range_C_mul_X_pow, IsAdjoinRoot.repr
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
g : S →+* T
hmap :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := T) ((g : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T) ((i : (a : R) → T) a : T)
hroot : (g : (a : S) → T) h.root = x
a : S
⊢ Eq.{u_1 + 1} (α := T)
    ((g : (a : S) → T)
        ((h.map : (a : R[X]) → S)
            (∑ i ∈ Finset.range ((h.repr a).natDegree + 1),
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((h.repr a).coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)) :
          S) :
      T)
    ((h.lift i x hx : (a : S) → T)
        ((h.map : (a : R[X]) → S)
            (∑ i ∈ Finset.range ((h.repr a).natDegree + 1),
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((h.repr a).coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)) :
          S) :
      T)

Tactic:
simp [← h.algebraMap_apply, *]

Premises used: IsAdjoinRoot.algebraMap_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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
g : S →+* T
hmap :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := T) ((g : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T) ((i : (a : R) → T) a : T)
hroot : (g : (a : S) → T) h.root = x
⊢ g = h.lift i x hx

Tactic:
RingHom.ext (h.apply_eq_lift hx g hmap hroot)

Premises used: RingHom.ext, IsAdjoinRoot.apply_eq_lift
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
x : T
inst_4 : Algebra R T
hx' : Eq.{u_1 + 1} (α := T) ((aeval x : (a : R[X]) → T) f : T) (0 : T)
⊢ (↑(h.liftHom x hx') : S →+* T) = h.lift (algebraMap R T) x hx'

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, IsAdjoinRoot.lift, RingHomClass.toRingHom, rfl
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
x : T
inst_4 : Algebra R T
hx' : Eq.{u_1 + 1} (α := T) ((aeval x : (a : R[X]) → T) f : T) (0 : T)
z : S
⊢ Eq.{u_1 + 1} (α := T) ((h.lift (algebraMap R T) x hx' : (a : S) → T) z : T) ((h.liftHom x hx' : (a : S) → T) z : T)

Tactic:
rfl

Premises used: rfl
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
x : T
inst_4 : Algebra R T
hx' : Eq.{u_1 + 1} (α := T) ((aeval x : (a : R[X]) → T) f : T) (0 : T)
z : R[X]
rw :
  Eq.{u_1 + 1} (α := T) ((h.lift (algebraMap R T) x hx' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
    ((aeval x : (a : R[X]) → T) z : T)
rw₁ : eval₂ (algebraMap R T) x z = (aeval x : (a : R[X]) → T) z
rw₂ rw₃ : eval₂ (algebraMap R T) x z = eval₂ (algebraMap R T) x z
⊢ Eq.{u_1 + 1} (α := T) ((h.liftHom x hx' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
    ((aeval x : (a : R[X]) → T) z : T)

Tactic:
rw [← lift_algebraMap_apply, lift_map, aeval_def]

Premises used: Polynomial.aeval_def, IsAdjoinRoot.lift_map, IsAdjoinRoot.lift_algebraMap_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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
x : T
inst_4 : Algebra R T
hx' : Eq.{u_1 + 1} (α := T) ((aeval x : (a : R[X]) → T) f : T) (0 : T)
rw : (h.lift (algebraMap R T) x hx' : (a : S) → T) h.root = x
rw₁ rw₂ : x = x
⊢ (h.liftHom x hx' : (a : S) → T) h.root = x

Tactic:
rw [← lift_algebraMap_apply, lift_root]

Premises used: IsAdjoinRoot.lift_root, IsAdjoinRoot.lift_algebraMap_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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
x : T
inst_4 : Algebra R T
hx' : Eq.{u_1 + 1} (α := T) ((aeval x : (a : R[X]) → T) f : T) (0 : T)
g : S →ₐ[R] T
hroot : (g : (a : S) → T) h.root = x
⊢ g = h.liftHom x hx'

Tactic:
AlgHom.ext (h.apply_eq_lift hx' g g.commutes hroot)

Premises used: AlgHom.ext, RingHomClass.toRingHom, AlgHom.commutes, IsAdjoinRoot.apply_eq_lift
-- 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 : IsAdjoinRoot S f
hf : f ≠ 0
⊢ f ≠ 0 ∧ Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) f : S) (0 : S)

Tactic:
simp [hf]
-- 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 :
  ∀ (x : R[X]),
    Membership.mem (γ := Ideal R[X]) (RingHom.ker (mkₐ f)) x ↔ Membership.mem (γ := Ideal R[X]) (Ideal.span {f}) x
⊢ Eq (α := Ideal R[X]) (RingHom.ker (mkₐ f)) (Ideal.span {f})

Tactic:
ext
-- 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
x : R[X]
⊢ Membership.mem (γ := Ideal R[X]) (RingHom.ker (mkₐ f)) x ↔ Membership.mem (γ := Ideal R[X]) (Ideal.span {f}) x

Tactic:
simp [Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
inst : CommRing R
f : R[X]
hf : f.Monic
⊢ (AdjoinRoot.isAdjoinRootMonic f hf).toIsAdjoinRoot = AdjoinRoot.isAdjoinRoot f

Tactic:
rfl

Premises used: AdjoinRoot.isAdjoinRoot, rfl
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
inst : CommRing R
f : R[X]
⊢ (AdjoinRoot.isAdjoinRoot f).map = mkₐ f

Tactic:
rfl

Premises used: AdjoinRoot.mkₐ, Ideal.Quotient.mkₐ, rfl
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
inst : CommRing R
f : R[X]
⊢ (AdjoinRoot.isAdjoinRoot f).root = root f

Tactic:
simp [AdjoinRoot.isAdjoinRoot, IsAdjoinRoot.root]

Premises used: IsAdjoinRoot.root, AdjoinRoot.isAdjoinRoot
-- 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 : R[X]
rw : f ∣ f * (g /ₘ f)
⊢ Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (g %ₘ f) : S) ((h.map : (a : R[X]) → S) g : S)

Tactic:
rw [← RingHom.sub_mem_ker_iff, mem_ker_map, modByMonic_eq_sub_mul_div, sub_right_comm,
    sub_self, zero_sub, dvd_neg]

Premises used: IsAdjoinRoot.mem_ker_map, sub_self, Polynomial.modByMonic_eq_sub_mul_div, sub_right_comm, dvd_neg, RingHom.sub_mem_ker_iff, zero_sub
-- 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 : R[X]
⊢ f ∣ f * (g /ₘ f)

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- 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 : R[X]
⊢ f ∣ f * (g /ₘ f)

Tactic:
exact ⟨_, rfl⟩
-- 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 : R[X]
rw : Membership.mem (γ := Ideal R[X]) (RingHom.ker h.map) (h.repr ((h.map : (a : R[X]) → S) g) - g)
rw₁ :
  Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (h.repr ((h.map : (a : R[X]) → S) g)) : S)
    ((h.map : (a : R[X]) → S) g : S)
rw₂ rw₃ : Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) g : S) ((h.map : (a : R[X]) → S) g : S)
⊢ f ∣ h.repr ((h.map : (a : R[X]) → S) g) - g

Tactic:
rw [← h.mem_ker_map, RingHom.sub_mem_ker_iff, map_repr]

Premises used: IsAdjoinRoot.mem_ker_map, IsAdjoinRootMonic.toIsAdjoinRoot, IsAdjoinRoot.map_repr, RingHom.sub_mem_ker_iff
-- 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 y : S
rw : h.repr x %ₘ f + h.repr y %ₘ f
| h.repr (x + y) %ₘ f

Tactic:
rw [← h.map_repr x, ← h.map_repr y, ← map_add, h.modByMonic_repr_map, add_modByMonic]

Premises used: IsAdjoinRootMonic.toIsAdjoinRoot, IsAdjoinRoot.map_repr, map_add, Polynomial.add_modByMonic, IsAdjoinRootMonic.modByMonic_repr_map
-- 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 y : S
conv_lhs : h.repr (x + y) %ₘ f = h.repr x %ₘ f + h.repr y %ₘ f
conv_lhs₁ : h.repr x %ₘ f + h.repr y %ₘ f = h.repr x %ₘ f + h.repr y %ₘ f
⊢ h.repr (x + y) %ₘ f = h.repr x %ₘ f + h.repr y %ₘ f

Tactic:
conv_lhs =>
      rw [← h.map_repr x, ← h.map_repr y, ← map_add, h.modByMonic_repr_map, add_modByMonic]

Premises used: IsAdjoinRootMonic.toIsAdjoinRoot, IsAdjoinRoot.map_repr, map_add, Polynomial.add_modByMonic, IsAdjoinRootMonic.modByMonic_repr_map
-- 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
c : R
x : S
rw : h.repr (c • x) %ₘ f = c • (h.repr x %ₘ f)
rw₁ :
  h.repr (HSMul.hSMul (β := S) c ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₂ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) c : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₃ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((h.map : (a : R[X]) → S) ((C : (a : R) → R[X]) c : R[X]) : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₄ :
  h.repr ((h.map : (a : R[X]) → S) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (h.repr x))) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₅ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (h.repr x) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₆ : c • h.repr x %ₘ f = c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₇ : c • (h.repr x %ₘ f) = c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₈ rw₉ : c • (h.repr x %ₘ f) = c • (h.repr x %ₘ f)
⊢ h.repr (c • x) %ₘ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.repr x %ₘ f)

Tactic:
rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul,
        h.modByMonic_repr_map, ← smul_eq_C_mul, smul_modByMonic, h.map_repr]

Premises used: RingHom.id_apply, IsAdjoinRootMonic.toIsAdjoinRoot, Polynomial.smul_eq_C_mul, IsAdjoinRoot.map_repr, map_mul, IsAdjoinRoot.algebraMap_apply, Algebra.smul_def, Polynomial.smul_modByMonic, IsAdjoinRootMonic.modByMonic_repr_map
-- 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 : R[X]
⊢ (h.modByMonicHom : (a : S) → R[X]) ((h.map : (a : R[X]) → S) g) = g %ₘ f

Tactic:
h.modByMonic_repr_map g

Premises used: dite, Polynomial.modByMonic, IsAdjoinRootMonic.modByMonic_repr_map
-- 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.map : (a : R[X]) → S) ((h.modByMonicHom : (a : S) → R[X]) x : R[X]) = x

Tactic:
simp [modByMonicHom, map_modByMonic, map_repr]

Premises used: IsAdjoinRootMonic.map_modByMonic, IsAdjoinRoot.map_repr, 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
n : ℕ
hdeg : n < f.natDegree
⊢ 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
n : ℕ
hdeg : n < f.natDegree
h_1 : Nontrivial R
rw : (↑n : WithBot ℕ) < f.degree
⊢ (h.modByMonicHom : (a : S) → R[X]) (h.root ^ n) = HPow.hPow (α := R[X]) X n

Tactic:
rw [← h.map_X, ← map_pow, modByMonicHom_map, modByMonic_eq_self_iff h.monic, degree_X_pow]

Premises used: Polynomial.modByMonic_eq_self_iff, IsAdjoinRootMonic.toIsAdjoinRoot, IsAdjoinRoot.map_X, IsAdjoinRootMonic.modByMonicHom_map, map_pow, Polynomial.degree_X_pow, 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
n : ℕ
hdeg : n < f.natDegree
h_1 : Nontrivial R
contrapose! : ∀ (hdeg : f.degree ≤ (↑n : WithBot ℕ)), f.natDegree ≤ n
⊢ (↑n : WithBot ℕ) < f.degree

Tactic:
contrapose! hdeg
-- 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 : ℕ
h_1 : Nontrivial R
hdeg : f.degree ≤ (↑n : WithBot ℕ)
⊢ f.natDegree ≤ n

Tactic:
simpa [natDegree_le_iff_degree_le] using hdeg

Premises used: Polynomial.natDegree_le_iff_degree_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
hdeg : 1 < f.natDegree
⊢ Eq.{u + 1} (α := R[X]) ((h.modByMonicHom : (a : S) → R[X]) h.root : R[X]) (X : R[X])

Tactic:
simpa using modByMonicHom_root_pow h hdeg

Premises used: IsAdjoinRootMonic.modByMonicHom_root_pow
-- 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 y : S),
    Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) (x + y)))) ⋯ =
      HAdd.hAdd (α := Fin f.natDegree →₀ R)
        (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) ⋯)
        (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) y))) ⋯)

Tactic:
simp [Finsupp.comapDomain_add_of_injective Fin.val_injective]

Premises used: Fin.val_injective, Finsupp.comapDomain_add_of_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
⊢ ∀ (m : R) (x : S),
    Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) (m • x)))) ⋯ =
      HSMul.hSMul (α := R) (β := Fin f.natDegree →₀ R) ((RingHom.id R : (a : R) → R) m : R)
        (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) ⋯)

Tactic:
simp [Finsupp.comapDomain_smul_of_injective Fin.val_injective]

Premises used: Finsupp.comapDomain_smul_of_injective, 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
x : S
⊢ Nontrivial R

Tactic:
nontriviality R using Algebra.subsingleton R S
-- 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
simp :
  (h.map : (a : R[X]) → S)
      {
        toFinsupp :=
          Finsupp.mapDomain (α := Fin f.natDegree) Fin.val
            (Finsupp.comapDomain Fin.val (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x)) ⋯) } =
    x
⊢ (fun (g : Fin f.natDegree →₀ R) ↦
        ((h.map : (a : R[X]) → S) { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) : R[X] } : S))
      ((fun (x : S) ↦
          (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) ⋯ :
            Fin f.natDegree →₀ R))
        x) =
    x

Tactic:
simp only [AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff]

Premises used: AddMonoidAlgebra.coeff, 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
x : S
h_1 : Nontrivial R
hf : Function.Injective (α := Fin f.natDegree) Fin.val
hl :
  (↑(Finsupp.support.{0, u} (M := R) (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) : Set ℕ) ⊆
    Set.range (ι := Fin f.natDegree) Fin.val
⊢ (h.map : (a : R[X]) → S)
      {
        toFinsupp :=
          Finsupp.mapDomain (α := Fin f.natDegree) Fin.val
            (Finsupp.comapDomain Fin.val (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x)) ⋯) } =
    x

Tactic:
rw [Finsupp.mapDomain_comapDomain, Polynomial.eta, h.map_modByMonicHom x]

Premises used: Polynomial.eta, Finsupp.mapDomain_comapDomain, IsAdjoinRootMonic.map_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
⊢ Function.Injective (α := Fin f.natDegree) Fin.val

Tactic:
Fin.val_injective

Premises used: 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
x : S
h_1 : Nontrivial R
⊢ Function.Injective (α := Fin f.natDegree) Fin.val

Tactic:
exact Fin.val_injective

Premises used: 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
x : S
h_1 : Nontrivial R
i : ℕ
hi : i ∈ (↑(Finsupp.support.{0, u} (M := R) (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) : Set ℕ)
⊢ i ∈ Set.range (ι := Fin f.natDegree) Fin.val

Tactic:
Set.mem_range.mpr ⟨⟨i, ?_⟩, rfl⟩

Premises used: Iff.mpr, Set.mem_range, Fin.mk, Exists.intro, rfl
-- 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 : i ∈ (↑(Finsupp.support.{0, u} (M := R) (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) : Set ℕ)
hl : i < f.natDegree
⊢ i ∈ Set.range (ι := Fin f.natDegree) Fin.val

Tactic:
refine Set.mem_range.mpr ⟨⟨i, ?_⟩, rfl⟩

Premises used: Iff.mpr, Set.mem_range, Exists.intro, rfl
-- 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 : i ∈ (↑(Finsupp.support.{0, u} (M := R) (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) : Set ℕ)
hl :
  ∀ (hi : f.natDegree ≤ i),
    i ∉ (↑(Finsupp.support.{0, u} (M := R) (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) : Set ℕ)
⊢ i < f.natDegree

Tactic:
contrapose! hi