awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
⊢ Eq (α := (a : AdjoinRoot p) → AdjoinRoot q) (⇑(mapAlgEquiv f p q h) : (a : AdjoinRoot p) → AdjoinRoot q)
    (⇑(map (↑f : S →+* T) p q ⋯) : (a : AdjoinRoot p) → AdjoinRoot q)

Tactic:
rfl

Premises used: AdjoinRoot, AlgEquiv.toAlgHom, Quotient.liftOn', Set.Mem, AddCon.liftOn, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h_1 : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
this :
  Eq (α := S →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.toRingEquiv.symm : T →+* S) (↑f : S →+* T))
    (RingHom.id S)
⊢ Associated (Polynomial.map (↑f.symm : T →+* S) q) p

Tactic:
simpa [Polynomial.map_map, -RingEquiv.symm_mk, this]
        using associated_map_map f.symm.toRingHom h.symm

Premises used: RingEquiv.symm_mk, AlgEquiv.symm, Polynomial.associated_map_map, Associated.symm, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, Polynomial.map_map
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f : S →+* T) p) q
⊢ (mapAlgEquiv f p q h).symm = mapAlgEquiv f.symm q p ⋯

Tactic:
rfl

Premises used: AlgEquiv.symm, AdjoinRoot.mapAlgEquiv, AlgEquiv.ofAlgHom, Equiv.symm, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f g : S[X]
hgf : g ∣ f
⊢ g ∣ Polynomial.map (↑(AlgHom.id R S) : S →+* S) f

Tactic:
simpa
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f g : S[X]
hgf : g ∣ f
⊢ Eq (α := AdjoinRoot g) ((mk g : (a : S[X]) → AdjoinRoot g) f : AdjoinRoot g) (0 : AdjoinRoot g)

Tactic:
simp [mk_eq_zero, hgf]

Premises used: AdjoinRoot.mk_eq_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hgf : g ∣ f
⊢ Eq (α := (a : AdjoinRoot f) → AdjoinRoot g) (⇑(algHomOfDvd R f g hgf) : (a : AdjoinRoot f) → AdjoinRoot g)
    (⇑(liftAlgHom f (Algebra.ofId S (AdjoinRoot g)) (root g) ⋯) : (a : AdjoinRoot f) → AdjoinRoot g)

Tactic:
rfl

Premises used: AdjoinRoot, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hgf : g ∣ f
⊢ (algHomOfDvd R f g hgf : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g

Tactic:
simp [algHomOfDvd]

Premises used: AdjoinRoot.algHomOfDvd
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f g : S[X]
hfg : Associated f g
⊢ Associated (Polynomial.map (↑AlgEquiv.refl : S →+* S) f) g

Tactic:
simpa
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : Associated f g
⊢ Eq (α := (a : AdjoinRoot f) → AdjoinRoot g) (⇑(algEquivOfAssociated R f g hfg) : (a : AdjoinRoot f) → AdjoinRoot g)
    (⇑(algHomOfDvd R f g ⋯) : (a : AdjoinRoot f) → AdjoinRoot g)

Tactic:
rfl

Premises used: AdjoinRoot, AlgEquiv.toAlgHom, Quotient.liftOn', Set.Mem, AddCon.liftOn, AlgHom.id, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : Associated f g
⊢ Eq (α := AdjoinRoot g ≃ₐ[R] AdjoinRoot f) (AlgEquiv.symm (algEquivOfAssociated R f g hfg))
    (algEquivOfAssociated R g f ⋯)

Tactic:
rfl

Premises used: AlgEquiv.symm, AdjoinRoot.algEquivOfAssociated, AdjoinRoot.mapAlgEquiv, AlgEquiv.ofAlgHom, Equiv.symm, AlgEquiv.refl, Equiv.refl, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : Associated f g
⊢ Eq (α := AdjoinRoot f →ₐ[R] AdjoinRoot g) (↑(algEquivOfAssociated R f g hfg) : AdjoinRoot f →ₐ[R] AdjoinRoot g)
    (algHomOfDvd R f g ⋯)

Tactic:
rfl

Premises used: AdjoinRoot, AlgEquiv.toAlgHom, Quotient.liftOn', Set.Mem, AddCon.liftOn, AdjoinRoot.algHomOfDvd, AlgHom.id, AdjoinRoot.map, AdjoinRoot.mapAlgHom, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AdjoinRoot.lift, AddCon.Quotient, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : Associated f g
rw : (algHomOfDvd R f g ⋯ : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g
rw₁ rw₂ : root g = root g
⊢ (algEquivOfAssociated R f g hfg : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g

Tactic:
rw [coe_algEquivOfAssociated, algHomOfDvd_root]

Premises used: AdjoinRoot.algHomOfDvd_root, AdjoinRoot.coe_algEquivOfAssociated
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f_1 g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h : eval₂ i a f_1 = 0
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R U
f g : S[X]
hfg : f = g
rw rw₁ : Associated g g
⊢ Associated f g

Tactic:
rw [hfg]
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : f = g
⊢ Eq (α := (a : AdjoinRoot f) → AdjoinRoot g) (⇑(algEquivOfEq R f g hfg) : (a : AdjoinRoot f) → AdjoinRoot g)
    (⇑(algHomOfDvd R f g ⋯) : (a : AdjoinRoot f) → AdjoinRoot g)

Tactic:
rfl

Premises used: AdjoinRoot, AlgEquiv.toAlgHom, Quotient.liftOn', Set.Mem, AddCon.liftOn, AlgHom.id, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : f = g
⊢ Eq (α := AdjoinRoot g ≃ₐ[R] AdjoinRoot f) (AlgEquiv.symm (algEquivOfEq R f g hfg)) (algEquivOfEq R g f ⋯)

Tactic:
rfl

Premises used: AlgEquiv.symm, AdjoinRoot.algEquivOfEq, AdjoinRoot.algEquivOfAssociated, AdjoinRoot.mapAlgEquiv, AlgEquiv.ofAlgHom, Equiv.symm, AlgEquiv.refl, Equiv.refl, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : f = g
⊢ Eq (α := AdjoinRoot f →ₐ[R] AdjoinRoot g) (↑(algEquivOfEq R f g hfg) : AdjoinRoot f →ₐ[R] AdjoinRoot g)
    (algHomOfDvd R f g ⋯)

Tactic:
rfl

Premises used: AdjoinRoot, AlgEquiv.toAlgHom, Quotient.liftOn', Set.Mem, AddCon.liftOn, AdjoinRoot.algHomOfDvd, AlgHom.id, AdjoinRoot.map, AdjoinRoot.mapAlgHom, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AdjoinRoot.lift, AddCon.Quotient, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f g : S[X]
hfg : f = g
rw : (algHomOfDvd R f g ⋯ : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g
rw₁ rw₂ : root g = root g
⊢ (algEquivOfEq R f g hfg : (a : AdjoinRoot f) → AdjoinRoot g) (root f) = root g

Tactic:
rw [coe_algEquivOfEq, algHomOfDvd_root]

Premises used: AdjoinRoot.algHomOfDvd_root, AdjoinRoot.coe_algEquivOfEq
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : Field K
f : K[X]
inst_1 : Fact (Irreducible f)
⊢ IsMaximal (α := K[X]) (span {f})

Tactic:
PrincipalIdealRing.isMaximal_of_irreducible <| Fact.out

Premises used: PrincipalIdealRing.isMaximal_of_irreducible, Fact.out
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : Field K
f : K[X]
inst_1 : Fact (Irreducible f)
q : ℚ≥0
rw : Eq (α := AdjoinRoot f) (↑q : AdjoinRoot f) ((of f : (a : K) → AdjoinRoot f) (↑q : K))
⊢ (↑q : AdjoinRoot f) = HDiv.hDiv (α := AdjoinRoot f) (↑q.num : AdjoinRoot f) (↑q.den : AdjoinRoot f)

Tactic:
rw [← map_natCast (of f), ← map_natCast (of f), ← map_div₀, ← NNRat.cast_def]

Premises used: NNRat.cast_def, map_div₀, map_natCast, AdjoinRoot.of
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : Field K
f : K[X]
inst_1 : Fact (Irreducible f)
q : ℚ≥0
⊢ Eq (α := AdjoinRoot f) (↑q : AdjoinRoot f) ((of f : (a : K) → AdjoinRoot f) (↑q : K))

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : Field K
f : K[X]
inst_1 : Fact (Irreducible f)
q : ℚ≥0
x : AdjoinRoot f
p : K[X]
⊢ (fun (y : AdjoinRoot f) ↦ q • y = (of f : (a : K) → AdjoinRoot f) (↑q : K) * y) ((mk f : (a : K[X]) → AdjoinRoot f) p)

Tactic:
simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.nnqsmul_eq_C_mul]

Premises used: Polynomial.nnqsmul_eq_C_mul, AdjoinRoot.smul_mk, AdjoinRoot.mk, RingHom.comp_apply, RingHom.map_mul, AdjoinRoot.of
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : Field K
f : K[X]
inst_1 : Fact (Irreducible f)
q : ℚ
rw : Eq (α := AdjoinRoot f) (↑q : AdjoinRoot f) ((of f : (a : K) → AdjoinRoot f) (↑q : K))
⊢ (↑q : AdjoinRoot f) = HDiv.hDiv (α := AdjoinRoot f) (↑q.num : AdjoinRoot f) (↑q.den : AdjoinRoot f)

Tactic:
rw [← map_natCast (of f), ← map_intCast (of f), ← map_div₀, ← Rat.cast_def]

Premises used: map_intCast, Rat.cast_def, map_div₀, map_natCast, AdjoinRoot.of
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : Field K
f : K[X]
inst_1 : Fact (Irreducible f)
q : ℚ
⊢ Eq (α := AdjoinRoot f) (↑q : AdjoinRoot f) ((of f : (a : K) → AdjoinRoot f) (↑q : K))

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : Field K
f : K[X]
inst_1 : Fact (Irreducible f)
q : ℚ
x : AdjoinRoot f
p : K[X]
⊢ (fun (y : AdjoinRoot f) ↦ q • y = (of f : (a : K) → AdjoinRoot f) (↑q : K) * y) ((mk f : (a : K[X]) → AdjoinRoot f) p)

Tactic:
simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.qsmul_eq_C_mul]

Premises used: AdjoinRoot.smul_mk, AdjoinRoot.mk, RingHom.comp_apply, RingHom.map_mul, Polynomial.qsmul_eq_C_mul, AdjoinRoot.of
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
h : f.degree ≠ 0
⊢ Function.Injective (α := K) (β := AdjoinRoot f) (⇑(of f) : (a : K) → AdjoinRoot f)

Tactic:
have := AdjoinRoot.nontrivial f h
  (of f).injective

Premises used: RingHom.injective, AdjoinRoot.nontrivial, AdjoinRoot.of
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
inst_1 : Fact (Irreducible f)
⊢ Function.Injective (α := K) (β := AdjoinRoot f) (⇑(of f) : (a : K) → AdjoinRoot f)

Tactic:
(of f).injective

Premises used: RingHom.injective, AdjoinRoot.of
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
K : Type u_5
inst : Field K
f : K[X]
inst_1 : Fact (Irreducible f)
⊢ HSub.hSub (α := (AdjoinRoot f)[X]) (β := (AdjoinRoot f)[X]) X
        ((C : (a : AdjoinRoot f) → (AdjoinRoot f)[X]) (root f) : (AdjoinRoot f)[X]) *
      (Polynomial.map (of f) f /
        HSub.hSub (α := (AdjoinRoot f)[X]) (β := (AdjoinRoot f)[X]) X
          ((C : (a : AdjoinRoot f) → (AdjoinRoot f)[X]) (root f) : (AdjoinRoot f)[X])) =
    Polynomial.map (of f) f

Tactic:
(isRoot_root _).mul_div_eq

Premises used: Polynomial.IsRoot.mul_div_eq
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : IsNoetherianRing R
f : R[X]
⊢ IsNoetherianRing.{u_1} (AdjoinRoot f)

Tactic:
Ideal.Quotient.isNoetherianRing _

Premises used: AdjoinRoot, Ideal.Quotient.isNoetherianRing
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
⊢ IsIntegral R (root g)

Tactic:
⟨g, hg, eval₂_root g⟩

Premises used: RingHom.IsIntegralElem, IsIntegral, AdjoinRoot.eval₂_root, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
f : R[X]
⊢ (modByMonicHom hg : (a : AdjoinRoot g) → R[X]) ((mk g : (a : R[X]) → AdjoinRoot g) f) = f %ₘ g

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, dite, Polynomial.modByMonic, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
f : AdjoinRoot g
ih :
  ∀ (p : R[X]),
    Eq (α := AdjoinRoot g)
      ((mk g : (a : R[X]) → AdjoinRoot g)
          ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) ((mk g : (a : R[X]) → AdjoinRoot g) p)) :
        AdjoinRoot g)
      ((mk g : (a : R[X]) → AdjoinRoot g) p : AdjoinRoot g)
⊢ (mk g : (a : R[X]) → AdjoinRoot g) ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) f) = f

Tactic:
induction f using AdjoinRoot.induction_on
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
p : R[X]
ih : g ∣ g * (p /ₘ g)
⊢ Eq (α := AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g)
        ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) ((mk g : (a : R[X]) → AdjoinRoot g) p)) :
      AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) p : AdjoinRoot g)

Tactic:
rw [modByMonicHom_mk hg, mk_eq_mk, modByMonic_eq_sub_mul_div, sub_sub_cancel_left, dvd_neg]

Premises used: AdjoinRoot.mk_eq_mk, sub_sub_cancel_left, Polynomial.modByMonic_eq_sub_mul_div, AdjoinRoot.modByMonicHom_mk, dvd_neg
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
p : R[X]
⊢ g ∣ g * (p /ₘ g)

Tactic:
apply dvd_mul_right

Premises used: dvd_mul_right
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
⊢ Function.Surjective (α := R[X]) (β := AdjoinRoot g) (⇑(mk g) : (a : R[X]) → AdjoinRoot g)

Tactic:
Ideal.Quotient.mk_surjective

Premises used: AdjoinRoot, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
f₁ f₂ : AdjoinRoot g
i : Fin g.natDegree
⊢ coeff ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) (f₁ + f₂)) (↑i : ℕ) =
    HAdd.hAdd (α := Fin g.natDegree → R) (β := Fin g.natDegree → R)
      (fun (i : Fin g.natDegree) ↦ coeff ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) f₁) (↑i : ℕ))
      (fun (i : Fin g.natDegree) ↦ coeff ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) f₂) (↑i : ℕ)) i

Tactic:
simp only [(modByMonicHom hg).map_add, coeff_add, Pi.add_apply]

Premises used: LinearMap.map_add, AdjoinRoot.modByMonicHom, Polynomial.coeff_add, Pi.add_apply
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
f₁ : R
f₂ : AdjoinRoot g
i : Fin g.natDegree
⊢ coeff ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) (f₁ • f₂)) (↑i : ℕ) =
    HSMul.hSMul (α := R) (β := Fin g.natDegree → R) ((RingHom.id R : (a : R) → R) f₁ : R)
      (fun (i : Fin g.natDegree) ↦ coeff ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) f₂) (↑i : ℕ)) i

Tactic:
simp only [(modByMonicHom hg).map_smul, coeff_smul, Pi.smul_apply, RingHom.id_apply]

Premises used: RingHom.id_apply, AdjoinRoot.modByMonicHom, Polynomial.coeff_smul, LinearMap.map_smul, Pi.smul_apply
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
f_1 : AdjoinRoot g
f : R[X]
simp : g ∣ f - f %ₘ g
⊢ g ∣
    f -
      ∑ i : Fin g.natDegree,
        (monomial (↑i : ℕ) : (a : R) → R[X])
          ((fun (f : AdjoinRoot g) (i : Fin g.natDegree) ↦
              (coeff ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) f) (↑i : ℕ) : R))
            ((mk g : (a : R[X]) → AdjoinRoot g) f) i)

Tactic:
simp only [modByMonicHom_mk, sum_modByMonic_coeff hg degree_le_natDegree]

Premises used: Polynomial.degree_le_natDegree, AdjoinRoot.modByMonicHom_mk, Polynomial.sum_modByMonic_coeff
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
f_1 : AdjoinRoot g
f : R[X]
rw : g ∣ g * (f /ₘ g)
⊢ g ∣ f - f %ₘ g

Tactic:
rw [modByMonic_eq_sub_mul_div, sub_sub_cancel]

Premises used: Polynomial.modByMonic_eq_sub_mul_div, sub_sub_cancel
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
f_1 : AdjoinRoot g
f : R[X]
⊢ g ∣ g * (f /ₘ g)

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
f_1 : AdjoinRoot g
f : R[X]
⊢ g ∣ g * (f /ₘ g)

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
simp : ((∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (x i)) %ₘ g).coeff (↑i : ℕ) = x i
⊢ (fun (f : AdjoinRoot g) (i : Fin g.natDegree) ↦
        (coeff ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) f) (↑i : ℕ) : R))
      ((fun (c : Fin g.natDegree → R) ↦
          ((mk g : (a : R[X]) → AdjoinRoot g) (∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (c i)) :
            AdjoinRoot g))
        x)
      i =
    x i

Tactic:
simp only [modByMonicHom_mk]

Premises used: AdjoinRoot.modByMonicHom_mk
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
rw : ∑ b : Fin g.natDegree, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (x b)) (↑i : ℕ) = x i
rw₁ : degree.{u_1} (R := R) (∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (x i)) < g.degree
⊢ ((∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (x i)) %ₘ g).coeff (↑i : ℕ) = x i

Tactic:
rw [(modByMonic_eq_self_iff hg).mpr, finsetSum_coeff]

Premises used: Polynomial.modByMonic_eq_self_iff, Iff.mpr, Polynomial.finsetSum_coeff
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
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
simp_rw₂ : (if Membership.mem (γ := Finset (Fin g.natDegree)) Finset.univ i then x i else 0) = x i
⊢ ∑ b : Fin g.natDegree, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (x b)) (↑i : ℕ) = x i

Tactic:
simp_rw [coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]

Premises used: Finset.mem_univ, Finset.sum_ite_eq', Polynomial.coeff_monomial, if_pos, Fin.val_eq_val
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
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
⊢ degree.{u_1} (R := R) (∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) (x i)) < g.degree

Tactic:
simp_rw [← C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
⊢ 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:
(degree_eq_natDegree <| hg.ne_zero).symm ▸ degree_sum_fin_lt _

Premises used: Polynomial.degree_eq_natDegree, Eq.rec, Eq.symm, Polynomial.degree_sum_fin_lt, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
x : Fin g.natDegree → R
i : Fin g.natDegree
h : Nontrivial R
⊢ 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:
exact (degree_eq_natDegree <| hg.ne_zero).symm ▸ degree_sum_fin_lt _
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
c : Fin g.natDegree →₀ R
⊢ Eq (α := AdjoinRoot g) (((powerBasisAux' hg).repr.symm : (a : Fin g.natDegree →₀ R) → AdjoinRoot g) c : AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g)
        (∑ i : Fin g.natDegree, (monomial (↑i : ℕ) : (a : R) → R[X]) ((c : (a : Fin g.natDegree) → R) i)) :
      AdjoinRoot g)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
g : R[X]
hg : g.Monic
f : AdjoinRoot g
i : Fin g.natDegree
⊢ Eq (α := R)
    (((((powerBasisAux' hg).repr : (a : AdjoinRoot g) → Fin g.natDegree →₀ R) f : Fin g.natDegree →₀ R) :
          (a : Fin g.natDegree) → R)
        i :
      R)
    (coeff ((modByMonicHom hg : (a : AdjoinRoot g) → R[X]) f) (↑i : ℕ) : R)

Tactic:
rfl

Premises used: Polynomial.coeff, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
hg : g.Monic
i : Fin g.natDegree
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 : ℕ)
⊢ (powerBasisAux' hg : (a : Fin g.natDegree) → AdjoinRoot g) i = root g ^ (↑i : ℕ)

Tactic:
simp only [powerBasisAux', Basis.coe_ofEquivFun, LinearEquiv.coe_symm_mk]

Premises used: LinearEquiv.coe_symm_mk, Module.Basis.coe_ofEquivFun, AdjoinRoot.powerBasisAux'