awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀⁰)
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₀))
      ⋯)
    0
⊢ 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 := Localization.mk 0 1 }
    (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]
-- 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₀⁰)
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₀))
      ⋯)
    0
simp_rw₁ :
  Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := Localization.mk 0 1 }
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    0
⊢ 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₂ : HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) 0 : G₀) ((φ : (a : R[X]) → G₀) (↑1 : R[X]) : G₀) = 0
Tactic: simp_rw [← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰), liftOn_ofFractionRing_mk,
      map_zero, zero_div]
-- 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₀⁰)
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₀))
      ⋯)
    0
simp_rw₁ :
  Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := Localization.mk 0 1 }
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    0
simp_rw₂ : HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) 0 : G₀) ((φ : (a : R[X]) → G₀) (↑1 : R[X]) : G₀) = 0
⊢ 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₃ : HDiv.hDiv (α := G₀) (β := G₀) (0 : G₀) ((φ : (a : R[X]) → G₀) (↑1 : R[X]) : G₀) = 0
Tactic: simp_rw [← ofFractionRing_zero, ← Localization.mk_zero (1 : R[X]⁰), liftOn_ofFractionRing_mk,
      map_zero, zero_div]
-- 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) 1
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
have simp_rw : Eq.{u_1 + 1} (α := G₀)
  (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := 1 }
    (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) sorry)
  1
Tactic: simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, div_one]
-- 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₀⁰)
simp_rw :
  Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := 1 }
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
⊢ Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) 1
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
have simp_rw₁ : Eq.{u_1 + 1} (α := G₀)
  (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := Localization.mk 1 1 }
    (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) sorry)
  1
Tactic: simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, div_one]
-- 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₀⁰)
simp_rw :
  Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := 1 }
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
simp_rw₁ :
  Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := Localization.mk 1 1 }
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
⊢ Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) 1
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
have simp_rw₂ : HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) 1 : G₀) ((φ : (a : R[X]) → G₀) (↑1 : R[X]) : G₀) = 1
Tactic: simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, div_one]
-- 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₀⁰)
simp_rw :
  Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := 1 }
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
simp_rw₁ :
  Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := Localization.mk 1 1 }
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
simp_rw₂ : HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) 1 : G₀) ((φ : (a : R[X]) → G₀) (↑1 : R[X]) : G₀) = 1
⊢ Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) 1
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
have simp_rw₃ : HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) 1 : G₀) ((φ : (a : R[X]) → G₀) 1 : G₀) = 1
Tactic: simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, div_one]
-- 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₀⁰)
simp_rw :
  Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := 1 }
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
simp_rw₁ :
  Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) { toFractionRing := Localization.mk 1 1 }
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
simp_rw₂ : HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) 1 : G₀) ((φ : (a : R[X]) → G₀) (↑1 : R[X]) : G₀) = 1
simp_rw₃ : HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) 1 : G₀) ((φ : (a : R[X]) → G₀) 1 : G₀) = 1
⊢ Eq.{u_1 + 1} (α := G₀)
    (RatFunc.liftOn.{u_3, u_1 + 1} (K := R) 1
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯)
    1
have simp_rw₄ : 1 / 1 = 1
Tactic: simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, div_one]
-- 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₀⁰)
x y : R⟮X⟯
⊢ (x * y).liftOn
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯ =
    HMul.hMul (α := G₀)
      (x.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        ⋯)
      (y.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        ⋯)
have obtain : ∀ (x : FractionRing R[X]),
  ({ toFractionRing := x : R⟮X⟯ } * y).liftOn
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      sorry =
    HMul.hMul (α := G₀)
      ({ toFractionRing := x : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        sorry)
      (y.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        sorry)
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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
y : R⟮X⟯
x : FractionRing R[X]
⊢ ({ toFractionRing := x : R⟮X⟯ } * y).liftOn
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯ =
    HMul.hMul (α := G₀)
      ({ toFractionRing := x : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        ⋯)
      (y.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        ⋯)
have obtain : ∀ (y : FractionRing R[X]),
  ({ toFractionRing := x : R⟮X⟯ } * { toFractionRing := y : R⟮X⟯ }).liftOn
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      sorry =
    HMul.hMul (α := G₀)
      ({ toFractionRing := x : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        sorry)
      ({ toFractionRing := y : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        sorry)
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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
x y : FractionRing R[X]
⊢ ({ toFractionRing := x : R⟮X⟯ } * { toFractionRing := y : R⟮X⟯ }).liftOn
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯ =
    HMul.hMul (α := G₀)
      ({ toFractionRing := x : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        ⋯)
      ({ toFractionRing := y : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        ⋯)
have H : ∀ (y_1 : R[X] × ↥R[X]⁰),
  ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } * { toFractionRing := y : R⟮X⟯ }).liftOn
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      sorry =
    HMul.hMul (α := G₀)
      ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        sorry)
      ({ toFractionRing := y : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        sorry)
Tactic: cases 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]
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
y : FractionRing R[X]
y_1 : R[X] × ↥R[X]⁰
⊢ ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } * { toFractionRing := y : R⟮X⟯ }).liftOn
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯ =
    HMul.hMul (α := G₀)
      ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        ⋯)
      ({ toFractionRing := y : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        ⋯)
have H : ∀ (y : R[X] × ↥R[X]⁰),
  ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } *
          { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ }).liftOn
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      sorry =
    HMul.hMul (α := G₀)
      ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        sorry)
      ({ toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        sorry)
Tactic: cases 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₀⁰)
y y_1 : R[X] × ↥R[X]⁰
⊢ ({ toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ } *
          { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ }).liftOn
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      ⋯ =
    HMul.hMul (α := G₀)
      ({ toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        ⋯)
      ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ }.liftOn
        (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
        ⋯)
have H : { toFractionRing := Localization.mk (y.1 * y_1.1) (y.2 * y_1.2) : R⟮X⟯ }.liftOn
    (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀)) sorry =
  HMul.hMul (α := G₀)
    ({ toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ }.liftOn
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      sorry)
    ({ toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ }.liftOn
      (fun (p q : R[X]) ↦ HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) p : G₀) ((φ : (a : R[X]) → G₀) q : G₀))
      sorry)
Tactic: rw [← ofFractionRing_mul, Localization.mk_mul]
-- 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₀⁰)
x y : FractionRing R[X]
⊢ Eq.{u_1 + 1} (α := G₀) ((liftMonoidWithZeroHom φ hφ' : (a : R⟮X⟯) → G₀) { toFractionRing := x : R⟮X⟯ } : G₀)
      ((liftMonoidWithZeroHom φ hφ' : (a : R⟮X⟯) → G₀) { toFractionRing := y : R⟮X⟯ } : G₀) →
    { toFractionRing := x : R⟮X⟯ } = { toFractionRing := y }
have H : ∀ (y_1 : R[X] × ↥R[X]⁰),
  Eq.{u_1 + 1} (α := G₀)
      ((liftMonoidWithZeroHom φ hφ' : (a : R⟮X⟯) → G₀) { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } : G₀)
      ((liftMonoidWithZeroHom φ hφ' : (a : R⟮X⟯) → G₀) { toFractionRing := y : R⟮X⟯ } : G₀) →
    { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } = { toFractionRing := y }
Tactic: cases x using Localization.induction_on
Cleared hypotheses: x
-- 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 : FractionRing R[X]
y_1 : R[X] × ↥R[X]⁰
⊢ Eq.{u_1 + 1} (α := G₀)
      ((liftMonoidWithZeroHom φ hφ' : (a : R⟮X⟯) → G₀) { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } : G₀)
      ((liftMonoidWithZeroHom φ hφ' : (a : R⟮X⟯) → G₀) { toFractionRing := y : R⟮X⟯ } : G₀) →
    { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } = { toFractionRing := y }
have H : ∀ (a' : R[X] × ↥R[X]⁰),
  Eq.{u_1 + 1} (α := G₀)
      ((liftMonoidWithZeroHom φ hφ' : (a : R⟮X⟯) → G₀) { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } : G₀)
      ((liftMonoidWithZeroHom φ hφ' : (a : R⟮X⟯) → G₀) { toFractionRing := Localization.mk a'.1 a'.2 : R⟮X⟯ } : G₀) →
    { toFractionRing := Localization.mk y_1.1 y_1.2 : R⟮X⟯ } = { toFractionRing := Localization.mk a'.1 a'.2 }
Tactic: cases y using Localization.induction_on with | _ a'
Cleared hypotheses: y
-- 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]⁰
⊢ Eq.{u_1 + 1} (α := G₀)
      ((liftMonoidWithZeroHom φ hφ' : (a : R⟮X⟯) → G₀) { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ } : G₀)
      ((liftMonoidWithZeroHom φ hφ' : (a : R⟮X⟯) → G₀) { toFractionRing := Localization.mk a'.1 a'.2 : R⟮X⟯ } : G₀) →
    { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ } = { toFractionRing := Localization.mk a'.1 a'.2 }
have 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₀) →
  { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ } = { toFractionRing := Localization.mk a'.1 a'.2 }
Tactic: simp_rw [liftMonoidWithZeroHom_apply_ofFractionRing_mk]
-- 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₀)
⊢ { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ } = { toFractionRing := Localization.mk a'.1 a'.2 }
have H : Localization.mk y.1 y.2 = Localization.mk a'.1 a'.2
Tactic: congr 1
-- 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₀)
⊢ Localization.mk y.1 y.2 = Localization.mk a'.1 a'.2
have H : (↑(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: refine Localization.mk_eq_mk_iff.mpr (Localization.r_of_eq (M := R[X]) ?_)