awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
h : DenomsClearable a b N f i
h_1 : DenomsClearable a b N g i
Df : R
bf : K
bfu : HMul.hMul (β := K) bf ((i : (a : R) → K) b : K) = 1
Hf :
  (i : (a : R) → K) Df =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : HMul.hMul (β := K) bg ((i : (a : R) → K) b : K) = 1
Hg :
  (i : (a : R) → K) Dg =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bg) (Polynomial.map i g)
⊢ bg = bf

Tactic:
@inv_unique K _ (i b) bg bf ?_ ?_

Premises used: inv_unique
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
h : DenomsClearable a b N f i
h_1 : DenomsClearable a b N g i
Df : R
bf : K
bfu : HMul.hMul (β := K) bf ((i : (a : R) → K) b : K) = 1
Hf :
  (i : (a : R) → K) Df =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : HMul.hMul (β := K) bg ((i : (a : R) → K) b : K) = 1
Hg :
  (i : (a : R) → K) Dg =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bg) (Polynomial.map i g)
e_a : HMul.hMul (α := K) ((i : (a : R) → K) b : K) bg = 1
e_a₁ : HMul.hMul (α := K) ((i : (a : R) → K) b : K) bf = 1
⊢ bg = bf

Tactic:
refine @inv_unique K _ (i b) bg bf ?_ ?_

Premises used: inv_unique
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
h : DenomsClearable a b N f i
h_1 : DenomsClearable a b N g i
Df : R
bf : K
bfu : HMul.hMul (β := K) bf ((i : (a : R) → K) b : K) = 1
Hf :
  (i : (a : R) → K) Df =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : HMul.hMul (β := K) bg ((i : (a : R) → K) b : K) = 1
Hg :
  (i : (a : R) → K) Dg =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bg) (Polynomial.map i g)
e_a e_a₁ e_a₂ e_a₃ : HMul.hMul (β := K) bg ((i : (a : R) → K) b : K) = 1
⊢ HMul.hMul (α := K) ((i : (a : R) → K) b : K) bg = 1

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
h : DenomsClearable a b N f i
h_1 : DenomsClearable a b N g i
Df : R
bf : K
bfu : HMul.hMul (β := K) bf ((i : (a : R) → K) b : K) = 1
Hf :
  (i : (a : R) → K) Df =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : HMul.hMul (β := K) bg ((i : (a : R) → K) b : K) = 1
Hg :
  (i : (a : R) → K) Dg =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bg) (Polynomial.map i g)
e_a e_a₁ e_a₂ e_a₃ : HMul.hMul (β := K) bf ((i : (a : R) → K) b : K) = 1
⊢ HMul.hMul (α := K) ((i : (a : R) → K) b : K) bf = 1

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : HMul.hMul (β := K) bi ((i : (a : R) → K) b : K) = 1
⊢ ∀ (f : R[X]), f.natDegree ≤ N → DenomsClearable a b N f i

Tactic:
induction_with_natDegree_le _ N (denomsClearable_zero N a bu)
    (fun _ r _ => denomsClearable_C_mul_X_pow a bu r) fun _ _ _ _ df dg => df.add dg

Premises used: denomsClearable_zero, Polynomial.induction_with_natDegree_le, denomsClearable_C_mul_X_pow, DenomsClearable.add
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
R : Type u_1
K : Type u_2
inst : Semiring R
inst_1 : CommSemiring K
b : R
bi : K
i : R →+* K
f : R[X]
a : R
bu : HMul.hMul (β := K) bi ((i : (a : R) → K) b : K) = 1
⊢ DenomsClearable a b f.natDegree f i

Tactic:
denomsClearable_of_natDegree_le f.natDegree a bu f le_rfl

Premises used: le_rfl, denomsClearable_of_natDegree_le, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
rw : Ne.{u_1 + 1} (α := K) (↑b : K) 0
⊢ HMul.hMul (β := K) (HDiv.hDiv (α := K) 1 (↑b : K)) ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1

Tactic:
rw [eq_intCast, one_div_mul_cancel]

Premises used: eq_intCast, one_div_mul_cancel
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
rw : b ≠ 0
⊢ Ne.{u_1 + 1} (α := K) (↑b : K) 0

Tactic:
rw [Int.cast_ne_zero]

Premises used: Int.cast_ne_zero
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ b ≠ 0

Tactic:
b0.ne.symm

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ b ≠ 0

Tactic:
exact b0.ne.symm

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
obtain :
  ∀ (ev : ℤ) (bi : K) (bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1)
    (hF :
      (algebraMap ℤ K : (a : ℤ) → K) ev =
        HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
          eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)),
    1 ≤
      HPow.hPow (α := K) (↑b : K) f.natDegree *
        |eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
obtain ⟨ev, bi, bu, hF⟩ :=
    denomsClearable_natDegree (b := b) (algebraMap ℤ K) f a
      (by
        rw [eq_intCast, one_div_mul_cancel]
        rw [Int.cast_ne_zero]
        exact b0.ne.symm)

Premises used: Algebra.algebraMap, denomsClearable_natDegree, Int
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
hF :
  (algebraMap ℤ K : (a : ℤ) → K) ev =
    HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
      eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)
⊢ |(algebraMap ℤ K : (a : ℤ) → K) ev| =
    |HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
        eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
obtain Fa := congr_arg abs hF

Premises used: abs, congr_arg
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
hF :
  (algebraMap ℤ K : (a : ℤ) → K) ev =
    HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
      eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |(algebraMap ℤ K : (a : ℤ) → K) ev| =
    |HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
        eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)|
⊢ |(↑ev : K)| =
    |HPow.hPow (α := K) (↑b : K) f.natDegree| *
      |eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) (HDiv.hDiv (α := K) 1 (↑b : K)))
          (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
rw [eq_one_div_of_mul_eq_one_left bu, eq_intCast, eq_intCast, abs_mul] at Fa

Premises used: abs_mul, eq_intCast, eq_one_div_of_mul_eq_one_left
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
hF :
  (algebraMap ℤ K : (a : ℤ) → K) ev =
    HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
      eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |(↑ev : K)| =
    |HPow.hPow (α := K) (↑b : K) f.natDegree| *
      |eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) (HDiv.hDiv (α := K) 1 (↑b : K)))
          (Polynomial.map (algebraMap ℤ K) f)|
⊢ |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
rw [abs_of_pos (pow_pos (Int.cast_pos.mpr b0) _ : 0 < (b : K) ^ _), one_div, eq_intCast] at Fa

Premises used: pow_pos, eq_intCast, one_div, abs_of_pos
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
hF :
  (algebraMap ℤ K : (a : ℤ) → K) ev =
    HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
      eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
rw : 1 ≤ |ev|
⊢ 1 ≤
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
rw [div_eq_mul_inv, ← Fa, ← Int.cast_abs, ← Int.cast_one, Int.cast_le]

Premises used: Int.cast_abs, Int.cast_le, div_eq_mul_inv, Int.cast_one
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
hF :
  (algebraMap ℤ K : (a : ℤ) → K) ev =
    HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
      eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ |ev|

Tactic:
Int.le_of_lt_add_one ((lt_add_iff_pos_left 1).mpr (abs_pos.mpr fun F0 => fab ?_))

Premises used: Iff.mpr, Int.le_of_lt_add_one, abs_pos, OfNat.ofNat, lt_add_iff_pos_left
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
hF :
  (algebraMap ℤ K : (a : ℤ) → K) ev =
    HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
      eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
refine : ∀ (F0 : ev = 0), eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0
⊢ 1 ≤ |ev|

Tactic:
refine Int.le_of_lt_add_one ((lt_add_iff_pos_left 1).mpr (abs_pos.mpr fun F0 => fab ?_))

Premises used: Iff.mpr, Int.le_of_lt_add_one, abs_pos, OfNat.ofNat, lt_add_iff_pos_left
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
hF :
  (algebraMap ℤ K : (a : ℤ) → K) ev =
    HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
      eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree = 0 ∨
    eval (HMul.hMul (α := K) (β := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) (((algebraMap ℤ K : (a : ℤ) → K) b)⁻¹ : K))
        (Polynomial.map (algebraMap ℤ K) f) =
      0

Tactic:
rw [eq_one_div_of_mul_eq_one_left bu, F0, one_div, eq_intCast, Int.cast_zero, zero_eq_mul] at hF

Premises used: Int.cast_zero, zero_eq_mul, eq_intCast, one_div, eq_one_div_of_mul_eq_one_left
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
hF :
  (algebraMap ℤ K : (a : ℤ) → K) ev =
    HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
      eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF₁ :
  HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree = 0 ∨
    eval (HMul.hMul (α := K) (β := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) (((algebraMap ℤ K : (a : ℤ) → K) b)⁻¹ : K))
        (Polynomial.map (algebraMap ℤ K) f) =
      0
⊢ |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
rw [eq_one_div_of_mul_eq_one_left bu, F0, one_div, eq_intCast, Int.cast_zero, zero_eq_mul] at hF

Premises used: Int.cast_zero, zero_eq_mul, eq_intCast, one_div, eq_one_div_of_mul_eq_one_left
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
hF :
  (algebraMap ℤ K : (a : ℤ) → K) ev =
    HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree *
      eval (HMul.hMul (α := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) bi) (Polynomial.map (algebraMap ℤ K) f)
Fa :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF₁ :
  HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree = 0 ∨
    eval (HMul.hMul (α := K) (β := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) (((algebraMap ℤ K : (a : ℤ) → K) b)⁻¹ : K))
        (Polynomial.map (algebraMap ℤ K) f) =
      0
Fa₁ :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ ev = 0

Tactic:
rw [eq_one_div_of_mul_eq_one_left bu, F0, one_div, eq_intCast, Int.cast_zero, zero_eq_mul] at hF

Premises used: Int.cast_zero, zero_eq_mul, eq_intCast, one_div, eq_one_div_of_mul_eq_one_left
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
hF :
  HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree = 0 ∨
    eval (HMul.hMul (α := K) (β := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) (((algebraMap ℤ K : (a : ℤ) → K) b)⁻¹ : K))
        (Polynomial.map (algebraMap ℤ K) f) =
      0
Fa :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
inl :
  ∀ (hF : HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree = 0),
    eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0
inr :
  ∀
    (hF :
      eval
          (HMul.hMul (α := K) (β := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K)
            (((algebraMap ℤ K : (a : ℤ) → K) b)⁻¹ : K))
          (Polynomial.map (algebraMap ℤ K) f) =
        0),
    eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0
⊢ eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0

Tactic:
rcases hF with hF | hF
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
Fa :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF : HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree = 0
⊢ eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0

Tactic:
(not_le.mpr b0 (le_of_eq (Int.cast_eq_zero.mp (eq_zero_of_pow_eq_zero hF)))).elim

Premises used: not_le, Iff.mpr, False.elim, Iff.mp, Int.cast_eq_zero, eq_zero_of_pow_eq_zero, le_of_eq
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
Fa :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF : HPow.hPow (α := K) ((algebraMap ℤ K : (a : ℤ) → K) b : K) f.natDegree = 0
⊢ eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0

Tactic:
exact (not_le.mpr b0 (le_of_eq (Int.cast_eq_zero.mp (eq_zero_of_pow_eq_zero hF)))).elim

Premises used: not_le, Iff.mpr, False.elim, Iff.mp, Int.cast_eq_zero, eq_zero_of_pow_eq_zero, le_of_eq
-- Module: Mathlib.Algebra.Polynomial.DenomsClearable
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : HMul.hMul (β := K) bi ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
Fa :
  |(↑ev : K)| =
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF :
  eval (HMul.hMul (α := K) (β := K) ((algebraMap ℤ K : (a : ℤ) → K) a : K) (((algebraMap ℤ K : (a : ℤ) → K) b)⁻¹ : K))
      (Polynomial.map (algebraMap ℤ K) f) =
    0
inr inr₁ inr₂ inr₃ : eval (HMul.hMul (α := K) (↑a : K) (↑b : K)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
⊢ eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0

Tactic:
rwa [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
f g : R[X]
⊢ ({ toFun := (⇑derivative : (a : R[X]) → R[X]), map_add' := ⋯, map_smul' := ⋯ } : (a : R[X]) → R[X]) (f * g) =
    HSMul.hSMul (β := R[X]) f
        (({ toFun := (⇑derivative : (a : R[X]) → R[X]), map_add' := ⋯, map_smul' := ⋯ : R[X] →ₗ[R] R[X] } :
              (a : R[X]) → R[X])
            g :
          R[X]) +
      HSMul.hSMul (β := R[X]) g
        (({ toFun := (⇑derivative : (a : R[X]) → R[X]), map_add' := ⋯, map_smul' := ⋯ : R[X] →ₗ[R] R[X] } :
              (a : R[X]) → R[X])
            f :
          R[X])

Tactic:
simp [mul_comm, add_comm, derivative_mul]

Premises used: Polynomial.derivative_mul, add_comm, mul_comm
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
D : Derivation R R[X] A
a : R
⊢ Eq.{u_2 + 1} (α := A) ((D : (a : R[X]) → A) ((C : (a : R) → R[X]) a : R[X]) : A) (0 : A)

Tactic:
D.map_algebraMap a

Premises used: Derivation.map_algebraMap
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
    (D : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
    (D : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f)

Tactic:
have : C a • D f = D (C a * f) := by simp
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
this :
  HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
    (D : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f)
rw :
  (D : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f) =
    HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
rw₁ : (D : (a : R[X]) → A) (a • f) = HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
rw₂ rw₃ : HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A) = HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)
⊢ HSMul.hSMul (α := R[X]) (β := A) ((C : (a : R) → R[X]) a : R[X]) ((D : (a : R[X]) → A) f : A) =
    HSMul.hSMul (β := A) a ((D : (a : R[X]) → A) f : A)

Tactic:
rw [this, C_mul', D.map_smul]

Premises used: Polynomial.C_mul', Derivation.map_smul