awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation (R := K[X]) K⟮X⟯ (idealX K) : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
          (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        RatFunc.X :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have rw : Eq (α := WithZero (Multiplicative ℤ))
  (((valuation (R := K[X]) K⟮X⟯ (idealX K) : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
        (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) X) :
    WithZero (Multiplicative ℤ))
  (exp (-1) : WithZero (Multiplicative ℤ))
Tactic: rw [← RatFunc.algebraMap_X, valuation_of_algebraMap, intValuation_singleton
      _ (Polynomial.X_ne_zero) (idealX_span K)]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation (R := K[X]) K⟮X⟯ (idealX K) : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
          (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) X) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation (R := K[X]) K⟮X⟯ (idealX K) : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
          (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        RatFunc.X :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have rw₁ : Eq (α := WithZero (Multiplicative ℤ))
  (((intValuation (idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) : (a : K[X]) → WithZero (Multiplicative ℤ))
      X :
    WithZero (Multiplicative ℤ))
  (exp (-1) : WithZero (Multiplicative ℤ))
Tactic: rw [← RatFunc.algebraMap_X, valuation_of_algebraMap, intValuation_singleton
      _ (Polynomial.X_ne_zero) (idealX_span K)]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation (R := K[X]) K⟮X⟯ (idealX K) : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
          (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) X) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        X :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation (R := K[X]) K⟮X⟯ (idealX K) : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
          (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        RatFunc.X :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have rw₂ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-1)) (exp (-1))
Tactic: rw [← RatFunc.algebraMap_X, valuation_of_algebraMap, intValuation_singleton
      _ (Polynomial.X_ne_zero) (idealX_span K)]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ)
p : K[X]
hp : p ≠ 0
⊢ (v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) p.natDegree
have h : Eq.{u_1 + 1} (α := (P : K[X]) → K⟮X⟯) coePolynomial (⇑(aeval RatFunc.X) : (a : K[X]) → K⟮X⟯)
Tactic: convert! valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X .X hlt hp
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ)
p : K[X]
hp : p ≠ 0
⊢ Eq.{u_1 + 1} (α := (P : K[X]) → K⟮X⟯) coePolynomial (⇑(aeval RatFunc.X) : (a : K[X]) → K⟮X⟯)
have h : ∀ (p : K[X]), (↑p : K⟮X⟯) = (aeval RatFunc.X : (a : K[X]) → K⟮X⟯) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ)
p_1 : K[X]
hp : p_1 ≠ 0
p : K[X]
⊢ (↑p : K⟮X⟯) = (aeval RatFunc.X : (a : K[X]) → K⟮X⟯) p
have h : Eq.{u_1 + 1} (α := K⟮X⟯) (↑((aeval X : (a : K[X]) → K[X]) p) : K⟮X⟯)
  (((aeval ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) X) : K[X] →ₐ[K] K⟮X⟯) : (a : K[X]) → K⟮X⟯) p)
Tactic: nth_rw 1 [RatFunc.X, ← aeval_X_left_apply p (R := K)]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (1 : Γ)
p : K[X]
⊢ LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ)
have rw : LE.le.{u_2} (α := Γ)
  ((v : (a : K⟮X⟯) → Γ)
      (∑ x ∈ Finset.range (p.natDegree + 1),
        (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial x : (a : K) → K[X]) (p.coeff x))) :
    Γ)
  (1 : Γ)
Tactic: rw [as_sum_range p, RatFunc.coePolynomial, map_sum]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (1 : Γ)
p : K[X]
⊢ LE.le.{u_2} (α := Γ)
    ((v : (a : K⟮X⟯) → Γ)
        (∑ x ∈ Finset.range (p.natDegree + 1),
          (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial x : (a : K) → K[X]) (p.coeff x))) :
      Γ)
    (1 : Γ)
have apply : ∀ i ∈ Finset.range (p.natDegree + 1),
  LE.le.{u_2} (α := Γ)
    ((v : (a : K⟮X⟯) → Γ)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
      Γ)
    (1 : Γ)
Tactic: apply map_sum_le v
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (1 : Γ)
p : K[X]
i : ℕ
⊢ i ∈ Finset.range (p.natDegree + 1) →
    LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
        Γ)
      (1 : Γ)
have pos : ∀ (h0 : p.coeff i = 0),
  i ∈ Finset.range (p.natDegree + 1) →
    LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
        Γ)
      (1 : Γ)
Tactic: by_cases h0 : p.coeff i = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (1 : Γ)
p : K[X]
i : ℕ
pos :
  ∀ (h0 : p.coeff i = 0),
    i ∈ Finset.range (p.natDegree + 1) →
      LE.le.{u_2} (α := Γ)
        ((v : (a : K⟮X⟯) → Γ)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
          Γ)
        (1 : Γ)
⊢ i ∈ Finset.range (p.natDegree + 1) →
    LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
        Γ)
      (1 : Γ)
have neg : ∀ (h0 : ¬p.coeff i = 0),
  i ∈ Finset.range (p.natDegree + 1) →
    LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
        Γ)
      (1 : Γ)
Tactic: by_cases h0 : p.coeff i = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (1 : Γ)
p : K[X]
i : ℕ
h0 : ¬p.coeff i = 0
⊢ i ∈ Finset.range (p.natDegree + 1) →
    LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
        Γ)
      (1 : Γ)
have neg : i ∈ Finset.range (p.natDegree + 1) →
  LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) : Γ) (1 : Γ)
Tactic: rw [← RatFunc.coePolynomial]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
n : WithZero (Multiplicative ℤ)
⊢ ∃ (a : K⟮X⟯),
    ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n
have pos : ∀ (hn0 : n = 0),
  ∃ (a : K⟮X⟯),
    ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
n : WithZero (Multiplicative ℤ)
pos :
  ∀ (hn0 : n = 0),
    ∃ (a : K⟮X⟯),
      ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n
⊢ ∃ (a : K⟮X⟯),
    ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n
have neg : ∀ (hn0 : ¬n = 0),
  ∃ (a : K⟮X⟯),
    ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
⊢ ∃ (a : K⟮X⟯),
    ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n
have h : ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) 0 = n
Tactic: use 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.AsPolynomial (goal)
Goal:
K : Type u_1
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ ∃ (a : K⟮X⟯),
    ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n
have h : ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
    (HPow.hPow (α := K⟮X⟯) X (-n.log)) =
  n
Tactic: use (RatFunc.X ^ (-WithZero.log n))
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p : K⟮X⟯ } ≠ 0
hp : p = 0
⊢ { toFractionRing := p : K⟮X⟯ } = 0
have rw : Eq.{u + 1} (α := K⟮X⟯) { toFractionRing := 0 } 0
Tactic: rw [hp, ofFractionRing_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p : K⟮X⟯ } ≠ 0
hp : p = 0
rw : Eq.{u + 1} (α := K⟮X⟯) { toFractionRing := 0 } 0
⊢ { toFractionRing := p : K⟮X⟯ } = 0
have rw₁ : Eq.{u + 1} (α := K⟮X⟯) 0 0
Tactic: rw [hp, ofFractionRing_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p : K⟮X⟯ } ≠ 0
⊢ { toFractionRing := p : K⟮X⟯ } * { toFractionRing := p : K⟮X⟯ }⁻¹ = 1
have this : p ≠ 0
Tactic: have : p ≠ 0 := fun hp => h <| by rw [hp, ofFractionRing_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : SMul.{u_1, u} R (FractionRing K[X])
c : R
p : K⟮X⟯
⊢ (c • p).toFractionRing = c • p.toFractionRing
have ofFractionRing : ∀ (toFractionRing : FractionRing K[X]),
  (c • { toFractionRing := toFractionRing : K⟮X⟯ }).toFractionRing =
    c • { toFractionRing := toFractionRing : K⟮X⟯ }.toFractionRing
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : SMul.{u_1, u} R (FractionRing K[X])
c : R
toFractionRing : FractionRing K[X]
⊢ (c • { toFractionRing := toFractionRing : K⟮X⟯ }).toFractionRing =
    c • { toFractionRing := toFractionRing : K⟮X⟯ }.toFractionRing
have ofFractionRing : { toFractionRing := c • toFractionRing : K⟮X⟯ }.toFractionRing =
  c • { toFractionRing := toFractionRing : K⟮X⟯ }.toFractionRing
Tactic: rw [← ofFractionRing_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
x : K⟮X⟯
r : K
⊢ r • x = HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) x
have obtain : ∀ (x : FractionRing K[X]),
  r • { toFractionRing := x : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) { toFractionRing := x : K⟮X⟯ }
Tactic: obtain ⟨x⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
r : K
x : FractionRing K[X]
⊢ r • { toFractionRing := x : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) { toFractionRing := x : K⟮X⟯ }
have H : ∀ (y : K[X] × ↥K[X]⁰),
  r • { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
Tactic: induction x using Localization.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
r : K
y : K[X] × ↥K[X]⁰
⊢ r • { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
have H : { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
  HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
    { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
Tactic: rw [← ofFractionRing_smul, ← ofFractionRing_smul, Localization.smul_mk,
    Localization.smul_mk, smul_eq_mul, Polynomial.smul_eq_C_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
r : K
y : K[X] × ↥K[X]⁰
H :
  { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
⊢ r • { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
have H₁ : { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
  { toFractionRing := HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) (Localization.mk y.1 y.2) }
Tactic: rw [← ofFractionRing_smul, ← ofFractionRing_smul, Localization.smul_mk,
    Localization.smul_mk, smul_eq_mul, Polynomial.smul_eq_C_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
r : K
y : K[X] × ↥K[X]⁰
H :
  { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
H₁ :
  { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
    { toFractionRing := HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) (Localization.mk y.1 y.2) }
⊢ r • { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
have H₂ : { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
  { toFractionRing := HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) (Localization.mk y.1 y.2) }
Tactic: rw [← ofFractionRing_smul, ← ofFractionRing_smul, Localization.smul_mk,
    Localization.smul_mk, smul_eq_mul, Polynomial.smul_eq_C_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
r : K
y : K[X] × ↥K[X]⁰
H :
  { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
H₁ :
  { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
    { toFractionRing := HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) (Localization.mk y.1 y.2) }
H₂ :
  { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
    { toFractionRing := HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) (Localization.mk y.1 y.2) }
⊢ r • { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
have H₃ : { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
  { toFractionRing := Localization.mk (HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) y.1) y.2 }
Tactic: rw [← ofFractionRing_smul, ← ofFractionRing_smul, Localization.smul_mk,
    Localization.smul_mk, smul_eq_mul, Polynomial.smul_eq_C_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
r : K
y : K[X] × ↥K[X]⁰
H :
  { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
H₁ :
  { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
    { toFractionRing := HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) (Localization.mk y.1 y.2) }
H₂ :
  { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
    { toFractionRing := HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) (Localization.mk y.1 y.2) }
H₃ :
  { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
    { toFractionRing := Localization.mk (HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) y.1) y.2 }
⊢ r • { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
have H₄ : { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
  { toFractionRing := Localization.mk (HMul.hMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) y.1) y.2 }
Tactic: rw [← ofFractionRing_smul, ← ofFractionRing_smul, Localization.smul_mk,
    Localization.smul_mk, smul_eq_mul, Polynomial.smul_eq_C_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
r : K
y : K[X] × ↥K[X]⁰
H :
  { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
H₁ :
  { toFractionRing := r • Localization.mk y.1 y.2 : K⟮X⟯ } =
    { toFractionRing := HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) (Localization.mk y.1 y.2) }
H₂ :
  { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
    { toFractionRing := HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) (Localization.mk y.1 y.2) }
H₃ :
  { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
    { toFractionRing := Localization.mk (HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) y.1) y.2 }
H₄ :
  { toFractionRing := Localization.mk (r • y.1) y.2 : K⟮X⟯ } =
    { toFractionRing := Localization.mk (HMul.hMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) y.1) y.2 }
⊢ r • { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
      { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
have H₅ : { toFractionRing := Localization.mk (HMul.hMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) y.1) y.2 :
    K⟮X⟯ } =
  { toFractionRing := Localization.mk (HMul.hMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) y.1) y.2 }
Tactic: rw [← ofFractionRing_smul, ← ofFractionRing_smul, Localization.smul_mk,
    Localization.smul_mk, smul_eq_mul, Polynomial.smul_eq_C_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass.{u_1, u} R (FractionRing K[X]) := inferInstance
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
have pos : ∀ (hq : q = 0), RatFunc.mk (c • p) q = c • RatFunc.mk p q
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass.{u_1, u} R (FractionRing K[X]) := inferInstance
pos : ∀ (hq : q = 0), RatFunc.mk (c • p) q = c • RatFunc.mk p q
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
have neg : ∀ (hq : ¬q = 0), RatFunc.mk (c • p) q = c • RatFunc.mk p q
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass.{u_1, u} R (FractionRing K[X]) := inferInstance
hq : q = 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
have pos : RatFunc.mk (c • p) 0 = c • RatFunc.mk p 0
Tactic: rw [hq, mk_zero, mk_zero, ← ofFractionRing_smul, smul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass.{u_1, u} R (FractionRing K[X]) := inferInstance
hq : q = 0
pos : RatFunc.mk (c • p) 0 = c • RatFunc.mk p 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
have pos₁ : { toFractionRing := 0 } = c • RatFunc.mk p 0
Tactic: rw [hq, mk_zero, mk_zero, ← ofFractionRing_smul, smul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass.{u_1, u} R (FractionRing K[X]) := inferInstance
hq : q = 0
pos : RatFunc.mk (c • p) 0 = c • RatFunc.mk p 0
pos₁ : { toFractionRing := 0 } = c • RatFunc.mk p 0
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
have pos₂ : { toFractionRing := 0 } = HSMul.hSMul (β := K⟮X⟯) c { toFractionRing := 0 : K⟮X⟯ }
Tactic: rw [hq, mk_zero, mk_zero, ← ofFractionRing_smul, smul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : IsDomain K
inst_2 : Monoid R
inst_3 : DistribMulAction.{u_1, u} R K[X]
inst_4 : IsScalarTower.{u_1, u, u} R K[X] K[X]
c : R
p q : K[X]
this : SMulZeroClass.{u_1, u} R (FractionRing K[X]) := inferInstance
hq : q = 0
pos : RatFunc.mk (c • p) 0 = c • RatFunc.mk p 0
pos₁ : { toFractionRing := 0 } = c • RatFunc.mk p 0
pos₂ : { toFractionRing := 0 } = HSMul.hSMul (β := K⟮X⟯) c { toFractionRing := 0 : K⟮X⟯ }
⊢ RatFunc.mk (c • p) q = c • RatFunc.mk p q
have pos₃ : { toFractionRing := 0 } = { toFractionRing := HSMul.hSMul (β := FractionRing K[X]) c 0 : K⟮X⟯ }
Tactic: rw [hq, mk_zero, mk_zero, ← ofFractionRing_smul, smul_zero]