awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
rw :
  x * y =
    HDiv.hDiv (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
⊢ x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
have rw₁ : x * y =
  HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯) /
    HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
rw :
  x * y =
    HDiv.hDiv (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
rw₁ :
  x * y =
    HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯) /
      HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
⊢ x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
have rw₂ : x * y =
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) *
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
rw :
  x * y =
    HDiv.hDiv (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
rw₁ :
  x * y =
    HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯) /
      HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
rw₂ :
  x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) *
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
⊢ x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
have rw₃ : x * y =
  x *
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
rw :
  x * y =
    HDiv.hDiv (β := K⟮X⟯)
      (HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯))
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
rw₁ :
  x * y =
    HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯) /
      HMul.hMul (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
rw₂ :
  x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) *
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
rw₃ :
  x * y =
    x *
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯)
⊢ x * y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
have rw₄ : x * y = x * y
Tactic: rw [map_mul, map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
⊢ (x + y).denom ∣ x.denom * y.denom
have rw : ∃ (p : K[X]),
  x + y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
Tactic: rw [denom_dvd (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
⊢ ∃ (p : K[X]),
    x + y =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
have refine : x + y =
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.denom + x.denom * y.num) : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
Tactic: refine ⟨x.num * y.denom + x.denom * y.num, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
⊢ x + y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.denom + x.denom * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
have hb : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) (0 : K⟮X⟯)
Tactic: rw [map_mul, map_add, map_mul, map_mul, ← div_add_div, num_div_denom, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hb : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯) (0 : K⟮X⟯)
⊢ x + y =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.num * y.denom + x.denom * y.num) : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (x.denom * y.denom) : K⟮X⟯)
have hd : Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y.denom : K⟮X⟯) (0 : K⟮X⟯)
Tactic: rw [map_mul, map_add, map_mul, map_mul, ← div_add_div, num_div_denom, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x⁻¹.num ∣ x.denom
have rw : ∃ (q : K[X]),
  q ≠ 0 ∧
    x⁻¹ =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)
Tactic: rw [num_dvd x.denom_ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ ∃ (q : K[X]),
    q ≠ 0 ∧
      x⁻¹ =
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)
have refine : x⁻¹ =
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
Tactic: refine ⟨x.num, num_ne_zero hx, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x⁻¹ =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
have nth_rw : (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯))⁻¹ =
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
Tactic: nth_rw 1 [← x.num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯))⁻¹ =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
have rw : HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯) =
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
Tactic: rw [inv_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x⁻¹.denom ∣ x.num
have rw : ∃ (p : K[X]),
  x⁻¹ =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
Tactic: rw [denom_dvd (num_ne_zero hx)]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ ∃ (p : K[X]),
    x⁻¹ =
      HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
have refine : x⁻¹ =
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.denom : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.num : K⟮X⟯)
Tactic: refine ⟨x.denom, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ Associated x⁻¹.num x.denom
have apply : x.denom ∣ x⁻¹.num
Tactic: apply associated_of_dvd_dvd (num_inv_dvd hx)
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x.denom ∣ x⁻¹.num
have h : x = x⁻¹⁻¹
Tactic: convert! denom_inv_dvd (inv_ne_zero hx)
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x = x⁻¹⁻¹
have h : x = x
Tactic: rw [inv_inv]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ Associated x⁻¹.denom x.num
have a : Associated x.num x⁻¹.denom
Tactic: apply Associated.symm
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ Associated x.num x⁻¹.denom
have h : x = x⁻¹⁻¹
Tactic: convert! associated_num_inv (inv_ne_zero hx)
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
R : Type u_1
F : Type u_2
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : FunLike.{u_2 + 1, u + 1, u_1 + 1} F K[X] R[X]
inst_4 : MonoidHomClass.{u_2, u, u_1} F K[X] R[X]
φ : F
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ R[X]⁰)
f : K⟮X⟯
⊢ (map φ hφ : (a : K⟮X⟯) → R⟮X⟯) f =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) f.num) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((φ : (a : K[X]) → R[X]) f.denom) : R⟮X⟯)
have hq : f.denom ≠ 0
Tactic: rw [← num_div_denom f, map_apply_div_ne_zero, num_div_denom f]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : CommGroupWithZero L
φ : MonoidWithZeroHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
f : K⟮X⟯
⊢ (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L) f =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L)
have rw : (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L)
    (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)) =
  HDiv.hDiv (α := L) (β := L)
    ((φ : (a : K[X]) → L)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)).num :
      L)
    ((φ : (a : K[X]) → L)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)).denom :
      L)
Tactic: rw [← num_div_denom f, liftMonoidWithZeroHom_apply_div, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : CommGroupWithZero L
φ : MonoidWithZeroHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
f : K⟮X⟯
rw :
  (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L)
      (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)) =
    HDiv.hDiv (α := L) (β := L)
      ((φ : (a : K[X]) → L)
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
              ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)).num :
        L)
      ((φ : (a : K[X]) → L)
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
              ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)).denom :
        L)
⊢ (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L) f =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L)
have rw₁ : HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L) =
  HDiv.hDiv (α := L) (β := L)
    ((φ : (a : K[X]) → L)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)).num :
      L)
    ((φ : (a : K[X]) → L)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)).denom :
      L)
Tactic: rw [← num_div_denom f, liftMonoidWithZeroHom_apply_div, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : CommGroupWithZero L
φ : MonoidWithZeroHom.{u, u_1} K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
f : K⟮X⟯
rw :
  (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L)
      (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)) =
    HDiv.hDiv (α := L) (β := L)
      ((φ : (a : K[X]) → L)
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
              ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)).num :
        L)
      ((φ : (a : K[X]) → L)
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
              ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)).denom :
        L)
rw₁ :
  HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L) =
    HDiv.hDiv (α := L) (β := L)
      ((φ : (a : K[X]) → L)
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
              ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)).num :
        L)
      ((φ : (a : K[X]) → L)
          (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.num : K⟮X⟯)
              ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) f.denom : K⟮X⟯)).denom :
        L)
⊢ (liftMonoidWithZeroHom φ hφ : (a : K⟮X⟯) → L) f =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L)
have rw₂ : HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L) =
  HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) f.num : L) ((φ : (a : K[X]) → L) f.denom : L)
Tactic: rw [← num_div_denom f, liftMonoidWithZeroHom_apply_div, num_div_denom]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
⊢ False
have h : (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom
Tactic: have h := num_denom_add x y
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
x y : K⟮X⟯
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
h : (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom
⊢ False
have h₁ : (x + y).num * (x.denom * y.denom) = 0
Tactic: rw [h_zero, zero_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
x y : FractionRing K[X]
xy : { toFractionRing := x : K⟮X⟯ }.toFractionRing = { toFractionRing := y }.toFractionRing
⊢ { toFractionRing := x : K⟮X⟯ } = { toFractionRing := y }
have subst : { toFractionRing := x : K⟮X⟯ } = { toFractionRing := { toFractionRing := x }.toFractionRing }
Tactic: subst xy
Cleared hypotheses: y, xy
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
P : Sort v
n : K[X]
d : ↥K[X]⁰
f : K[X] → K[X] → P
H :
  ∀ {p q p' q' : K[X]} (_hq : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q)
    (_hq' : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q'), q' * p = q * p' → f p q = f p' q'
⊢ { toFractionRing := Localization.mk n d : K⟮X⟯ }.liftOn f @H = f n (↑d : K[X])
have rw : Localization.liftOn { toFractionRing := Localization.mk n d : K⟮X⟯ }.toFractionRing
    (fun (p : K[X]) (q : ↥K[X]⁰) ↦ f p (↑q : K[X])) sorry =
  f n (↑d : K[X])
Tactic: rw [RatFunc.liftOn]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
P : Sort v
f : K[X] → K[X] → P
H : ∀ {p q a : K[X]}, q ≠ 0 → ∀ (_ha : a ≠ 0), f (a * p) (a * q) = f p q
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
h : q' * p = q * p'
⊢ f (q' * p) (q' * q) = f (q * p') (q * q')
have rw : f (q * p') (q' * q) = f (q * p') (q * q')
Tactic: rw [h, mul_comm q']
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
P : Sort v
f : K[X] → K[X] → P
H : ∀ {p q a : K[X]}, q ≠ 0 → ∀ (_ha : a ≠ 0), f (a * p) (a * q) = f p q
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
h : q' * p = q * p'
rw : f (q * p') (q' * q) = f (q * p') (q * q')
⊢ f (q' * p) (q' * q) = f (q * p') (q * q')
have rw₁ : f (q * p') (q * q') = f (q * p') (q * q')
Tactic: rw [h, mul_comm q']
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q : K[X]
⊢ RatFunc.mk p q =
    {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) q : FractionRing K[X]) }
have rw : {
    toFractionRing :=
      HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) q : FractionRing K[X]) :
    K⟮X⟯ } =
  {
    toFractionRing :=
      HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) q : FractionRing K[X]) }
Tactic: rw [RatFunc.mk]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : K[X]
⊢ RatFunc.mk p 0 = { toFractionRing := 0 }
have rw : {
    toFractionRing :=
      HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) 0 : FractionRing K[X]) :
    K⟮X⟯ } =
  { toFractionRing := 0 }
Tactic: rw [mk_eq_div', map_zero, div_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : K[X]
rw :
  {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) 0 : FractionRing K[X]) :
      K⟮X⟯ } =
    { toFractionRing := 0 }
⊢ RatFunc.mk p 0 = { toFractionRing := 0 }
have rw₁ : {
    toFractionRing :=
      HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
        (0 : FractionRing K[X]) :
    K⟮X⟯ } =
  { toFractionRing := 0 }
Tactic: rw [mk_eq_div', map_zero, div_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : K[X]
rw :
  {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) 0 : FractionRing K[X]) :
      K⟮X⟯ } =
    { toFractionRing := 0 }
rw₁ :
  {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) p : FractionRing K[X])
          (0 : FractionRing K[X]) :
      K⟮X⟯ } =
    { toFractionRing := 0 }
⊢ RatFunc.mk p 0 = { toFractionRing := 0 }
have rw₂ : Eq.{u + 1} (α := K⟮X⟯) { toFractionRing := 0 } { toFractionRing := 0 }
Tactic: rw [mk_eq_div', map_zero, div_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Defs (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q : K[X]
hq : q ≠ 0
⊢ RatFunc.mk p q =
    {
      toFractionRing :=
        Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q ⋯) }
have rw : {
    toFractionRing :=
      IsLocalization.mk' (FractionRing K[X]) p
        (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) } =
  {
    toFractionRing :=
      Localization.mk p (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) q sorry) :
    K⟮X⟯ }
Tactic: rw [mk_def_of_ne _ hq, Localization.mk_eq_mk']