awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
G₀ : Type u_1
R : Type u_3
inst : CommGroupWithZero G₀
inst_1 : CommRing R
inst_2 : Nontrivial R
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : Function.Injective.{u_3 + 1, u_1 + 1} (α := R[X]) (β := G₀) (⇑φ : (a : R[X]) → G₀)
hφ' : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
y a' : R[X] × ↥R[X]⁰
h :
  HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) =
    HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀)
⊢ (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
have H : ∀
  (this :
    HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀) =
      HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)),
  (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
Tactic: have := mul_eq_mul_of_div_eq_div _ _ ?_ ?_ h
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
G₀ : Type u_1
R : Type u_3
inst : CommGroupWithZero G₀
inst_1 : CommRing R
inst_2 : Nontrivial R
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : Function.Injective.{u_3 + 1, u_1 + 1} (α := R[X]) (β := G₀) (⇑φ : (a : R[X]) → G₀)
hφ' : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
y a' : R[X] × ↥R[X]⁰
h :
  HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) =
    HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀)
H :
  ∀
    (this :
      HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀) =
        HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
⊢ (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
have H₁ : Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) (0 : G₀)
Tactic: have := mul_eq_mul_of_div_eq_div _ _ ?_ ?_ h
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
G₀ : Type u_1
R : Type u_3
inst : CommGroupWithZero G₀
inst_1 : CommRing R
inst_2 : Nontrivial R
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : Function.Injective.{u_3 + 1, u_1 + 1} (α := R[X]) (β := G₀) (⇑φ : (a : R[X]) → G₀)
hφ' : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
y a' : R[X] × ↥R[X]⁰
h :
  HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) =
    HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀)
H :
  ∀
    (this :
      HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀) =
        HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
H₁ : Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) (0 : G₀)
⊢ (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
have H₂ : Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀) (0 : G₀)
Tactic: have := mul_eq_mul_of_div_eq_div _ _ ?_ ?_ h
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
G₀ : Type u_1
R : Type u_3
inst : CommGroupWithZero G₀
inst_1 : CommRing R
inst_2 : Nontrivial R
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : Function.Injective.{u_3 + 1, u_1 + 1} (α := R[X]) (β := G₀) (⇑φ : (a : R[X]) → G₀)
hφ' : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
y a' : R[X] × ↥R[X]⁰
h :
  HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) =
    HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀)
this :
  HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀) =
    HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)
⊢ (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
have H : ∀
  (this :
    (φ : (a : R[X]) → G₀) (y.1 * (↑a'.2 : R[X])) =
      HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)),
  (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
Tactic: rwa [← map_mul, ← map_mul, hφ.eq_iff, mul_comm, mul_comm a'.fst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
G₀ : Type u_1
R : Type u_3
inst : CommGroupWithZero G₀
inst_1 : CommRing R
inst_2 : Nontrivial R
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : Function.Injective.{u_3 + 1, u_1 + 1} (α := R[X]) (β := G₀) (⇑φ : (a : R[X]) → G₀)
hφ' : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
y a' : R[X] × ↥R[X]⁰
h :
  HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) =
    HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀)
this :
  HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀) =
    HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)
H :
  ∀
    (this :
      (φ : (a : R[X]) → G₀) (y.1 * (↑a'.2 : R[X])) =
        HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
⊢ (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
have H₁ : ∀
  (this :
    Eq.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (y.1 * (↑a'.2 : R[X])) : G₀)
      ((φ : (a : R[X]) → G₀) (a'.1 * (↑y.2 : R[X])) : G₀)),
  (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
Tactic: rwa [← map_mul, ← map_mul, hφ.eq_iff, mul_comm, mul_comm a'.fst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
G₀ : Type u_1
R : Type u_3
inst : CommGroupWithZero G₀
inst_1 : CommRing R
inst_2 : Nontrivial R
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : Function.Injective.{u_3 + 1, u_1 + 1} (α := R[X]) (β := G₀) (⇑φ : (a : R[X]) → G₀)
hφ' : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
y a' : R[X] × ↥R[X]⁰
h :
  HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) =
    HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀)
this :
  HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀) =
    HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)
H :
  ∀
    (this :
      (φ : (a : R[X]) → G₀) (y.1 * (↑a'.2 : R[X])) =
        HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
H₁ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (y.1 * (↑a'.2 : R[X])) : G₀)
        ((φ : (a : R[X]) → G₀) (a'.1 * (↑y.2 : R[X])) : G₀)),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
⊢ (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
have H₂ : ∀ (this : y.1 * (↑a'.2 : R[X]) = a'.1 * (↑y.2 : R[X])),
  (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
Tactic: rwa [← map_mul, ← map_mul, hφ.eq_iff, mul_comm, mul_comm a'.fst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
G₀ : Type u_1
R : Type u_3
inst : CommGroupWithZero G₀
inst_1 : CommRing R
inst_2 : Nontrivial R
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : Function.Injective.{u_3 + 1, u_1 + 1} (α := R[X]) (β := G₀) (⇑φ : (a : R[X]) → G₀)
hφ' : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
y a' : R[X] × ↥R[X]⁰
h :
  HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) =
    HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀)
this :
  HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀) =
    HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)
H :
  ∀
    (this :
      (φ : (a : R[X]) → G₀) (y.1 * (↑a'.2 : R[X])) =
        HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
H₁ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (y.1 * (↑a'.2 : R[X])) : G₀)
        ((φ : (a : R[X]) → G₀) (a'.1 * (↑y.2 : R[X])) : G₀)),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
H₂ :
  ∀ (this : y.1 * (↑a'.2 : R[X]) = a'.1 * (↑y.2 : R[X])),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
⊢ (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
have H₃ : ∀ (this : (↑a'.2 : R[X]) * y.1 = a'.1 * (↑y.2 : R[X])),
  (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
Tactic: rwa [← map_mul, ← map_mul, hφ.eq_iff, mul_comm, mul_comm a'.fst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
G₀ : Type u_1
R : Type u_3
inst : CommGroupWithZero G₀
inst_1 : CommRing R
inst_2 : Nontrivial R
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : Function.Injective.{u_3 + 1, u_1 + 1} (α := R[X]) (β := G₀) (⇑φ : (a : R[X]) → G₀)
hφ' : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
y a' : R[X] × ↥R[X]⁰
h :
  HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) =
    HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀)
this :
  HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) y.1 : G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀) =
    HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)
H :
  ∀
    (this :
      (φ : (a : R[X]) → G₀) (y.1 * (↑a'.2 : R[X])) =
        HMul.hMul (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) a'.1 : G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀)),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
H₁ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (y.1 * (↑a'.2 : R[X])) : G₀)
        ((φ : (a : R[X]) → G₀) (a'.1 * (↑y.2 : R[X])) : G₀)),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
H₂ :
  ∀ (this : y.1 * (↑a'.2 : R[X]) = a'.1 * (↑y.2 : R[X])),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
H₃ :
  ∀ (this : (↑a'.2 : R[X]) * y.1 = a'.1 * (↑y.2 : R[X])),
    (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
⊢ (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
have H₄ : ∀ (this : (↑a'.2 : R[X]) * y.1 = (↑y.2 : R[X]) * a'.1),
  (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
Tactic: rwa [← map_mul, ← map_mul, hφ.eq_iff, mul_comm, mul_comm a'.fst] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
x y : R⟮X⟯
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [ZeroHom.toFun_eq_coe, MonoidWithZeroHom.toZeroHom_coe]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
x y : R⟮X⟯
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have inl : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
x y : R⟮X⟯
inl : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
x y : R⟮X⟯
h : Nontrivial R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain ⟨x⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
y : R⟮X⟯
h : Nontrivial R
x : FractionRing R[X]
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain ⟨y⟩ := y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
x y : FractionRing R[X]
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: cases x using Localization.induction_on with | _ pq
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
y : FractionRing R[X]
pq : R[X] × ↥R[X]⁰
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: cases y using Localization.induction_on with | _ p'q'
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
pq p'q' : R[X] × ↥R[X]⁰
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain ⟨p, q⟩ := pq
Cleared hypotheses: pq
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p'q' : R[X] × ↥R[X]⁰
p : R[X]
q : ↥R[X]⁰
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain ⟨p', q'⟩ := p'q'
Cleared hypotheses: p'q'
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have inr : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [← ofFractionRing_add, Localization.add_mk]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have inr : HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) ((↑q : R[X]) * p' + (↑q' : R[X]) * p) : L)
    ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) =
  HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) +
    HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p' : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)
Tactic: simp only [RingHom.toMonoidWithZeroHom_eq_coe,
        liftMonoidWithZeroHom_apply_ofFractionRing_mk]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) ((↑q : R[X]) * p' + (↑q' : R[X]) * p) : L)
      ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) +
      HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p' : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)
have inr : HMul.hMul (α := L) ((φ : (a : R[X]) → L) ((↑q : R[X]) * p' + (↑q' : R[X]) * p) : L)
    (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)) =
  HMul.hMul (β := L)
    (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) +
      HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) p' : L))
    ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L)
Tactic: rw [div_add_div, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
inr :
  HMul.hMul (α := L) ((φ : (a : R[X]) → L) ((↑q : R[X]) * p' + (↑q' : R[X]) * p) : L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)) =
    HMul.hMul (β := L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) +
        HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) p' : L))
      ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L)
⊢ HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) ((↑q : R[X]) * p' + (↑q' : R[X]) * p) : L)
      ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) +
      HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p' : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)
have inr₁ : Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) (0 : L)
Tactic: rw [div_add_div, div_eq_div_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst_1 : CommGroupWithZero G₀
inst_2 : Field L
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
φ : RingHom.{u_3, u_2} R[X] L
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ L⁰)
h : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
inr :
  HMul.hMul (α := L) ((φ : (a : R[X]) → L) ((↑q : R[X]) * p' + (↑q' : R[X]) * p) : L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)) =
    HMul.hMul (β := L)
      (HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) +
        HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) p' : L))
      ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L)
inr₁ : Ne.{u_2 + 1} (α := L) ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) (0 : L)
⊢ HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) ((↑q : R[X]) * p' + (↑q' : R[X]) * p) : L)
      ((φ : (a : R[X]) → L) (↑(q * q') : R[X]) : L) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p : L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) +
      HDiv.hDiv (α := L) (β := L) ((φ : (a : R[X]) → L) p' : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L)
have inr₂ : HMul.hMul (α := L) (β := L) ((φ : (a : R[X]) → L) (↑q : R[X]) : L) ((φ : (a : R[X]) → L) (↑q' : R[X]) : L) ≠ 0
Tactic: rw [div_add_div, div_eq_div_iff]