awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
hp : p.Monic
⊢ (HPow.hPow (α := R[X]) (-1) p.natDegree * p.comp (-X)).leadingCoeff =
    (HMul.hMul (β := R[X]) (p.comp (-X))
        ((C : (a : R) → R[X]) (HPow.hPow (α := R) (-1) p.natDegree) : R[X])).leadingCoeff

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
hp : p.Monic
hp₁ : (p.comp (-X)).leadingCoeff * HPow.hPow (α := R) (-1) p.natDegree = 1
⊢ (HMul.hMul (β := R[X]) (p.comp (-X))
        ((C : (a : R) → R[X]) (HPow.hPow (α := R) (-1) p.natDegree) : R[X])).leadingCoeff =
    1

Tactic:
apply monic_mul_C_of_leadingCoeff_mul_eq_one

Premises used: Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
hp : p.Monic
⊢ (p.comp (-X)).leadingCoeff * HPow.hPow (α := R) (-1) p.natDegree = 1

Tactic:
simp [← pow_add, hp]

Premises used: pow_add
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
hp : p.Monic
C :
  (HPow.hPow (α := R[X]) (-1) p.natDegree * p.comp (-X)).leadingCoeff =
    (HMul.hMul (β := R[X]) (p.comp (-X))
        ((Polynomial.C : (a : R) → R[X]) (HPow.hPow (α := R) (-1) p.natDegree) : R[X])).leadingCoeff
C₁ :
  (HMul.hMul (β := R[X]) (p.comp (-X))
        ((Polynomial.C : (a : R) → R[X]) (HPow.hPow (α := R) (-1) p.natDegree) : R[X])).leadingCoeff =
    1
⊢ (HPow.hPow (α := R[X]) (-1) p.natDegree * p.comp (-X)).leadingCoeff = 1

Tactic:
calc
    ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff =
        (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff := by
      simp [mul_comm]
    _ = 1 := by
      apply monic_mul_C_of_leadingCoeff_mul_eq_one
      simp [← pow_add, hp]

Premises used: HMul.hMul, Polynomial.leadingCoeff, HPow.hPow, Polynomial.natDegree, OfNat.ofNat, Polynomial.X, Polynomial.comp, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
h : Associated p q
let : ∀ (u : R[X]ˣ) (hu : p * (↑u : R[X]) = q), p.degree = q.degree
⊢ p.degree = q.degree

Tactic:
let ⟨u, hu⟩ := h
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
h : Associated p q
u : R[X]ˣ
hu : p * (↑u : R[X]) = q
⊢ p.degree = q.degree

Tactic:
simp [hu.symm]

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
x x_1 : R[X]
simp_rw : eval r x = 0 ∨ eval r x_1 = 0 → eval r x = 0 ∨ eval r x_1 = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ∣ x * x_1 →
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ∣ x ∨
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ∣ x_1

Tactic:
simp_rw [dvd_iff_isRoot, IsRoot.def, eval_mul, mul_eq_zero]

Premises used: Polynomial.IsRoot.def, Polynomial.eval_mul, mul_eq_zero, Polynomial.dvd_iff_isRoot
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
x x_1 : R[X]
⊢ eval r x = 0 ∨ eval r x_1 = 0 → eval r x = 0 ∨ eval r x_1 = 0

Tactic:
id

Premises used: id
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
x x_1 : R[X]
⊢ eval r x = 0 ∨ eval r x_1 = 0 → eval r x = 0 ∨ eval r x_1 = 0

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ Prime (HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0))

Tactic:
prime_X_sub_C (0 : R)

Premises used: Polynomial.prime_X_sub_C, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
h : X = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)
⊢ Prime.{u} (M := R[X]) X

Tactic:
convert! prime_X_sub_C (0 : R)

Premises used: Polynomial.prime_X_sub_C, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ X = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp1 : p.degree = 1
hm : p.Monic
⊢ p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-p.coeff 0) : R[X])

Tactic:
simpa [hm.leadingCoeff] using eq_X_add_C_of_degree_eq_one hp1

Premises used: Polynomial.eq_X_add_C_of_degree_eq_one, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
r : R
⊢ Irreducible (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))

Tactic:
(prime_X_sub_C r).irreducible

Premises used: Prime.irreducible, Polynomial.prime_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ Irreducible.{u} (M := R[X]) X

Tactic:
Prime.irreducible prime_X

Premises used: Prime.irreducible, Polynomial.prime_X
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp1 : p.degree = 1
hm : p.Monic
⊢ Irreducible p

Tactic:
(hm.prime_of_degree_eq_one hp1).irreducible

Premises used: Prime.irreducible, Polynomial.Monic.prime_of_degree_eq_one
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
h : IsUnit p
obtain : ∀ (u : R) (h : (C : (a : R) → R[X]) u = p), False
⊢ False

Tactic:
obtain ⟨u, -, h⟩ := isUnit_iff.mp h

Premises used: Polynomial.isUnit_iff, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
h_1 : IsUnit p
u : R
h : (C : (a : R) → R[X]) u = p
apply : LE.le (α := WithBot ℕ) 1 0
⊢ False

Tactic:
apply not_le.mpr (zero_lt_one' (WithBot ℕ))

Premises used: not_le, Iff.mpr, WithBot, zero_lt_one', Nat
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
h_1 : IsUnit p
u : R
h : (C : (a : R) → R[X]) u = p
⊢ LE.le (α := WithBot ℕ) 1 0

Tactic:
simp [← hp, ← h, degree_C_le]

Premises used: Polynomial.degree_C_le
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
inr :
  ∀ (this : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g) (H : g.degree < f.degree),
    IsUnit f ∨ IsUnit g
wlog! : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g
⊢ IsUnit f ∨ IsUnit g

Tactic:
wlog! H : f.degree ≤ g.degree generalizing f g

Premises used: Polynomial.degree
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
this : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g
H : g.degree < f.degree
⊢ p = g * f

Tactic:
rw [mul_comm] at h

Premises used: mul_comm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
this : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g
H : g.degree < f.degree
h₁ : p = g * f
⊢ ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g

Tactic:
rw [mul_comm] at h

Premises used: mul_comm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
this : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g
H : g.degree < f.degree
h₁ : p = g * f
this₁ : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g
⊢ g.degree < f.degree

Tactic:
rw [mul_comm] at h

Premises used: mul_comm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = g * f
this : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g
H : g.degree < f.degree
⊢ IsUnit f ∨ IsUnit g

Tactic:
(this g f h H.le).symm

Premises used: LT.lt.le, Or.symm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = g * f
this : ∀ (f g : R[X]) (h : p = f * g) (H : f.degree ≤ g.degree), IsUnit f ∨ IsUnit g
H : g.degree < f.degree
⊢ IsUnit f ∨ IsUnit g

Tactic:
exact (this g f h H.le).symm

Premises used: LT.lt.le, Or.symm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
h₁ : IsUnit f
⊢ IsUnit f ∨ IsUnit g

Tactic:
left
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
⊢ f.degree = 0 ∧ g.degree = 1 ∨ f.degree = 1 ∧ g.degree = 0

Tactic:
rw [h, degree_mul, Nat.WithBot.add_eq_one_iff] at hp

Premises used: Nat.WithBot.add_eq_one_iff, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hp₁ : f.degree = 0 ∧ g.degree = 1 ∨ f.degree = 1 ∧ g.degree = 0
⊢ p = f * g

Tactic:
rw [h, degree_mul, Nat.WithBot.add_eq_one_iff] at hp

Premises used: Nat.WithBot.add_eq_one_iff, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hp₁ : f.degree = 0 ∧ g.degree = 1 ∨ f.degree = 1 ∧ g.degree = 0
h₁ : p = f * g
⊢ f.degree ≤ g.degree

Tactic:
rw [h, degree_mul, Nat.WithBot.add_eq_one_iff] at hp

Premises used: Nat.WithBot.add_eq_one_iff, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
hp : f.degree = 0 ∧ g.degree = 1 ∨ f.degree = 1 ∧ g.degree = 0
h : p = f * g
H : f.degree ≤ g.degree
h₁ : ∀ (hf : f.degree = 0) (hg : g.degree = 1), IsUnit f
h₂ : ∀ (hf : f.degree = 1) (hg : g.degree = 0), IsUnit f
⊢ IsUnit f

Tactic:
rcases hp with ⟨hf, hg⟩ | ⟨hf, hg⟩
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 1
hg : g.degree = 0
⊢ IsUnit f

Tactic:
simp [← not_lt, hf, hg] at H

Premises used: not_lt
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 0
hg : g.degree = 1
⊢ f = (C : (a : R) → R[X]) (f.coeff 0)

Tactic:
replace hf := f.eq_C_of_degree_eq_zero hf
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
h₁ : IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
⊢ IsUnit f

Tactic:
rw [hf]
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
h₁ : IsUnit (f.coeff 0)
⊢ IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])

Tactic:
apply IsUnit.map C

Premises used: Polynomial.C, IsUnit.map
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
⊢ IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)

Tactic:
rw [h, hf, coeff_C_mul, coeff_C_mul] at hc

Premises used: Polynomial.coeff_C_mul
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
hc₁ : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
⊢ p = f * g

Tactic:
rw [h, hf, coeff_C_mul, coeff_C_mul] at hc

Premises used: Polynomial.coeff_C_mul
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
hc₁ : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h₁ : p = f * g
⊢ f.degree ≤ g.degree

Tactic:
rw [h, hf, coeff_C_mul, coeff_C_mul] at hc

Premises used: Polynomial.coeff_C_mul
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
hc₁ : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h₁ : p = f * g
H₁ : f.degree ≤ g.degree
⊢ g.degree = 1

Tactic:
rw [h, hf, coeff_C_mul, coeff_C_mul] at hc

Premises used: Polynomial.coeff_C_mul
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
hc₁ : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h₁ : p = f * g
H₁ : f.degree ≤ g.degree
hg₁ : g.degree = 1
⊢ f = (C : (a : R) → R[X]) (f.coeff 0)

Tactic:
rw [h, hf, coeff_C_mul, coeff_C_mul] at hc

Premises used: Polynomial.coeff_C_mul
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
h₁ : f.coeff 0 ∣ f.coeff 0 * g.coeff 0
h₂ : f.coeff 0 ∣ f.coeff 0 * g.coeff 1
⊢ IsUnit (f.coeff 0)

Tactic:
apply hc
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
⊢ f.coeff 0 ∣ f.coeff 0 * g.coeff 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = (C : (a : R) → R[X]) (f.coeff 0)
⊢ f.coeff 0 ∣ f.coeff 0 * g.coeff 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
hp :
  (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])).degree =
    1
hc :
  IsRelPrime
    ((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])).coeff
      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])).coeff
      1)
⊢ Irreducible
    (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]))

Tactic:
apply irreducible_of_degree_eq_one_of_isRelPrime_coeff

Premises used: Polynomial.irreducible_of_degree_eq_one_of_isRelPrime_coeff
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
hp :
  ((if WithBot.unbotD 0 1 = HAdd.hAdd (α := ℕ) 0 1 then
        (if Eq (α := ℕ) 0 0 then a else 0) * if Eq (α := ℕ) 1 1 then 1 else 0
      else 0) +
      if Eq (α := ℕ) (WithBot.unbotD 0 1) 0 then b else 0) ≠
    0
hp₁ : HAdd.hAdd (α := ℕ) 0 1 ≤ WithBot.unbotD 0 1
hp₂ : a ≠ 0
hp₃ : LE.le (α := ℕ) 1 (WithBot.unbotD 0 1)
⊢ (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])).degree =
    1

Tactic:
compute_degree!
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ IsRelPrime
    ((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])).coeff
      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])).coeff
      1)

Tactic:
simpa using hab.symm

Premises used: IsRelPrime.symm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
S : Type v
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial S
inst_2 : Semiring S
inst_3 : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
by_contra! :
  ∀ (hp : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S))
    (hq : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)), False
⊢ Ne.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S) ∨
    Ne.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)

Tactic:
by_contra! ⟨hp, hq⟩
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
S : Type v
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial S
inst_2 : Semiring S
inst_3 : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
hp : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
hq : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
rcases : ∀ (w w_1 : R[X]) (h : w * p + w_1 * q = 1), False
⊢ False

Tactic:
rcases h with ⟨_, _, h⟩
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
S : Type v
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial S
inst_2 : Semiring S
inst_3 : Algebra R S
p q : R[X]
s : S
hp : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
hq : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
w w_1 : R[X]
h : w * p + w_1 * q = 1
⊢ Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) (w * p + w_1 * q) : S) ((aeval s : (a : R[X]) → S) 1 : S)

Tactic:
apply_fun aeval s at h

Premises used: Polynomial.aeval
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
S : Type v
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial S
inst_2 : Semiring S
inst_3 : Algebra R S
p q : R[X]
s : S
hp : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
hq : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
w w_1 : R[X]
h : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) (w * p + w_1 * q) : S) ((aeval s : (a : R[X]) → S) 1 : S)
⊢ False

Tactic:
simp only [map_add, map_mul, map_one, hp, hq, mul_zero, add_zero, zero_ne_one] at h

Premises used: zero_ne_one, map_add, MulZeroClass.mul_zero, map_mul, map_one, add_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u_1
inst : CommRing R
a b : R
h : IsUnit (a - b)
rw : Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑h.unit⁻¹ : R) * (a - b)) : R[X]) (1 : R[X])
⊢ HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑h.unit⁻¹ : R) : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])) =
    1

Tactic:
rw [neg_mul_comm, ← left_distrib, neg_add_eq_sub, sub_sub_sub_cancel_left, ← C_sub, ← C_mul]

Premises used: neg_add_eq_sub, Polynomial.C_sub, Polynomial.C_mul, neg_mul_comm, sub_sub_sub_cancel_left, left_distrib
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u_1
inst : CommRing R
a b : R
h : IsUnit (a - b)
h₁ : (↑h.unit⁻¹ : R) * (a - b) = 1
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑h.unit⁻¹ : R) * (a - b)) : R[X]) ((C : (a : R) → R[X]) 1 : R[X])

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u_1
inst : CommRing R
a b : R
h : IsUnit (a - b)
⊢ (↑h.unit⁻¹ : R) * (a - b) = 1

Tactic:
h.val_inv_mul

Premises used: IsUnit.val_inv_mul
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u_1
inst : CommRing R
a b : R
h : IsUnit (a - b)
⊢ (↑h.unit⁻¹ : R) * (a - b) = 1

Tactic:
exact h.val_inv_mul

Premises used: IsUnit.val_inv_mul
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
K : Type u_1
inst : Field K
I : Type v
s : I → K
H : Function.Injective s
⊢ Pairwise.{v} (α := I)
    (Function.onFun.{v + 1, u_1 + 1, 1} (β := K[X]) IsCoprime fun (i : I) ↦
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) (s i) : K[X]))

Tactic:
fun _ _ hij =>
  isCoprime_X_sub_C_of_isUnit_sub (sub_ne_zero_of_ne <| H.ne hij).isUnit

Premises used: Ne.isUnit, Function.Injective.ne, sub_ne_zero_of_ne, Pairwise, Polynomial.isCoprime_X_sub_C_of_isUnit_sub
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ p ≠ 0

Tactic:
have hp : p ≠ 0 := left_ne_zero_of_mul hpq
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
⊢ q ≠ 0

Tactic:
have hq : q ≠ 0 := right_ne_zero_of_mul hpq