awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
simp_rw₄ : 1 / 1 = 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

Tactic:
simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, div_one]

Premises used: RatFunc.liftOn_ofFractionRing_mk, OneMemClass.coe_one, RatFunc.ofFractionRing_one, map_one, Localization.mk_one, div_one
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯
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₀))
        ⋯ =
      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₀))
          ⋯)
⊢ (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₀))
        ⋯)

Tactic:
obtain ⟨x⟩ := x
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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]
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₀))
        ⋯ =
      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₀))
          ⋯)
⊢ ({ 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₀))
        ⋯)

Tactic:
obtain ⟨y⟩ := y
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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]
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₀))
        ⋯ =
      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₀))
          ⋯)
⊢ ({ 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₀))
        ⋯)

Tactic:
cases x using Localization.induction_on
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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]⁰
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₀))
        ⋯ =
      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 := 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⟯ } * { 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₀))
        ⋯)

Tactic:
cases y using Localization.induction_on
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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]⁰
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₀))
      ⋯ =
    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₀))
        ⋯)
⊢ ({ 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₀))
        ⋯)

Tactic:
rw [← ofFractionRing_mul, Localization.mk_mul]

Premises used: Localization.mk_mul, RatFunc.ofFractionRing_mul
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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_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₀))
      ⋯ =
    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₀))
        ⋯)

Tactic:
simp only [liftOn_ofFractionRing_mk, div_mul_div_comm, map_mul, Submonoid.coe_mul]

Premises used: RatFunc.liftOn_ofFractionRing_mk, div_mul_div_comm, map_mul, Submonoid.coe_mul
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
G₀ : Type u_1
R : Type u_3
inst : CommGroupWithZero G₀
inst_1 : CommRing R
φ : MonoidWithZeroHom.{u_3, u_1} R[X] G₀
hφ : LE.le (α := Submonoid R[X]) R[X]⁰ (Submonoid.comap φ G₀⁰)
n : R[X]
d : ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ hφ : (a : R⟮X⟯) → G₀) { toFractionRing := Localization.mk n d : R⟮X⟯ } =
    HDiv.hDiv (α := G₀) (β := G₀) ((φ : (a : R[X]) → G₀) n : G₀) ((φ : (a : R[X]) → G₀) (↑d : R[X]) : G₀)

Tactic:
liftOn_ofFractionRing_mk _ _ _ _

Premises used: RatFunc.liftOn_ofFractionRing_mk
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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]
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 }
⊢ 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 }

Tactic:
cases x using Localization.induction_on
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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]⁰
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 }
⊢ 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 y using Localization.induction_on with | _ a'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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 }
⊢ 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 }

Tactic:
simp_rw [liftMonoidWithZeroHom_apply_ofFractionRing_mk]

Premises used: RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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 : Localization.mk y.1 y.2 = Localization.mk a'.1 a'.2
⊢ { toFractionRing := Localization.mk y.1 y.2 : R⟮X⟯ } = { toFractionRing := Localization.mk a'.1 a'.2 }

Tactic:
congr 1
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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

Tactic:
Localization.mk_eq_mk_iff.mpr (Localization.r_of_eq (M := R[X]) ?_)

Premises used: Iff.mpr, Localization.r_of_eq, Localization.mk_eq_mk_iff
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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 : (↑(a'.1, a'.2).2 : R[X]) * (y.1, y.2).1 = (↑(y.1, y.2).2 : R[X]) * (a'.1, a'.2).1
⊢ Localization.mk y.1 y.2 = Localization.mk a'.1 a'.2

Tactic:
refine Localization.mk_eq_mk_iff.mpr (Localization.r_of_eq (M := R[X]) ?_)

Premises used: Iff.mpr, Localization.r_of_eq, Localization.mk_eq_mk_iff
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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₀)
H₂ : Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (↑a'.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

Tactic:
have := mul_eq_mul_of_div_eq_div _ _ ?_ ?_ h
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
H₄ H₅ H₆ 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
⊢ (↑(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

Premises used: Function.Injective.eq_iff, Prod.fst, map_mul, mul_comm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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₀)
⊢ Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) (0 : G₀)

Tactic:
map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _)

Premises used: SetLike.coe_mem, map_ne_zero_of_mem_nonZeroDivisors
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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₀)
⊢ Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (↑y.2 : R[X]) : G₀) (0 : G₀)

Tactic:
exact map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _)

Premises used: SetLike.coe_mem, map_ne_zero_of_mem_nonZeroDivisors
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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₀)
⊢ Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀) (0 : G₀)

Tactic:
map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _)

Premises used: SetLike.coe_mem, map_ne_zero_of_mem_nonZeroDivisors
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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₀)
⊢ Ne.{u_1 + 1} (α := G₀) ((φ : (a : R[X]) → G₀) (↑a'.2 : R[X]) : G₀) (0 : G₀)

Tactic:
exact map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _)

Premises used: SetLike.coe_mem, map_ne_zero_of_mem_nonZeroDivisors