awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
h : IsUnit p
h_1 : Nontrivial R
q : R[X]
hq : p * q = 1
this : (p * q).natDegree = p.natDegree + q.natDegree
⊢ p.natDegree = 0
have this₁ : p.natDegree = 0 ∧ q.natDegree = 0
Tactic: rw [hq, natDegree_one, eq_comm, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
⊢ ¬IsUnit p
have inl : Subsingleton R → ¬IsUnit p
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
inl : Subsingleton R → ¬IsUnit p
⊢ ¬IsUnit p
have inr : Nontrivial R → ¬IsUnit p
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
u : R[X]ˣ
⊢ (↑u : R[X]).natDegree = 0
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
u : R[X]ˣ
| 0
have rw : (↑u : R[X]).natDegree
Tactic: rw [← natDegree_coe_units u]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
u : R[X]ˣ
⊢ (↑u : R[X]).coeff 0 ≠ 0
have conv : (↑u : R[X]).coeff (↑u : R[X]).natDegree ≠ 0
Tactic: conv in 0 => rw [← natDegree_coe_units u]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
u : R[X]ˣ
⊢ (↑u : R[X]).coeff (↑u : R[X]).natDegree ≠ 0
have rw : ¬(↑u : R[X]) = 0
Tactic: rw [← leadingCoeff, Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (goal)
Goal:
R : Type u
inst : CommSemiring R
a p : R[X]
hp : p.Monic
ha : ¬IsUnit a
hap : a ∣ p
⊢ 0 < a.degree
have contrapose! : ∀ (h : a.degree ≤ 0), IsUnit a
Tactic: contrapose! ha with h
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (goal)
Goal:
R : Type u
inst : CommSemiring R
a p : R[X]
hp : p.Monic
hap : a ∣ p
h : a.degree ≤ 0
⊢ IsUnit a
have rw : ∀ (hap : (C : (a : R) → R[X]) (a.coeff 0) ∣ p) (h : a.degree ≤ 0),
  IsUnit (M := R[X]) ((C : (a : R) → R[X]) (a.coeff 0) : R[X])
Tactic: rw [Polynomial.eq_C_of_degree_le_zero h] at hap ⊢
Cleared hypotheses: hap, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
n : ℕ
r : R
nN : n ≤ N
⊢ DenomsClearable a b N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) i
have refine : (i : (a : R) → K) (r * a ^ n * b ^ (N - n)) =
  HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
    eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi)
      (Polynomial.map i (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
Tactic: refine ⟨r * a ^ n * b ^ (N - n), bi, bu, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
n : ℕ
r : R
nN : n ≤ N
⊢ (i : (a : R) → K) (r * a ^ n * b ^ (N - n)) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi)
        (Polynomial.map i (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
have rw : (i : (a : R) → K) (r * a ^ n * b ^ (N - n)) =
  HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
    HMul.hMul (α := K) ((i : (a : R) → K) r : K) (eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi) X ^ n)
Tactic: rw [C_mul_X_pow_eq_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, eval_mul, eval_pow, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
n : ℕ
r : R
nN : n ≤ N
⊢ (i : (a : R) → K) (r * a ^ n * b ^ (N - n)) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi) X ^ n)
have rw : HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n) *
    HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HPow.hPow (α := K) ((i : (a : R) → K) a : K) n) =
  HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
    HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi ^ n)
Tactic: rw [map_mul, map_mul, map_pow, map_pow, eval_X, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
n : ℕ
r : R
nN : n ≤ N
⊢ HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HPow.hPow (α := K) ((i : (a : R) → K) a : K) n) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi ^ n)
have rw : HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n - n) *
    HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HPow.hPow (α := K) ((i : (a : R) → K) a : K) n) =
  HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n) *
    HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi ^ n)
Tactic: rw [← tsub_add_cancel_of_le nN]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
n : ℕ
r : R
nN : n ≤ N
| HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n - n) *
    HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HPow.hPow (α := K) ((i : (a : R) → K) a : K) n)
have rw : HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n - n) *
  HMul.hMul (α := K) ((i : (a : R) → K) r : K)
    (HMul.hMul (α := K) ((i : (a : R) → K) a : K) (HMul.hMul (β := K) bi ((i : (a : R) → K) b : K)) ^ n)
Tactic: rw [← mul_one (i a), ← bu]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
n : ℕ
r : R
nN : n ≤ N
⊢ HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n - n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HPow.hPow (α := K) ((i : (a : R) → K) a : K) n) =
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n) *
      HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi ^ n)
have conv_lhs : HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n - n) *
    HMul.hMul (α := K) ((i : (a : R) → K) r : K)
      (HMul.hMul (α := K) ((i : (a : R) → K) a : K) (HMul.hMul (β := K) bi ((i : (a : R) → K) b : K)) ^ n) =
  HPow.hPow (α := K) ((i : (a : R) → K) b : K) (N - n + n) *
    HMul.hMul (α := K) ((i : (a : R) → K) r : K) (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bi ^ n)
Tactic: conv_lhs => rw [← mul_one (i a), ← bu]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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)
⊢ (i : (a : R) → K) (Df + Dg) =
    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 + g))
have rw : 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) +
    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) =
  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) +
    HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
      eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i g)
Tactic: rw [map_add, Polynomial.map_add, eval_add, mul_add, Hf, Hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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)
⊢ 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) +
      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) =
    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) +
      HPow.hPow (α := K) ((i : (a : R) → K) b : K) N *
        eval (HMul.hMul (α := K) ((i : (a : R) → K) a : K) bf) (Polynomial.map i g)
have e_a : bg = bf
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
have e_a : HMul.hMul (α := K) ((i : (a : R) → K) b : K) bg = 1
Tactic: refine @inv_unique K _ (i b) bg bf ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
⊢ bg = bf
have e_a₁ : HMul.hMul (α := K) ((i : (a : R) → K) b : K) bf = 1
Tactic: refine @inv_unique K _ (i b) bg bf ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
⊢ HMul.hMul (β := K) (HDiv.hDiv (α := K) 1 (↑b : K)) ((algebraMap ℤ K : (a : ℤ) → K) b : K) = 1
have rw : Ne.{u_1 + 1} (α := K) (↑b : K) 0
Tactic: rw [eq_intCast, one_div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
⊢ Ne.{u_1 + 1} (α := K) (↑b : K) 0
have rw : b ≠ 0
Tactic: rw [Int.cast_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
⊢ 1 ≤
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f)|
have 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)|
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)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (hypothesis)
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)
⊢ 1 ≤
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f)|
have 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)|
Tactic: obtain Fa := congr_arg abs hF
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (hypothesis)
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)|
⊢ 1 ≤
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f)|
have 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)|
Tactic: rw [eq_one_div_of_mul_eq_one_left bu, eq_intCast, eq_intCast, abs_mul] at Fa
Cleared hypotheses: Fa
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (hypothesis)
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)|
⊢ 1 ≤
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f)|
have Fa₁ : |(↑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
Cleared hypotheses: Fa
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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 ≤
    HPow.hPow (α := K) (↑b : K) f.natDegree *
      |eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f)|
have rw : 1 ≤ |ev|
Tactic: rw [div_eq_mul_inv, ← Fa, ← Int.cast_abs, ← Int.cast_one, Int.cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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|
have refine : ∀ (F0 : ev = 0), eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0
Tactic: refine Int.le_of_lt_add_one ((lt_add_iff_pos_left 1).mpr (abs_pos.mpr fun F0 => fab ?_))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (hypothesis)
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
⊢ eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0
have 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
Tactic: rw [eq_one_div_of_mul_eq_one_left bu, F0, one_div, eq_intCast, Int.cast_zero, zero_eq_mul] at hF
Cleared hypotheses: hF, Fa, F0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
⊢ eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0
have 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
Tactic: rcases hF with hF | hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.DenomsClearable (goal)
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
⊢ eval (HDiv.hDiv (α := K) (↑a : K) (↑b : K)) (Polynomial.map (algebraMap ℤ K) f) = 0
have 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
Tactic: rcases hF with hF | hF
Cleared hypotheses: hF