awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
h :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
this : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f
⊢ eval a ((derivative : (a : K[X]) → K[X]) f) = 0
have this₁ : Eq (α := K[X]) ((C : (a : K) → K[X]) (eval a ((derivative : (a : K[X]) → K[X]) f)) : K[X]) (0 : K[X])
Tactic: rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
h :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
this : Eq (α := K[X]) ((C : (a : K) → K[X]) (eval a ((derivative : (a : K[X]) → K[X]) f)) : K[X]) (0 : K[X])
⊢ eval a ((derivative : (a : K[X]) → K[X]) f) = 0
have rwa : Eq (α := K[X]) ((C : (a : K) → K[X]) (eval a ((derivative : (a : K[X]) → K[X]) f)) : K[X])
  ((C : (a : K) → K[X]) 0 : K[X])
Tactic: rwa [← C_inj, C_0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf' : eval a ((derivative : (a : K[X]) → K[X]) f) ≠ 0
⊢ IsCoprime (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
    (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
have refine : ¬HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
Tactic: classical
  refine Or.resolve_left
      (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
        (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_
  contrapose hf' with h
  have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h
  rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this
  rwa [← C_inj, C_0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf' : eval a ((derivative : (a : K[X]) → K[X]) f) ≠ 0
refine :
  ¬HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
      f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
⊢ IsCoprime (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
    (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
have refine₁ : ∀
  (h :
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
      f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])),
  eval a ((derivative : (a : K[X]) → K[X]) f) = 0
Tactic: classical
  refine Or.resolve_left
      (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
        (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_
  contrapose hf' with h
  have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h
  rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this
  rwa [← C_inj, C_0]
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf' : eval a ((derivative : (a : K[X]) → K[X]) f) ≠ 0
refine :
  ¬HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
      f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
refine₁ :
  ∀
    (h :
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
        f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])),
    eval a ((derivative : (a : K[X]) → K[X]) f) = 0
⊢ IsCoprime (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
    (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
have refine₂ : ∀
  (h :
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
      f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
  (this : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f),
  eval a ((derivative : (a : K[X]) → K[X]) f) = 0
Tactic: classical
  refine Or.resolve_left
      (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
        (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_
  contrapose hf' with h
  have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h
  rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this
  rwa [← C_inj, C_0]
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf' : eval a ((derivative : (a : K[X]) → K[X]) f) ≠ 0
refine :
  ¬HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
      f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
refine₁ :
  ∀
    (h :
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
        f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])),
    eval a ((derivative : (a : K[X]) → K[X]) f) = 0
refine₂ :
  ∀
    (h :
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
        f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
    (this : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f),
    eval a ((derivative : (a : K[X]) → K[X]) f) = 0
⊢ IsCoprime (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
    (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
have refine₃ : ∀
  (h :
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
      f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
  (this : Eq (α := K[X]) ((C : (a : K) → K[X]) (eval a ((derivative : (a : K[X]) → K[X]) f)) : K[X]) (0 : K[X])),
  eval a ((derivative : (a : K[X]) → K[X]) f) = 0
Tactic: classical
  refine Or.resolve_left
      (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
        (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_
  contrapose hf' with h
  have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h
  rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this
  rwa [← C_inj, C_0]
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ Irreducible p ↔ ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q
have rw : (∀ (q : R[X]),
    q.degree ≤ (↑((HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X])).natDegree / 2) : WithBot ℕ) →
      q ∣ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) → IsUnit q) ↔
  ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q
Tactic: rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_degree_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
rw :
  (∀ (q : R[X]),
      q.degree ≤
          (↑((HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X])).natDegree / 2) : WithBot ℕ) →
        q ∣ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) → IsUnit q) ↔
    ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q
⊢ Irreducible p ↔ ∀ (q : R[X]), q.degree ≤ (↑(p.natDegree / 2) : WithBot ℕ) → q ∣ p → IsUnit q
have rw₁ : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) ≠ 1
Tactic: rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_degree_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) ≠ 1
have contrapose : ∀ (hpu : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) = 1), IsUnit p
Tactic: contrapose hpu
Cleared hypotheses: hpu
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p
have this : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) ≠ 1
Tactic: have : p * C (leadingCoeff p)⁻¹ ≠ 1 := by
    contrapose hpu
    exact .of_mul_eq_one _ hpu
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
this : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X]) ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p
have rw : (∀ (q : R[X]),
    q.Monic →
      q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) →
        ¬q ∣ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) p.leadingCoeff⁻¹ : R[X])) ↔
  ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p
Tactic: rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_lt_natDegree_lt this,
      natDegree_mul_leadingCoeff_inv _ hp0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
a : R[X]
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a
have pos : ∀ (ha : a = 0), HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
a : R[X]
pos : ∀ (ha : a = 0), HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a
have neg : ∀ (ha : ¬a = 0), HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a
have neg : a * (C : (a : R) → R[X]) 1 = a
Tactic: rw [prod_normalizedFactors_eq, normalize_apply, coe_normUnit, CommGroupWithZero.coe_normUnit,
    mul_comm, mul_assoc, ← map_mul, inv_mul_cancel₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
a : R[X]
ha : ¬a = 0
neg : a * (C : (a : R) → R[X]) 1 = a
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a
have neg₁ : a.leadingCoeff ≠ 0
Tactic: rw [prod_normalizedFactors_eq, normalize_apply, coe_normUnit, CommGroupWithZero.coe_normUnit,
    mul_comm, mul_assoc, ← map_mul, inv_mul_cancel₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
a : R[X]
ha : ¬a = 0
neg : a * (C : (a : R) → R[X]) 1 = a
neg₁ : a.leadingCoeff ≠ 0
neg₂ : a.leadingCoeff ≠ 0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a.leadingCoeff : R[X]) (normalizedFactors a).prod = a
have neg₃ : a ≠ 0
Tactic: rw [prod_normalizedFactors_eq, normalize_apply, coe_normUnit, CommGroupWithZero.coe_normUnit,
    mul_comm, mul_assoc, ← map_mul, inv_mul_cancel₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
inst_1 : DecidableEq R
hq : q ≠ 0
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
have pos : ∀ (hp : p = 0), p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
inst_1 : DecidableEq R
hq : q ≠ 0
pos : ∀ (hp : p = 0), p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
have neg : ∀ (hp : ¬p = 0), p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
inst_1 : DecidableEq R
hq : q ≠ 0
hp : ¬p = 0
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
have neg : Irreducible p ∧ (normalize : (a : R[X]) → R[X]) p = p ∧ p ∣ q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
Tactic: rw [mem_normalizedFactors_iff' hq, normalize_eq_self_iff_monic hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
inst_1 : DecidableEq R
hq : q ≠ 0
hp : ¬p = 0
neg : Irreducible p ∧ (normalize : (a : R[X]) → R[X]) p = p ∧ p ∣ q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
have neg₁ : Irreducible p ∧ p.Monic ∧ p ∣ q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
Tactic: rw [mem_normalizedFactors_iff' hq, normalize_eq_self_iff_monic hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
p : R[X]
inst_1 : DecidableEq R
inst_2 : Field S
inst_3 : DecidableEq S
f : R →+* S
⊢ map f ((normalize : (a : R[X]) → R[X]) p) = (normalize : (a : S[X]) → S[X]) (map f p)
have pos : ∀ (hp : p = 0), map f ((normalize : (a : R[X]) → R[X]) p) = (normalize : (a : S[X]) → S[X]) (map f p)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
inst : Field R
p : R[X]
inst_1 : DecidableEq R
inst_2 : Field S
inst_3 : DecidableEq S
f : R →+* S
pos : ∀ (hp : p = 0), map f ((normalize : (a : R[X]) → R[X]) p) = (normalize : (a : S[X]) → S[X]) (map f p)
⊢ map f ((normalize : (a : R[X]) → R[X]) p) = (normalize : (a : S[X]) → S[X]) (map f p)
have neg : ∀ (hp : ¬p = 0), map f ((normalize : (a : R[X]) → R[X]) p) = (normalize : (a : S[X]) → S[X]) (map f p)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
⊢ p₁ % q = p₂ % q
have inl : ∀ (h : 0 ∣ p₁ - p₂), p₁ % 0 = p₂ % 0
Tactic: obtain rfl | hq := eq_or_ne q 0
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
inl : ∀ (h : 0 ∣ p₁ - p₂), p₁ % 0 = p₂ % 0
⊢ p₁ % q = p₂ % q
have inr : ∀ (hq : q ≠ 0), p₁ % q = p₂ % q
Tactic: obtain rfl | hq := eq_or_ne q 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ p₁ %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) =
    p₂ %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
have inr : HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) ∣ p₁ - p₂
Tactic: apply Polynomial.modByMonic_eq_of_dvd_sub (by simp [Polynomial.Monic.def, hq])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) ∣ p₁ - p₂
have inr : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) q ∣ p₁ - p₂
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
⊢ False
have obtain : ∀ (x : F) (hf : (C : (a : F) → F[X]) x = f), False
Tactic: obtain ⟨x, hf⟩ := natDegree_eq_zero.1 H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : (C : (a : F) → F[X]) x = f
⊢ False
have pos : ∀ (hx : x = 0), False
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : (C : (a : F) → F[X]) x = f
pos : ∀ (hx : x = 0), False
⊢ False
have neg : ∀ (hx : ¬x = 0), False
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : (C : (a : F) → F[X]) x = f
hx : x = 0
⊢ False
have h₁ : Irreducible.{u_1} (M := F[X]) 0
Tactic: rw [← hf, hx, map_zero] at h
Cleared hypotheses: h, hf, hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
F : Type u_1
inst : DivisionSemiring F
f : F[X]
h : Irreducible f
⊢ 0 < f.degree
have rw : 0 < f.natDegree
Tactic: rw [← natDegree_pos_iff_degree_pos]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
R : Type u_2
inst_1 : Semiring R
inst_2 : MulSemiringAction M R
m : M
⊢ HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)
have h : ∀ (x : R[X]) (n : ℕ), (m • x).coeff n = (map (MulSemiringAction.toRingHom M R m) x).coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x r : S
⊢ eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X])) = m • eval x ((C : (a : S) → S[X]) r)
have rw : eval (m • x) ((C : (a : S) → S[X]) (m • r)) = m • eval x ((C : (a : S) → S[X]) r)
Tactic: rw [smul_C, eval_C, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x r : S
rw : eval (m • x) ((C : (a : S) → S[X]) (m • r)) = m • eval x ((C : (a : S) → S[X]) r)
⊢ eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X])) = m • eval x ((C : (a : S) → S[X]) r)
have rw₁ : m • r = m • eval x ((C : (a : S) → S[X]) r)
Tactic: rw [smul_C, eval_C, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x r : S
rw : eval (m • x) ((C : (a : S) → S[X]) (m • r)) = m • eval x ((C : (a : S) → S[X]) r)
rw₁ : m • r = m • eval x ((C : (a : S) → S[X]) r)
⊢ eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X])) = m • eval x ((C : (a : S) → S[X]) r)
have rw₂ : m • r = m • r
Tactic: rw [smul_C, eval_C, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f_1 : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)
have rw : eval (m • x) (m • f + m • g) = m • eval x (f + g)
Tactic: rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f_1 : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
rw : eval (m • x) (m • f + m • g) = m • eval x (f + g)
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)
have rw₁ : eval (m • x) (m • f) + eval (m • x) (m • g) = m • eval x (f + g)
Tactic: rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f_1 : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
rw : eval (m • x) (m • f + m • g) = m • eval x (f + g)
rw₁ : eval (m • x) (m • f) + eval (m • x) (m • g) = m • eval x (f + g)
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)
have rw₂ : m • eval x f + eval (m • x) (m • g) = m • eval x (f + g)
Tactic: rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f_1 : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
rw : eval (m • x) (m • f + m • g) = m • eval x (f + g)
rw₁ : eval (m • x) (m • f) + eval (m • x) (m • g) = m • eval x (f + g)
rw₂ : m • eval x f + eval (m • x) (m • g) = m • eval x (f + g)
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)
have rw₃ : m • eval x f + m • eval x g = m • eval x (f + g)
Tactic: rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f_1 : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
rw : eval (m • x) (m • f + m • g) = m • eval x (f + g)
rw₁ : eval (m • x) (m • f) + eval (m • x) (m • g) = m • eval x (f + g)
rw₂ : m • eval x f + eval (m • x) (m • g) = m • eval x (f + g)
rw₃ : m • eval x f + m • eval x g = m • eval x (f + g)
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)
have rw₄ : m • eval x f + m • eval x g = m • (eval x f + eval x g)
Tactic: rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f_1 : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
rw : eval (m • x) (m • f + m • g) = m • eval x (f + g)
rw₁ : eval (m • x) (m • f) + eval (m • x) (m • g) = m • eval x (f + g)
rw₂ : m • eval x f + eval (m • x) (m • g) = m • eval x (f + g)
rw₃ : m • eval x f + m • eval x g = m • eval x (f + g)
rw₄ : m • eval x f + m • eval x g = m • (eval x f + eval x g)
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)
have rw₅ : m • eval x f + m • eval x g = m • eval x f + m • eval x g
Tactic: rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.GroupRingAction (goal)
Goal:
M : Type u_1
inst : Monoid M
S : Type u_3
inst_1 : CommSemiring S
inst_2 : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
h :
  eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n)) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X n))
⊢ eval (m • x) (m • HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1))) =
    m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
have rw : eval (m • x) (HSMul.hSMul (β := S[X]) m ((C : (a : S) → S[X]) r : S[X]) * m • HPow.hPow (α := S[X]) X (n + 1)) =
  m • eval x (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) r : S[X]) (HPow.hPow (α := S[X]) X (n + 1)))
Tactic: rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_X_pow, eval_mul, eval_C,
      eval_X_pow, smul_mul', smul_pow']