awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
obtain : ∀ (p : R[X]) (hp : g = EuclideanDomain.gcd f g * p), eval₂ ϕ α g = 0
⊢ eval₂ ϕ α g = 0

Tactic:
obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_right f g

Premises used: EuclideanDomain.gcd_dvd_right
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : g = EuclideanDomain.gcd f g * p
rw : eval₂ ϕ α (EuclideanDomain.gcd f g * p) = 0
rw₁ : eval₂ ϕ α (EuclideanDomain.gcd f g) * eval₂ ϕ α p = 0
rw₂ : 0 * eval₂ ϕ α p = 0
rw₃ rw₄ : Eq.{y + 1} (α := k) 0 0
⊢ eval₂ ϕ α g = 0

Tactic:
rw [hp, Polynomial.eval₂_mul, hα, zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.eval₂_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0 ↔ eval₂ ϕ α f = 0 ∧ eval₂ ϕ α g = 0

Tactic:
⟨fun h => ⟨root_left_of_root_gcd h, root_right_of_root_gcd h⟩, fun h => eval₂_gcd_eq_zero h.1 h.2⟩

Premises used: Polynomial.root_left_of_root_gcd, And.right, And.left, Polynomial.root_right_of_root_gcd, And.intro, Iff.intro, Polynomial.eval₂_gcd_eq_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
f g : R[X]
α : R
⊢ (EuclideanDomain.gcd f g).IsRoot α ↔ f.IsRoot α ∧ g.IsRoot α

Tactic:
root_gcd_iff_root_left_right

Premises used: Polynomial.eval, Polynomial.IsRoot, Polynomial.root_gcd_iff_root_left_right
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
rw : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsCoprime p q
rw₁ : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsUnit (EuclideanDomain.gcd p q)
rw₂ : IsUnit (map f (EuclideanDomain.gcd p q)) ↔ IsUnit (EuclideanDomain.gcd p q)
rw₃ rw₄ : IsUnit (EuclideanDomain.gcd p q) ↔ IsUnit (EuclideanDomain.gcd p q)
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q

Tactic:
rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]

Premises used: Polynomial.isUnit_map, Polynomial.gcd_map, EuclideanDomain.gcd_isUnit_iff
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
rw : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsCoprime p q
rw₁ : IsUnit (EuclideanDomain.gcd (map f p) (map f q)) ↔ IsUnit (EuclideanDomain.gcd p q)
rw₂ : IsUnit (map f (EuclideanDomain.gcd p q)) ↔ IsUnit (EuclideanDomain.gcd p q)
rw₃ rw₄ : IsUnit (EuclideanDomain.gcd p q) ↔ IsUnit (EuclideanDomain.gcd p q)
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q

Tactic:
classical
  rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]

Premises used: Polynomial.isUnit_map, Polynomial.gcd_map, EuclideanDomain.gcd_isUnit_iff
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p : R[X]
inst_1 : CommRing k
inst_2 : IsDomain k
f : R →+* k
x : k
hp : p ≠ 0
rw : (map f p).IsRoot x ↔ eval₂ f x p = 0
rw₁ : eval x (map f p) = 0 ↔ eval₂ f x p = 0
rw₂ rw₃ : eval₂ f x p = 0 ↔ eval₂ f x p = 0
⊢ x ∈ (map f p).roots ↔ eval₂ f x p = 0

Tactic:
rw [mem_roots (map_ne_zero hp), IsRoot, Polynomial.eval_map]

Premises used: Polynomial.eval_map, Polynomial.IsRoot, Polynomial.mem_roots, Polynomial.map_ne_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
rw₁ : (↑(HSMul.hSMul (β := Multiset S) n {0}).toFinset : Set S) = {0}
rw₂ : (↑(Multiset.toFinset {0}) : Set S) = {0}
rw₃ : (↑{0} : Set S) = {0}
rw₄ rw₅ : Eq (α := Set S) {0} {0}
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}

Tactic:
rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]

Premises used: Finset.coe_singleton, Polynomial.rootSet, Multiset.toFinset_nsmul, Polynomial.aroots_monomial, Multiset.toFinset_singleton
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : (↑(aroots.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S).toFinset : Set S) = {0}
rw₁ : (↑(HSMul.hSMul (β := Multiset S) n {0}).toFinset : Set S) = {0}
rw₂ : (↑(Multiset.toFinset {0}) : Set S) = {0}
rw₃ : (↑{0} : Set S) = {0}
rw₄ rw₅ : Eq (α := Set S) {0} {0}
⊢ rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}

Tactic:
classical
  rw [rootSet, aroots_monomial ha,
    Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]

Premises used: Finset.coe_singleton, Polynomial.rootSet, Multiset.toFinset_nsmul, Polynomial.aroots_monomial, Multiset.toFinset_singleton
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
rw : rootSet.{u, v} (T := R) ((monomial n : (a : R) → R[X]) a) S = {0}
rw₁ rw₂ : Eq (α := Set S) {0} {0}
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).rootSet S = {0}

Tactic:
rw [C_mul_X_pow_eq_monomial, rootSet_monomial hn ha]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.rootSet_monomial
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
rw : Ne.{u + 1} (α := R) 1 0
⊢ (HPow.hPow (α := R[X]) X n).rootSet S = {0}

Tactic:
rw [← one_mul (X ^ n : R[X]), ← C_1, rootSet_C_mul_X_pow hn]

Premises used: Polynomial.C_1, Polynomial.rootSet_C_mul_X_pow, HPow.hPow, Polynomial.X, one_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ Ne.{u + 1} (α := R) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ Ne.{u + 1} (α := R) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
a : Ne.{v + 1} (α := S[X]) (∏ i ∈ s, map (algebraMap R S) (f i)) 0
⊢ (↑(roots (map (algebraMap R S) (s.prod f))).toFinset : Set S) =
    ⋃ i ∈ (↑s : Set ι), (↑(roots (map (algebraMap R S) (f i))).toFinset : Set S)

Tactic:
rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]

Premises used: Finset.coe_biUnion, Finset.val_toFinset, Polynomial.map_prod, Polynomial.roots_prod, Finset.bind_toFinset
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
a : Ne (α := S[X]) (map (algebraMap R S) (∏ i ∈ s, f i)) 0
a₁ : ¬Eq (α := S[X]) (map (algebraMap R S) (∏ i ∈ s, f i)) 0
a₂ a₃ a₄ a₅ : ¬Eq.{u + 1} (α := R[X]) (∏ i ∈ s, f i) 0
⊢ Ne.{v + 1} (α := S[X]) (∏ i ∈ s, map (algebraMap R S) (f i)) 0

Tactic:
rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]

Premises used: Ne, Polynomial.map_prod, Polynomial.map_eq_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Field R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
simp :
  (↑(roots (map (algebraMap R S) (s.prod f))).toFinset : Set S) =
    ⋃ i ∈ (↑s : Set ι), (↑(roots (map (algebraMap R S) (f i))).toFinset : Set S)
a : Ne.{v + 1} (α := S[X]) (∏ i ∈ s, map (algebraMap R S) (f i)) 0
⊢ (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S

Tactic:
classical
  simp only [rootSet, aroots, ← Finset.mem_coe]
  rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]
  rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]

Premises used: Finset.coe_biUnion, Polynomial.rootSet, Ne, Polynomial.map_prod, Polynomial.roots_prod, Polynomial.aroots, Polynomial.map_eq_zero, Finset.mem_coe, Finset.bind_toFinset
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a : R
inst : Field R
b : R
ha : a ≠ 0
⊢ (HSub.hSub (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).roots =
    {a⁻¹ * b}

Tactic:
simp [roots_C_mul_X_sub_C_of_IsUnit b ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩]

Premises used: mul_inv_cancel₀, Polynomial.roots_C_mul_X_sub_C_of_IsUnit, Inv.inv, Units.mk, inv_mul_cancel₀
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a : R
inst : Field R
b : R
ha : a ≠ 0
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).roots =
    {-(a⁻¹ * b)}

Tactic:
simp [roots_C_mul_X_add_C_of_IsUnit b ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩]

Premises used: mul_inv_cancel₀, Inv.inv, Units.mk, inv_mul_cancel₀, Polynomial.roots_C_mul_X_add_C_of_IsUnit
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 1
rw rw₁ : LE.le (α := WithBot ℕ) 1 1
⊢ p.degree ≤ 1

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 1
rw :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
        ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).roots =
    {-(((HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
                  ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
              1)⁻¹ *
          (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
                ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
            0)}
⊢ p.roots = {-((p.coeff 1)⁻¹ * p.coeff 0)}

Tactic:
rw [eq_X_add_C_of_degree_le_one (show degree p ≤ 1 by rw [h])]

Premises used: Polynomial.eq_X_add_C_of_degree_le_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 1
⊢ p.coeff 1 ≠ 0

Tactic:
have : p.coeff 1 ≠ 0 := coeff_ne_zero_of_eq_degree h
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 1
this : p.coeff 1 ≠ 0
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
        ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).roots =
    {-(((HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
                  ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
              1)⁻¹ *
          (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
                ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
            0)}

Tactic:
simp [roots_C_mul_X_add_C _ this]

Premises used: Polynomial.roots_C_mul_X_add_C
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 1
⊢ p ≠ 0

Tactic:
simp [← zero_le_degree_iff, h]

Premises used: Polynomial.zero_le_degree_iff
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 1
rw : -((p.coeff 1)⁻¹ * p.coeff 0) ∈ p.roots
⊢ p.IsRoot (-((p.coeff 1)⁻¹ * p.coeff 0))

Tactic:
rw [← mem_roots (by simp [← zero_le_degree_iff, h])]

Premises used: Polynomial.mem_roots
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 1
⊢ -((p.coeff 1)⁻¹ * p.coeff 0) ∈ p.roots

Tactic:
simp [roots_degree_eq_one h]

Premises used: Polynomial.roots_degree_eq_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
u : R[X]ˣ
n : ℕ
rw : (1 / if n = 0 then (↑u : R[X]).coeff 0 else 0) = if n = 0 then (↑u⁻¹ : R[X]).coeff 0 else 0
⊢ ((↑u : R[X]).coeff n)⁻¹ = (↑u⁻¹ : R[X]).coeff n

Tactic:
rw [eq_C_of_degree_eq_zero (degree_coe_units u), eq_C_of_degree_eq_zero (degree_coe_units u⁻¹),
    coeff_C, coeff_C, inv_eq_one_div]

Premises used: Polynomial.eq_C_of_degree_eq_zero, inv_eq_one_div, Polynomial.coeff_C, Inv.inv, Polynomial.degree_coe_units
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
u : R[X]ˣ
n : ℕ
pos : n = 0 → 1 / (↑u : R[X]).coeff 0 = (↑u⁻¹ : R[X]).coeff 0
neg : ¬n = 0 → 1 / 0 = 0
⊢ (1 / if n = 0 then (↑u : R[X]).coeff 0 else 0) = if n = 0 then (↑u⁻¹ : R[X]).coeff 0 else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
u : R[X]ˣ
n : ℕ
h : n = 0
pos : Eq.{u + 1} (α := R) (eval 0 (↑1 : R[X])) 1
⊢ 1 / (↑u : R[X]).coeff 0 = (↑u⁻¹ : R[X]).coeff 0

Tactic:
rw [div_eq_iff_mul_eq (coeff_coe_units_zero_ne_zero u), coeff_zero_eq_eval_zero,
        coeff_zero_eq_eval_zero, ← eval_mul, ← Units.val_mul, inv_mul_cancel]

Premises used: inv_mul_cancel, Polynomial.coeff_zero_eq_eval_zero, div_eq_iff_mul_eq, Polynomial.eval_mul, Polynomial.coeff_coe_units_zero_ne_zero, Units.val_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
u : R[X]ˣ
n : ℕ
h : n = 0
⊢ Eq.{u + 1} (α := R) (eval 0 (↑1 : R[X])) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
u : R[X]ˣ
n : ℕ
h : ¬n = 0
⊢ 1 / 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
inst_1 : DecidableEq R
hp0 : p ≠ 0
⊢ IsUnit p.leadingCoeff

Tactic:
rw [Ne, ← leadingCoeff_eq_zero, ← Ne, ← isUnit_iff_ne_zero] at hp0

Premises used: Ne, isUnit_iff_ne_zero, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
inst_1 : DecidableEq R
hp0 : IsUnit p.leadingCoeff
rw : IsUnit p.leadingCoeff
⊢ Monic.{u} (R := R) ((normalize : (a : R[X]) → R[X]) p)

Tactic:
rw [Monic, leadingCoeff_normalize, normalize_eq_one]

Premises used: Polynomial.leadingCoeff_normalize, Polynomial.Monic, normalize_eq_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
inst_1 : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ IsUnit p.leadingCoeff

Tactic:
apply hp0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
p : R[X]
hp : p ≠ 0
⊢ (normalize : (a : R[X]) → R[X]) p = p ↔ p.Monic

Tactic:
⟨fun h ↦ h ▸ monic_normalize hp, fun h ↦ Monic.normalize_eq_self h⟩

Premises used: Polynomial.Monic.normalize_eq_self, Eq.rec, Iff.intro, Polynomial.monic_normalize
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
pos : ∀ (hq : q = 0), (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
neg : ∀ (hq : ¬q = 0), (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : q = 0
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
simp [hq]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
rw : (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
rw [div_def, leadingCoeff_mul, leadingCoeff_C,
    leadingCoeff_divByMonic_of_monic (monic_mul_leadingCoeff_inv hq) _, mul_comm,
    div_eq_mul_inv]

Premises used: Polynomial.div_def, Polynomial.leadingCoeff_mul, div_eq_mul_inv, Polynomial.leadingCoeff_divByMonic_of_monic, Polynomial.monic_mul_leadingCoeff_inv, mul_comm, Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
rwa rwa₁ rwa₂ rwa₃ : q.degree ≤ p.degree
⊢ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree

Tactic:
rwa [degree_mul_leadingCoeff_inv q hq]

Premises used: Polynomial.degree_mul_leadingCoeff_inv
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
pos :
  ∀ (ha : a = 0),
    p / HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p / q)
neg :
  ∀ (ha : ¬a = 0),
    p / HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p / q)
⊢ p / HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p / q)

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : a = 0
⊢ p / HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p / q)

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : ¬a = 0
neg :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
        (p /ₘ
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
            (q *
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
                ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])))
⊢ p / HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p / q)

Tactic:
simp only [div_def, leadingCoeff_mul, mul_inv, leadingCoeff_C, C.map_mul, mul_assoc]

Premises used: Polynomial.C, Polynomial.div_def, Polynomial.leadingCoeff_mul, mul_inv, mul_assoc, Polynomial.leadingCoeff_C, RingHom.map_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : ¬a = 0
neg :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (q *
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
          ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
        (p /ₘ
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
            (q *
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
                ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])))

Tactic:
congr 3
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : ¬a = 0
neg :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
neg₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) *
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
neg₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X])
      (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
neg₃ :
  (C : (a : R) → R[X]) 1 * HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
neg₄ :
  1 * HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
neg₅ neg₆ :
  HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (q *
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
          ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])

Tactic:
rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one, one_mul]

Premises used: Polynomial.C, mul_inv_cancel₀, mul_assoc, RingHom.map_one, mul_left_comm, RingHom.map_mul, one_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a : R
inst : Field R
p : R[X]
⊢ HDiv.hDiv (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]) = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a⁻¹ : R[X])

Tactic:
simpa [mul_comm] using div_C_mul (q := 1)

Premises used: mul_comm, Polynomial.div_C_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a b : R
inst : Field R
rw :
  (C : (a : R) → R[X]) (a / b) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b⁻¹ : R[X])
rw₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (a / b) : R[X]) ((C : (a : R) → R[X]) (a * b⁻¹) : R[X])
rw₂ rw₃ : Eq (α := R[X]) ((C : (a : R) → R[X]) (a * b⁻¹) : R[X]) ((C : (a : R) → R[X]) (a * b⁻¹) : R[X])
⊢ (C : (a : R) → R[X]) (a / b) =
    HDiv.hDiv (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b : R[X])

Tactic:
rw [div_C, ← C_mul, div_eq_mul_inv]

Premises used: div_eq_mul_inv, Polynomial.div_C, Polynomial.C_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : a ≠ 0
h : p ∣ q
r : R[X]
hr : q = p * r
rw :
  q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r)
rw₁ :
  q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p * r))
rw₂ : q = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) * (p * r)
rw₃ : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X]) (p * r)
rw₄ : q = (C : (a : R) → R[X]) 1 * (p * r)
rw₅ : q = 1 * (p * r)
rw₆ : q = p * r
rw₇ rw₈ : p * r = p * r
⊢ q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r

Tactic:
rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
        one_mul, hr]

Premises used: Polynomial.C, mul_inv_cancel₀, mul_assoc, RingHom.map_one, mul_left_comm, RingHom.map_mul, one_mul