awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : Field S
inst_2 : Algebra T S
a b c : T
x1 x2 : S
ha : Ne.{u_3 + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)
⊢ (HAdd.hAdd (β := S[X])
          (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
              (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
            HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
          ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])).roots =
      {x1, x2} ↔
    x1 + x2 =
        HDiv.hDiv (α := S) (β := S) (-(algebraMap T S : (a : T) → S) b : S) ((algebraMap T S : (a : T) → S) a : S) ∧
      x1 * x2 =
        HDiv.hDiv (α := S) (β := S) ((algebraMap T S : (a : T) → S) c : S) ((algebraMap T S : (a : T) → S) a : S)

Tactic:
roots_quadratic_eq_pair_iff_of_ne_zero' ha

Premises used: Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero'
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : Field S
inst_2 : Algebra T S
a b c : T
x1 x2 : S
ha : Ne.{u_3 + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)
⊢ (HAdd.hAdd (β := S[X])
          (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
              (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
            HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
          ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])).roots =
      {x1, x2} ↔
    x1 + x2 =
        HDiv.hDiv (α := S) (β := S) (-(algebraMap T S : (a : T) → S) b : S) ((algebraMap T S : (a : T) → S) a : S) ∧
      x1 * x2 =
        HDiv.hDiv (α := S) (β := S) ((algebraMap T S : (a : T) → S) c : S) ((algebraMap T S : (a : T) → S) a : S)

Tactic:
exact roots_quadratic_eq_pair_iff_of_ne_zero' ha

Premises used: Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero'
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
simp : (↑(if p.coeff n = 0 then 0 else Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) ⋯) : R) = p.coeff n
⊢ (↑((p.toSubring T hp).coeff n) : R) = p.coeff n

Tactic:
simp only [toSubring, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]

Premises used: Finset.sum_ite_eq', Polynomial.toSubring, Polynomial.mem_support_iff, Polynomial.finsetSum_coeff, Ne, Polynomial.coeff_monomial, ite_not
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
neg : ∀ (h : ¬p.coeff n = 0), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) ⋯) : R) = p.coeff n
⊢ (↑(if p.coeff n = 0 then 0 else Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) ⋯) : R) = p.coeff n

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
h : p.coeff n = 0
pos : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
⊢ (↑0 : R) = p.coeff n

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
h : p.coeff n = 0
⊢ Eq.{u_1 + 1} (α := R) (↑0 : R) 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
h : ¬p.coeff n = 0
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) ⋯) : R) = p.coeff n

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
simp : (↑(if p.coeff n = 0 then 0 else Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) ⋯) : R) = p.coeff n
pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
neg neg₁ : ∀ (h : ¬p.coeff n = 0), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) ⋯) : R) = p.coeff n
⊢ (↑((p.toSubring T hp).coeff n) : R) = p.coeff n

Tactic:
classical
  simp only [toSubring, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl

Premises used: Finset.sum_ite_eq', Polynomial.toSubring, Polynomial.mem_support_iff, Polynomial.finsetSum_coeff, Ne, Polynomial.coeff_monomial, ite_not
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
⊢ (↑((p.toSubring T hp).coeff n) : R) = p.coeff n

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
h : ∀ (i : ℕ), i ∈ (p.toSubring T hp).support ↔ i ∈ p.support
⊢ (p.toSubring T hp).support = p.support

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
i : ℕ
h : (p.toSubring T hp).coeff i = 0 ↔ p.coeff i = 0
⊢ i ∈ (p.toSubring T hp).support ↔ i ∈ p.support

Tactic:
simp only [mem_support_iff, not_iff_not, Ne]

Premises used: not_iff_not, Polynomial.mem_support_iff, Ne
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
i : ℕ
rw : (↑((p.toSubring T hp).coeff i) : R) = 0
| p.coeff i = 0

Tactic:
rw [← coeff_toSubring p T hp]

Premises used: Polynomial.coeff_toSubring
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
i : ℕ
h : (p.toSubring T hp).coeff i = 0 ↔ (↑((p.toSubring T hp).coeff i) : R) = 0
⊢ (p.toSubring T hp).coeff i = 0 ↔ p.coeff i = 0

Tactic:
conv_rhs => rw [← coeff_toSubring p T hp]

Premises used: Polynomial.coeff_toSubring
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
i : ℕ
H : (p.toSubring T hp).coeff i = 0
rw : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (↑((p.toSubring T hp).coeff i) : R) = 0

Tactic:
rw [H, ZeroMemClass.coe_zero]

Premises used: ZeroMemClass.coe_zero
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
i : ℕ
⊢ (p.toSubring T hp).coeff i = 0 ↔ (↑((p.toSubring T hp).coeff i) : R) = 0

Tactic:
exact ⟨fun H => by rw [H, ZeroMemClass.coe_zero], fun H => Subtype.coe_injective H⟩
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
⊢ (p.toSubring T hp).degree = p.degree

Tactic:
simp [degree]

Premises used: Polynomial.degree
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
⊢ (p.toSubring T hp).natDegree = p.natDegree

Tactic:
simp [natDegree]

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
simp_rw : (p.toSubring T hp).coeff p.natDegree = 1 ↔ (↑((p.toSubring T hp).coeff p.natDegree) : R) = 1
⊢ (p.toSubring T hp).Monic ↔ p.Monic

Tactic:
simp_rw [Monic, leadingCoeff, natDegree_toSubring, ← coeff_toSubring p T hp]

Premises used: Polynomial.natDegree_toSubring, Polynomial.leadingCoeff, Polynomial.coeff_toSubring, Polynomial.Monic
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
H : (p.toSubring T hp).coeff p.natDegree = 1
rw : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ (↑((p.toSubring T hp).coeff p.natDegree) : R) = 1

Tactic:
rw [H, OneMemClass.coe_one]

Premises used: OneMemClass.coe_one
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
⊢ (p.toSubring T hp).coeff p.natDegree = 1 ↔ (↑((p.toSubring T hp).coeff p.natDegree) : R) = 1

Tactic:
exact ⟨fun H => by rw [H, OneMemClass.coe_one], fun H => Subtype.coe_injective H⟩
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
⊢ (↑(coeffs 0) : Set R) ⊆ (↑T : Set R)

Tactic:
simp [coeffs]

Premises used: Polynomial.coeffs
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
T : Subring R
a : ∀ (i : ℕ), (↑((toSubring 0 T ⋯).coeff i) : R) = (↑(coeff 0 i) : R)
⊢ toSubring 0 T ⋯ = 0

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
T : Subring R
i : ℕ
⊢ (↑((toSubring 0 T ⋯).coeff i) : R) = (↑(coeff 0 i) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
T : Subring R
i : ℕ
rw : Eq.{u_1 + 1} (α := R) (coeff 1 i) (↑(coeff 1 i) : R)
rw₁ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (↑(coeff 1 i) : R)
rw₂ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (↑(if i = 0 then 1 else 0) : R)
rw₃ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (if i = 0 then (↑1 : R) else (↑0 : R))
rw₄ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (if i = 0 then (↑1 : R) else 0)
rw₅ rw₆ : Eq.{u_1 + 1} (α := R) (if i = 0 then 1 else 0) (if i = 0 then 1 else 0)
⊢ (↑((toSubring 1 T ⋯).coeff i) : R) = (↑(coeff 1 i) : R)

Tactic:
rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
      OneMemClass.coe_one]

Premises used: Polynomial.coeff_one, OneMemClass.coe_one, apply_ite, ZeroMemClass.coe_zero, Polynomial.coeff_toSubring', Subtype.val
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
a : ∀ (n : ℕ), (map T.subtype (p.toSubring T hp)).coeff n = p.coeff n
⊢ map T.subtype (p.toSubring T hp) = p

Tactic:
ext n
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
⊢ (map T.subtype (p.toSubring T hp)).coeff n = p.coeff n

Tactic:
simp [coeff_map]

Premises used: Polynomial.coeff_map
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
simp : p.coeff n = 0 → 0 = (↑(p.coeff n) : R)
⊢ (ofSubring T p).coeff n = (↑(p.coeff n) : R)

Tactic:
simp only [ofSubring, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, Classical.not_not, ite_eq_left_iff]

Premises used: Finset.sum_ite_eq', ite_eq_left_iff, Classical.not_not, Polynomial.mem_support_iff, Polynomial.finsetSum_coeff, Ne, Polynomial.coeff_monomial, Polynomial.ofSubring
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
h : p.coeff n = 0
rw : Eq.{u_1 + 1} (α := R) 0 (↑0 : R)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 0 = (↑(p.coeff n) : R)

Tactic:
rw [h, ZeroMemClass.coe_zero]

Premises used: ZeroMemClass.coe_zero
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
i : R
hi : i ∈ (↑(ofSubring T p).coeffs : Set R)
⊢ ∃ (x : ℕ), ¬(ofSubring T p).coeff x = 0 ∧ (ofSubring T p).coeff x = i

Tactic:
simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe,
    (Finset.coe_image)] at hi

Premises used: Set.mem_image, Finset.coe_image, Polynomial.mem_support_iff, Ne, Polynomial.coeffs, Finset.mem_coe
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
i : R
hi : ∃ (x : ℕ), ¬(ofSubring T p).coeff x = 0 ∧ (ofSubring T p).coeff x = i
rcases : ∀ (n : ℕ), ¬(ofSubring T p).coeff n = 0 → ∀ (h'n : (ofSubring T p).coeff n = i), i ∈ (↑T : Set R)
⊢ i ∈ (↑T : Set R)

Tactic:
rcases hi with ⟨n, _, h'n⟩
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
i : R
n : ℕ
left : ¬(ofSubring T p).coeff n = 0
h'n : (ofSubring T p).coeff n = i
rw : (↑(p.coeff n) : R) ∈ (↑T : Set R)
⊢ i ∈ (↑T : Set R)

Tactic:
rw [← h'n, coeff_ofSubring]

Premises used: Polynomial.coeff_ofSubring
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
i : R
n : ℕ
left : ¬(ofSubring T p).coeff n = 0
h'n : (ofSubring T p).coeff n = i
⊢ (↑(p.coeff n) : R) ∈ (↑T : Set R)

Tactic:
Subtype.mem (coeff p n : T)

Premises used: Set.Mem, Polynomial.coeff, Subtype.mem
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
i : R
n : ℕ
left : ¬(ofSubring T p).coeff n = 0
h'n : (ofSubring T p).coeff n = i
⊢ (↑(p.coeff n) : R) ∈ (↑T : Set R)

Tactic:
exact Subtype.mem (coeff p n : T)

Premises used: Polynomial.coeff, Subtype.mem
-- Module: Mathlib.RingTheory.Polynomial.Subring
Goal:
R : Type u_1
inst : Ring R
T : Subring R
p : (↥T)[X]
intro intro₁ : ∀ ⦃i : R⦄ (hi : i ∈ (↑(ofSubring T p).coeffs : Set R)), i ∈ (↑T : Set R)
intro₂ : ∀ ⦃i : R⦄ (hi : ∃ (x : ℕ), ¬(ofSubring T p).coeff x = 0 ∧ (ofSubring T p).coeff x = i), i ∈ (↑T : Set R)
intro₃ : ∀ ⦃i : R⦄ (n : ℕ), ¬(ofSubring T p).coeff n = 0 → ∀ (h'n : (ofSubring T p).coeff n = i), i ∈ (↑T : Set R)
intro₄ :
  ∀ ⦃i : R⦄ (n : ℕ),
    ¬(ofSubring T p).coeff n = 0 → ∀ (h'n : (ofSubring T p).coeff n = i), (↑(p.coeff n) : R) ∈ (↑T : Set R)
⊢ (↑(ofSubring T p).coeffs : Set R) ⊆ (↑T : Set R)

Tactic:
classical
  intro i hi
  simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe,
    (Finset.coe_image)] at hi
  rcases hi with ⟨n, _, h'n⟩
  rw [← h'n, coeff_ofSubring]
  exact Subtype.mem (coeff p n : T)

Premises used: Set.mem_image, Finset.coe_image, Polynomial.mem_support_iff, Polynomial.coeff_ofSubring, Ne, Polynomial.coeffs, Finset.mem_coe
-- Module: Mathlib.RingTheory.Polynomial.Tower
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : B
p : R[X]
rw : eval₂ (algebraMap A B) x (map (algebraMap R A) p) = (aeval x : (a : R[X]) → B) p
rw₁ : eval₂ (algebraMap A B) x (map (algebraMap R A) p) = eval₂ (algebraMap R B) x p
rw₂ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p =
    eval₂ (algebraMap R B) x p
rw₃ rw₄ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p =
    eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p
⊢ Eq.{u_3 + 1} (α := B) ((aeval x : (a : A[X]) → B) (map (algebraMap R A) p) : B) ((aeval x : (a : R[X]) → B) p : B)

Tactic:
rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]

Premises used: Polynomial.eval₂_map, Polynomial.aeval_def, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Polynomial.Tower
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
p : R[X]
rw :
  eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
    (algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A)
rw₁ :
  eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
    (algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x p)
rw₂ :
  eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
    eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A))
      ((algebraMap A B : (a : A) → B) x) p
rw₃ rw₄ :
  eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p =
    eval₂ (algebraMap R B) ((algebraMap A B : (a : A) → B) x) p
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)

Tactic:
rw [aeval_def, aeval_def, hom_eval₂, ← IsScalarTower.algebraMap_eq]

Premises used: Polynomial.hom_eval₂, Polynomial.aeval_def, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Polynomial.Tower
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
inst_7 : IsDomain A
inst_8 : IsTorsionFree A B
inst_9 : Nontrivial B
x : A
p : R[X]
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) (β := B) ((aeval x : (a : R[X]) → A) p : A) 1 = 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₂ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) ∨ Eq.{u_3 + 1} (α := B) 1 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₃ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) ∨ False ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₄ rw₅ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)

Tactic:
rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
    iff_false_intro (one_ne_zero' B), or_false]

Premises used: one_ne_zero', iff_false_intro, Algebra.algebraMap_eq_smul_one, or_false, Polynomial.aeval_algebraMap_apply, smul_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Tower
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₁ :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
      ((algebraMap A B : (a : A) → B) 0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)

Tactic:
rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]

Premises used: Algebra.algebraMap, Function.Injective.eq_iff, RingHom.map_zero, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Polynomial.Tower
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
⊢ Eq.{u_2 + 1} (α := A) ((aeval (↑x : A) : (a : R[X]) → A) p : A) ((↑((aeval x : (a : R[X]) → ↥S) p) : A) : A)

Tactic:
aeval_algebraMap_apply A x p

Premises used: Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Polynomial.Tower
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp :
  Eq (α := A[X]) (((mapAlg R A : AlgHom.{u_1, u_1, u_2} R R[X] A[X]) : (a : R[X]) → A[X]) p : A[X])
    (Multiset.prod
        (Multiset.map (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) s) :
      A[X])
rw :
  Membership.mem (γ := Multiset A)
    (Multiset.map (α := A[X]) (⇑(aeval x) : (a : A[X]) → A)
      (Multiset.map (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) s))
    0
⊢ Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)

Tactic:
rw [← aeval_map_algebraMap A, ← mapAlg_eq_map, hp, map_multiset_prod, Multiset.prod_eq_zero]

Premises used: Polynomial.aeval_map_algebraMap, Multiset.prod_eq_zero, Polynomial.mapAlg_eq_map, map_multiset_prod
-- Module: Mathlib.RingTheory.Polynomial.Tower
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp :
  Eq (α := A[X]) (((mapAlg R A : AlgHom.{u_1, u_1, u_2} R R[X] A[X]) : (a : R[X]) → A[X]) p : A[X])
    (Multiset.prod
        (Multiset.map (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) s) :
      A[X])
rw :
  ∃ a ∈ s,
    Eq (α := A)
      (Function.comp (β := A[X]) (⇑(aeval x) : (a : A[X]) → A)
        (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) a)
      0
⊢ Membership.mem (γ := Multiset A)
    (Multiset.map (α := A[X]) (⇑(aeval x) : (a : A[X]) → A)
      (Multiset.map (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) s))
    0

Tactic:
rw [Multiset.map_map, Multiset.mem_map]

Premises used: Multiset.mem_map, Multiset.map_map
-- Module: Mathlib.RingTheory.Polynomial.Tower
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp :
  Eq (α := A[X]) (((mapAlg R A : AlgHom.{u_1, u_1, u_2} R R[X] A[X]) : (a : R[X]) → A[X]) p : A[X])
    (Multiset.prod
        (Multiset.map (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) s) :
      A[X])
⊢ Eq (α := A)
    (Function.comp (β := A[X]) (⇑(aeval x) : (a : A[X]) → A)
      (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) x)
    0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Tower
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp :
  Eq (α := A[X]) (((mapAlg R A : AlgHom.{u_1, u_1, u_2} R R[X] A[X]) : (a : R[X]) → A[X]) p : A[X])
    (Multiset.prod
        (Multiset.map (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) s) :
      A[X])
⊢ ∃ a ∈ s,
    Eq (α := A)
      (Function.comp (β := A[X]) (⇑(aeval x) : (a : A[X]) → A)
        (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) a)
      0

Tactic:
exact ⟨x, hx, by simp⟩
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f : R[X]
⊢ WellFounded.{u_1 + 1} (α := R[X]) DvdNotUnit

Tactic:
RelHomClass.wellFounded
          (⟨fun p : R[X] =>
              ((if p = 0 then ⊤ else ↑p.degree : WithTop (WithBot ℕ)), p.leadingCoeff), ?_⟩ :
            DvdNotUnit →r Prod.Lex (· < ·) DvdNotUnit)
          (wellFounded_lt.prod_lex ‹WfDvdMonoid R›.wf)

Premises used: RelHomClass.wellFounded, Polynomial.leadingCoeff, Prod.mk, Polynomial.degree, IsWellFounded.wf, WithTop.some, wellFounded_lt, RelHom.mk, Top.top, OfNat.ofNat, Eq, WellFounded.prod_lex, ite