awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
this : MulPosStrictMono R
hc : 0 < c
⊢ a * c < b * d

Tactic:
mul_lt_mul_of_pos' hab hcd hc hab.pos

Premises used: LT.lt.pos, mul_lt_mul_of_pos'
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
this : MulPosStrictMono R
hc : 0 < c
⊢ a * c < b * d

Tactic:
exact mul_lt_mul_of_pos' hab hcd hc hab.pos

Premises used: LT.lt.pos, mul_lt_mul_of_pos'
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
inl : ∀ (hbc : b ≤ c), a * (b - c) = a * b - a * c
inr : ∀ (hcb : c ≤ b), a * (b - c) = a * b - a * c
⊢ a * (b - c) = a * b - a * c

Tactic:
obtain (hbc | hcb) := total_of (· ≤ ·) b c

Premises used: LE.le, total_of
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hbc : b ≤ c
inl : a * 0 = a * b - a * c
inl₁ : 0 = a * b - a * c
inl₂ inl₃ : Eq.{u + 1} (α := R) 0 0
⊢ a * (b - c) = a * b - a * c

Tactic:
rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_right hbc a)]

Premises used: Iff.mpr, mul_le_mul_right, tsub_eq_zero_iff_le, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
inr : a * (b - c) + a * c = a * b
⊢ a * (b - c) = a * b - a * c

Tactic:
apply h.eq_tsub_of_add_eq

Premises used: AddLECancellable.eq_tsub_of_add_eq
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hcb : c ≤ b
inr : a * (b - c + c) = a * b
inr₁ inr₂ : a * b = a * b
⊢ a * (b - c) + a * c = a * b

Tactic:
rw [← mul_add, tsub_add_cancel_of_le hcb]

Premises used: tsub_add_cancel_of_le, mul_add
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
inl : ∀ (hab : a ≤ b), (a - b) * c = a * c - b * c
inr : ∀ (hba : b ≤ a), (a - b) * c = a * c - b * c
⊢ (a - b) * c = a * c - b * c

Tactic:
obtain (hab | hba) := total_of (· ≤ ·) a b

Premises used: LE.le, total_of
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
inl : 0 * c = a * c - b * c
inl₁ : 0 = a * c - b * c
inl₂ inl₃ : Eq.{u + 1} (α := R) 0 0
⊢ (a - b) * c = a * c - b * c

Tactic:
rw [tsub_eq_zero_iff_le.2 hab, zero_mul, tsub_eq_zero_iff_le.2 (mul_le_mul_left hab c)]

Premises used: Iff.mpr, MulZeroClass.zero_mul, tsub_eq_zero_iff_le, mul_le_mul_left
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
inr : (a - b) * c + b * c = a * c
⊢ (a - b) * c = a * c - b * c

Tactic:
apply h.eq_tsub_of_add_eq

Premises used: AddLECancellable.eq_tsub_of_add_eq
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
inr : (a - b + b) * c = a * c
inr₁ inr₂ : a * c = a * c
⊢ (a - b) * c + b * c = a * c

Tactic:
rw [← add_mul, tsub_add_cancel_of_le hba]

Premises used: add_mul, tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b c : R
⊢ a * (b - c) = a * b - a * c

Tactic:
Contravariant.AddLECancellable.mul_tsub

Premises used: AddLECancellable.mul_tsub, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
inst_7 : MulRightMono R
a b c : R
⊢ (a - b) * c = a * c - b * c

Tactic:
Contravariant.AddLECancellable.tsub_mul

Premises used: AddLECancellable.tsub_mul, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
rw : a * b - a * 1 = a * b - a
rw₁ rw₂ : a * b - a = a * b - a
⊢ a * (b - 1) = a * b - a

Tactic:
rw [mul_tsub, mul_one]

Premises used: mul_one, mul_tsub
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : NonAssocSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : MulRightMono R
inst_7 : AddLeftReflectLE R
a b : R
rw : a * b - 1 * b = a * b - b
rw₁ rw₂ : a * b - b = a * b - b
⊢ (a - 1) * b = a * b - b

Tactic:
rw [tsub_mul, one_mul]

Premises used: tsub_mul, one_mul
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
rw : a * a - b * b = (a + b) * a - (a + b) * b
rw₁ : a * a - b * b = a * a + b * a - (a + b) * b
rw₂ : a * a - b * b = a * a + b * a - (a * b + b * b)
rw₃ : a * a - b * b = a * a + b * a - a * b - b * b
rw₄ : a * a - b * b = a * a + a * b - a * b - b * b
rw₅ rw₆ : a * a - b * b = a * a - b * b
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]

Premises used: add_mul, mul_comm, tsub_add_eq_tsub_tsub, add_tsub_cancel_right, mul_tsub
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a b : R
rw : a * a - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
rw₁ : a * a - b * b = (a + b) * (a - b)
rw₂ rw₃ : (a + b) * (a - b) = (a + b) * (a - b)
⊢ HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)

Tactic:
rw [sq, sq, mul_self_tsub_mul_self]

Premises used: mul_self_tsub_mul_self, sq
-- Module: Mathlib.Algebra.Order.Ring.Canonical
Goal:
R : Type u
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : Sub R
inst_4 : OrderedSub R
inst_5 : Std.Total fun (x1 x2 : R) ↦ x1 ≤ x2
inst_6 : AddLeftReflectLE R
a : R
rw : a * a - 1 = a * a - HMul.hMul (α := R) 1 1
rw₁ rw₂ : a * a - 1 = a * a - 1
⊢ a * a - 1 = (a + 1) * (a - 1)

Tactic:
rw [← mul_self_tsub_mul_self, mul_one]

Premises used: mul_self_tsub_mul_self, mul_one
-- Module: Mathlib.Algebra.Polynomial.Eval.Algebra
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p q : R[X]
⊢ eval₂ (algebraMap R S) x (p * q) = eval₂ (algebraMap R S) x p * eval₂ (algebraMap R S) x q

Tactic:
eval₂_mul_noncomm _ _ fun k => Algebra.commute_algebraMap_left (coeff q k) x

Premises used: Polynomial.coeff, Algebra.commute_algebraMap_left, Polynomial.eval₂_mul_noncomm
-- Module: Mathlib.Algebra.Polynomial.Eval.Algebra
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p q : R[X]
⊢ eval₂ (algebraMap R S) x (p * q) = eval₂ (algebraMap R S) x p * eval₂ (algebraMap R S) x q

Tactic:
exact eval₂_mul_noncomm _ _ fun k => Algebra.commute_algebraMap_left (coeff q k) x

Premises used: Polynomial.coeff, Algebra.commute_algebraMap_left, Polynomial.eval₂_mul_noncomm
-- Module: Mathlib.Algebra.Polynomial.Eval.Algebra
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
⊢ eval₂ (algebraMap R S) x (HPow.hPow (β := ℕ) p 0) = HPow.hPow (β := ℕ) (eval₂ (algebraMap R S) x p) 0

Tactic:
simp only [pow_zero, eval₂_one]

Premises used: Polynomial.eval₂_one, pow_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Algebra
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
n : ℕ
ih : eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n
succ : eval₂ (algebraMap R S) x (p ^ n * p) = eval₂ (algebraMap R S) x p ^ (n + 1)
succ₁ : eval₂ (algebraMap R S) x (p ^ n * p) = eval₂ (algebraMap R S) x p ^ n * eval₂ (algebraMap R S) x p
succ₂ :
  eval₂ (algebraMap R S) x (p ^ n) * eval₂ (algebraMap R S) x p =
    eval₂ (algebraMap R S) x p ^ n * eval₂ (algebraMap R S) x p
succ₃ succ₄ :
  eval₂ (algebraMap R S) x p ^ n * eval₂ (algebraMap R S) x p =
    eval₂ (algebraMap R S) x p ^ n * eval₂ (algebraMap R S) x p
⊢ eval₂ (algebraMap R S) x (p ^ (n + 1)) = eval₂ (algebraMap R S) x p ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ, eval₂_mul', ih]

Premises used: pow_succ, Polynomial.eval₂_mul'
-- Module: Mathlib.Algebra.Polynomial.Eval.Algebra
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
n : ℕ
zero : eval₂ (algebraMap R S) x (HPow.hPow (β := ℕ) p 0) = HPow.hPow (β := ℕ) (eval₂ (algebraMap R S) x p) 0
succ :
  ∀ (n : ℕ) (ih : eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n),
    eval₂ (algebraMap R S) x (p ^ (n + 1)) = eval₂ (algebraMap R S) x p ^ (n + 1)
⊢ eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n

Tactic:
induction n with
  | zero => simp only [pow_zero, eval₂_one]
  | succ n ih => rw [pow_succ, pow_succ, eval₂_mul', ih]

Premises used: Polynomial.eval₂_one, pow_succ, Polynomial.eval₂_mul', pow_zero, AddMonoidAlgebra.zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Algebra
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p q r s : R[X]
hr : eval₂ (algebraMap R S) x (r.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) r
hs : eval₂ (algebraMap R S) x (s.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) s
⊢ eval₂ (algebraMap R S) x ((r + s).comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) (r + s)

Tactic:
simp only [add_comp, eval₂_add, hr, hs]

Premises used: Polynomial.add_comp, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Algebra
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p q : R[X]
n : ℕ
a : R
⊢ eval₂ (algebraMap R S) x (comp ((monomial n : (a : R) → R[X]) a) q) =
    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) ((monomial n : (a : R) → R[X]) a)

Tactic:
simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']

Premises used: Polynomial.eval₂_monomial, Polynomial.eval₂_mul', Polynomial.eval₂_C, Polynomial.eval₂_pow', Polynomial.monomial_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Algebra
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p q : R[X]
add :
  ∀ (r s : R[X]) (hr : eval₂ (algebraMap R S) x (r.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) r)
    (hs : eval₂ (algebraMap R S) x (s.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) s),
    eval₂ (algebraMap R S) x ((r + s).comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) (r + s)
monomial :
  ∀ (n : ℕ) (a : R),
    eval₂ (algebraMap R S) x (comp ((Polynomial.monomial n : (a : R) → R[X]) a) q) =
      eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) ((Polynomial.monomial n : (a : R) → R[X]) a)
⊢ eval₂ (algebraMap R S) x (p.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p

Tactic:
induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [add_comp, eval₂_add, hr, hs]
  | monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']

Premises used: Polynomial.eval₂_monomial, Polynomial.eval₂_mul', Polynomial.monomial, Polynomial.add_comp, Polynomial.eval₂_C, Polynomial.eval₂_pow', Polynomial.monomial_comp, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.Monic
h_irr : Irreducible (map φ f)
⊢ Irreducible f

Tactic:
⟨h_irr.not_isUnit ∘ IsUnit.map (mapRingHom φ), fun a b h => ?_⟩

Premises used: Irreducible.not_isUnit, Function.comp, Irreducible.mk, Polynomial.mapRingHom, IsUnit.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.Monic
h_irr : Irreducible (map φ f)
refine : ∀ (a b : R[X]) (h : f = a * b), IsUnit a ∨ IsUnit b
⊢ Irreducible f

Tactic:
refine ⟨h_irr.not_isUnit ∘ IsUnit.map (mapRingHom φ), fun a b h => ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ a.leadingCoeff * b.leadingCoeff = (a * b).leadingCoeff

Tactic:
have q := (leadingCoeff_mul a b).symm
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = (a * b).leadingCoeff
⊢ a.leadingCoeff * b.leadingCoeff = 1

Tactic:
rw [← h, h_mon] at q
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
(h_irr.isUnit_or_isUnit <|
    (congr_arg (Polynomial.map φ) h).trans (Polynomial.map_mul φ)).imp ?_ ?_

Premises used: Polynomial.map_mul, congr_arg, Irreducible.isUnit_or_isUnit, Polynomial.map, Or.imp, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
refine_1 : IsUnit (map φ a) → IsUnit a
refine_2 : IsUnit (map φ b) → IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
refine (h_irr.isUnit_or_isUnit <|
    (congr_arg (Polynomial.map φ) h).trans (Polynomial.map_mul φ)).imp ?_ ?_

Premises used: Polynomial.map_mul, congr_arg, Irreducible.isUnit_or_isUnit, Polynomial.map, Or.imp, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
refine_1 : IsUnit a.leadingCoeff
⊢ IsUnit (map φ a) → IsUnit a

Tactic:
apply isUnit_of_isUnit_leadingCoeff_of_isUnit_map

Premises used: Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
refine_2 : IsUnit b.leadingCoeff
⊢ IsUnit (map φ b) → IsUnit b

Tactic:
apply isUnit_of_isUnit_leadingCoeff_of_isUnit_map

Premises used: Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
refine_1 : a.leadingCoeff * b.leadingCoeff = 1
refine_1₁ : R
⊢ IsUnit a.leadingCoeff

Tactic:
apply IsUnit.of_mul_eq_one

Premises used: IsUnit.of_mul_eq_one
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
refine_2 : b.leadingCoeff * a.leadingCoeff = 1
refine_2₁ : R
⊢ IsUnit b.leadingCoeff

Tactic:
apply IsUnit.of_mul_eq_one

Premises used: IsUnit.of_mul_eq_one
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ a.leadingCoeff * b.leadingCoeff = 1

Tactic:
q
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ a.leadingCoeff * b.leadingCoeff = 1

Tactic:
exact q
-- Module: Mathlib.Algebra.Polynomial.Eval.Irreducible
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CommRing S
inst_3 : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
refine_2 : a.leadingCoeff * b.leadingCoeff = 1
refine_2₁ : R
⊢ b.leadingCoeff * a.leadingCoeff = 1

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Semiring S
inst_2 : Algebra R S
p : R[X]
hp : p ≠ 0
z : S
hz : Eq.{v + 1} (α := S) ((aeval z : (a : R[X]) → S) p : S) (0 : S)
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S) → x = 0
⊢ 0 < p.natDegree

Tactic:
natDegree_pos_of_eval₂_root hp (algebraMap R S) hz inj

Premises used: Algebra.algebraMap, Polynomial.natDegree_pos_of_eval₂_root
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Semiring S
inst_2 : Algebra R S
p : R[X]
hp : p ≠ 0
z : S
hz : Eq.{v + 1} (α := S) ((aeval z : (a : R[X]) → S) p : S) (0 : S)
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S) → x = 0
⊢ 0 < p.degree

Tactic:
natDegree_pos_iff_degree_pos.mp (natDegree_pos_of_aeval_root hp hz inj)

Premises used: Iff.mp, Polynomial.natDegree_pos_iff_degree_pos, Polynomial.natDegree_pos_of_aeval_root
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
pos : ∀ (hq : q.Monic), c • p %ₘ q = c • (p %ₘ q)
neg : ∀ (hq : ¬q.Monic), c • p %ₘ q = c • (p %ₘ q)
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
by_cases hq : q.Monic

Premises used: Polynomial.Monic
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
pos : ∀ (hR : Subsingleton R), c • p %ₘ q = c • (p %ₘ q)
pos₁ : ∀ (hR : Nontrivial R), c • p %ₘ q = c • (p %ₘ q)
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Subsingleton R
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
rw : c • (p %ₘ q) + c • (q * (p /ₘ q)) = c • p
rw₁ : c • (p %ₘ q + q * (p /ₘ q)) = c • p
rw₂ rw₃ : c • p = c • p
⊢ c • (p %ₘ q) + q * c • (p /ₘ q) = c • p

Tactic:
rw [mul_smul_comm, ← smul_add, modByMonic_add_div]

Premises used: Polynomial.modByMonic_add_div, mul_smul_comm, smul_add
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
exact
      (div_modByMonic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
          ⟨by rw [mul_smul_comm, ← smul_add, modByMonic_add_div],
            (degree_smul_le _ _).trans_lt (degree_modByMonic_lt _ hq)⟩).2

Premises used: Polynomial.divByMonic, Polynomial.div_modByMonic_unique, And.right, Polynomial.degree_smul_le, Polynomial.modByMonic, And.intro, Polynomial.degree_modByMonic_lt, HSMul.hSMul, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
q : R[X]
c : R
p : R[X]
hq : ¬q.Monic
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
simp_rw [modByMonic_eq_of_not_monic _ hq]

Premises used: Polynomial.modByMonic_eq_of_not_monic
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
q : R[X]
hq : q.Monic
p : R[X]
⊢ p ∈ q.modByMonicHom.ker ↔ q ∣ p

Tactic:
LinearMap.mem_ker.trans (modByMonic_eq_zero_iff_dvd hq)

Premises used: Polynomial.modByMonic_eq_zero_iff_dvd, LinearMap.mem_ker, Iff.trans
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : R[X]
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
rw : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p - q * (p /ₘ q)) : S) ((aeval x : (a : R[X]) → S) p : S)
rw₁ :
  HSub.hSub (α := S) (β := S) ((aeval x : (a : R[X]) → S) p : S) ((aeval x : (a : R[X]) → S) (q * (p /ₘ q)) : S) =
    (aeval x : (a : R[X]) → S) p
rw₂ :
  HSub.hSub (α := S) ((aeval x : (a : R[X]) → S) p : S)
      (HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) q : S) ((aeval x : (a : R[X]) → S) (p /ₘ q) : S)) =
    (aeval x : (a : R[X]) → S) p
rw₃ :
  HSub.hSub (α := S) ((aeval x : (a : R[X]) → S) p : S)
      (HMul.hMul (α := S) (β := S) (0 : S) ((aeval x : (a : R[X]) → S) (p /ₘ q) : S)) =
    (aeval x : (a : R[X]) → S) p
rw₄ : HSub.hSub (α := S) (β := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S) = (aeval x : (a : R[X]) → S) p
rw₅ rw₆ : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) ((aeval x : (a : R[X]) → S) p : S)
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) (p %ₘ q) : S) ((aeval x : (a : R[X]) → S) p : S)

Tactic:
rw [modByMonic_eq_sub_mul_div, map_sub, map_mul, hx, zero_mul, sub_zero]

Premises used: map_sub, sub_zero, MulZeroClass.zero_mul, Polynomial.modByMonic_eq_sub_mul_div, map_mul