awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
F : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_4 + 1} F R[X] S[X]
inst_3 : MonoidHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := R[X]) (β := S[X]) (⇑φ : (a : R[X]) → S[X])
y : FractionRing R[X]
y_1 : R[X] × ↥R[X]⁰
h :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk y_1.1 y_1.2 } : S⟮X⟯)
    ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := y } : S⟮X⟯)
⊢ { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } = { toFractionRing := y }
have H : ∀ (y : R[X] × ↥R[X]⁰)
  (h :
    Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk y_1.1 y_1.2 } : S⟮X⟯)
      ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk y.1 y.2 } : S⟮X⟯)),
  { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } = { toFractionRing := Localization.mk y.1 y.2 }
Tactic: induction y using Localization.induction_on
Cleared hypotheses: y, h
-- 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]
inst_6 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun 0 = 0
have simp_rw : Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) 0) 0
Tactic: simp_rw [MonoidHom.toFun_eq_coe, ← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰),
        ← Localization.mk_zero (1 : S[X]⁰), map_apply_ofFractionRing_mk, map_zero,
        Localization.mk_eq_mk', IsLocalization.mk'_zero]
-- 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]
inst_6 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
simp_rw : Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) 0) 0
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun 0 = 0
have simp_rw₁ : Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := 0 } : S⟮X⟯)
  ({ toFractionRing := 0 } : S⟮X⟯)
Tactic: simp_rw [MonoidHom.toFun_eq_coe, ← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰),
        ← Localization.mk_zero (1 : S[X]⁰), map_apply_ofFractionRing_mk, map_zero,
        Localization.mk_eq_mk', IsLocalization.mk'_zero]
-- 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]
inst_6 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
simp_rw : Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) 0) 0
simp_rw₁ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := 0 } : S⟮X⟯)
    ({ toFractionRing := 0 } : S⟮X⟯)
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun 0 = 0
have simp_rw₂ : Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
  ({ toFractionRing := 0 } : S⟮X⟯)
Tactic: simp_rw [MonoidHom.toFun_eq_coe, ← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰),
        ← Localization.mk_zero (1 : S[X]⁰), map_apply_ofFractionRing_mk, map_zero,
        Localization.mk_eq_mk', IsLocalization.mk'_zero]
-- 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]
inst_6 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
simp_rw : Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) 0) 0
simp_rw₁ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := 0 } : S⟮X⟯)
    ({ toFractionRing := 0 } : S⟮X⟯)
simp_rw₂ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
    ({ toFractionRing := 0 } : S⟮X⟯)
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun 0 = 0
have simp_rw₃ : Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
  ({ toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
Tactic: simp_rw [MonoidHom.toFun_eq_coe, ← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰),
        ← Localization.mk_zero (1 : S[X]⁰), map_apply_ofFractionRing_mk, map_zero,
        Localization.mk_eq_mk', IsLocalization.mk'_zero]
-- 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]
inst_6 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
simp_rw : Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) 0) 0
simp_rw₁ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := 0 } : S⟮X⟯)
    ({ toFractionRing := 0 } : S⟮X⟯)
simp_rw₂ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
    ({ toFractionRing := 0 } : S⟮X⟯)
simp_rw₃ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
    ({ toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun 0 = 0
have simp_rw₄ : {
    toFractionRing :=
      Localization.mk ((φ : (a : R[X]) → S[X]) 0)
        (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
          ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) sorry) :
    S⟮X⟯ } =
  { toFractionRing := Localization.mk 0 1 }
Tactic: simp_rw [MonoidHom.toFun_eq_coe, ← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰),
        ← Localization.mk_zero (1 : S[X]⁰), map_apply_ofFractionRing_mk, map_zero,
        Localization.mk_eq_mk', IsLocalization.mk'_zero]
-- 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]
inst_6 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
simp_rw : Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) 0) 0
simp_rw₁ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := 0 } : S⟮X⟯)
    ({ toFractionRing := 0 } : S⟮X⟯)
simp_rw₂ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
    ({ toFractionRing := 0 } : S⟮X⟯)
simp_rw₃ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
    ({ toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
simp_rw₄ :
  {
      toFractionRing :=
        Localization.mk ((φ : (a : R[X]) → S[X]) 0)
          (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
            ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) ⋯) :
      S⟮X⟯ } =
    { toFractionRing := Localization.mk 0 1 }
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun 0 = 0
have simp_rw₅ : {
    toFractionRing :=
      Localization.mk 0
        (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
          ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) sorry) :
    S⟮X⟯ } =
  { toFractionRing := Localization.mk 0 1 }
Tactic: simp_rw [MonoidHom.toFun_eq_coe, ← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰),
        ← Localization.mk_zero (1 : S[X]⁰), map_apply_ofFractionRing_mk, map_zero,
        Localization.mk_eq_mk', IsLocalization.mk'_zero]
-- 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]
inst_6 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
simp_rw : Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) 0) 0
simp_rw₁ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := 0 } : S⟮X⟯)
    ({ toFractionRing := 0 } : S⟮X⟯)
simp_rw₂ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
    ({ toFractionRing := 0 } : S⟮X⟯)
simp_rw₃ :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
    ({ toFractionRing := Localization.mk 0 1 } : S⟮X⟯)
simp_rw₄ :
  {
      toFractionRing :=
        Localization.mk ((φ : (a : R[X]) → S[X]) 0)
          (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
            ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) ⋯) :
      S⟮X⟯ } =
    { toFractionRing := Localization.mk 0 1 }
simp_rw₅ :
  {
      toFractionRing :=
        Localization.mk 0
          (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
            ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) ⋯) :
      S⟮X⟯ } =
    { toFractionRing := Localization.mk 0 1 }
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun 0 = 0
have simp_rw₆ : Eq (α := S⟮X⟯)
  ({
      toFractionRing :=
        IsLocalization.mk' (Localization (M := S[X]) S[X]⁰) 0
          (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
            ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) sorry) } :
    S⟮X⟯)
  ({ toFractionRing := IsLocalization.mk' (R := S[X]) (M := S[X]⁰) (Localization (M := S[X]) S[X]⁰) 0 1 } : S⟮X⟯)
Tactic: simp_rw [MonoidHom.toFun_eq_coe, ← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰),
        ← Localization.mk_zero (1 : S[X]⁰), map_apply_ofFractionRing_mk, map_zero,
        Localization.mk_eq_mk', IsLocalization.mk'_zero]
-- 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]
inst_6 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
x y : FractionRing R[X]
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun ({ toFractionRing := x : R⟮X⟯ } + { toFractionRing := y : R⟮X⟯ }) =
    (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := x : R⟮X⟯ } +
      (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := y : R⟮X⟯ }
have H : ∀ (y_1 : R[X] × ↥R[X]⁰),
  (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun
      ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } + { toFractionRing := y : R⟮X⟯ }) =
    (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } +
      (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := y : R⟮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
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]
inst_6 : RingHomClass.{u_5, u_3, u_4} F R[X] S[X]
φ : F
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ S[X]⁰)
y : FractionRing R[X]
y_1 : R[X] × ↥R[X]⁰
⊢ (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun
      ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } + { toFractionRing := y : R⟮X⟯ }) =
    (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } +
      (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := y : R⟮X⟯ }
have H : ∀ (y : R[X] × ↥R[X]⁰),
  (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun
      ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } +
        { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ }) =
    (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } +
      (↑(map φ hφ) : OneHom R⟮X⟯ S⟮X⟯).toFun { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ }
Tactic: induction y using Localization.induction_on
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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
f : R⟮X⟯
p q p' q' : R[X]
hq : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q
hq' : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q'
h : q' * p = q * p'
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
have inl : Subsingleton R →
  Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
f : R⟮X⟯
p q p' q' : R[X]
hq : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q
hq' : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q'
h : q' * p = q * p'
inl :
  Subsingleton R →
    Eq.{u_1 + 1} (α := G₀)
      ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        p q)
      ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        p' q')
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
have inr : Nontrivial R →
  Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
f : R⟮X⟯
p q p' q' : R[X]
hq : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q
hq' : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q'
h : q' * p = q * p'
h_1 : Subsingleton R
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
have inl : Eq.{u_1 + 1} (α := G₀)
  ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q q)
  ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
    q')
Tactic: rw [Subsingleton.elim p q, Subsingleton.elim p' q, Subsingleton.elim q' 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
f : R⟮X⟯
p q p' q' : R[X]
hq : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q
hq' : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q'
h : q' * p = q * p'
h_1 : Subsingleton R
inl :
  Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
have inl₁ : Eq.{u_1 + 1} (α := G₀)
  ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q q)
  ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q
    q')
Tactic: rw [Subsingleton.elim p q, Subsingleton.elim p' q, Subsingleton.elim q' 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
f : R⟮X⟯
p q p' q' : R[X]
hq : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q
hq' : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q'
h : q' * p = q * p'
h_1 : Subsingleton R
inl :
  Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
inl₁ :
  Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q
      q')
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
have inl₂ : Eq.{u_1 + 1} (α := G₀)
  ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q q)
  ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) q q)
Tactic: rw [Subsingleton.elim p q, Subsingleton.elim p' q, Subsingleton.elim q' 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
f : R⟮X⟯
p q p' q' : R[X]
hq : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q
hq' : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q'
h : q' * p = q * p'
h_1 : Nontrivial R
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
have inr : Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) q : G₀) (0 : G₀)
Tactic: rw [div_eq_div_iff, ← map_mul, mul_comm p, h, map_mul, mul_comm]
-- 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
f : R⟮X⟯
p q p' q' : R[X]
hq : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q
hq' : Membership.mem (γ := Submonoid R[X]) R[X]⁰ q'
h : q' * p = q * p'
h_1 : Nontrivial R
inr : Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) q : G₀) (0 : G₀)
⊢ Eq.{u_1 + 1} (α := G₀)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p
      q)
    ((fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) p'
      q')
have inr₁ : Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) q' : G₀) (0 : G₀)
Tactic: rw [div_eq_div_iff, ← map_mul, mul_comm p, h, map_mul, mul_comm]
-- 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
⊢ Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) 0
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    0
have simp_rw : Eq.{u_1 + 1} (α := G₀)
  (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := 0 }
    (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) sorry)
  0
Tactic: simp_rw [← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰), liftOn_ofFractionRing_mk,
      map_zero, zero_div]