awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
frac_tac :
  ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
    ({ toFractionRing := toFractionRing : K⟮X⟯ } + b) * c = { toFractionRing := toFractionRing : K⟮X⟯ } * c + b * c
⊢ ∀ (a b c : K⟮X⟯), (a + b) * c = a * c + b * c
have frac_tac₁ : ∀ (toFractionRing toFractionRing_1 : FractionRing K[X]) (c : K⟮X⟯),
  ({ toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing_1 : K⟮X⟯ }) * c =
    { toFractionRing := toFractionRing : K⟮X⟯ } * c + { toFractionRing := toFractionRing_1 : K⟮X⟯ } * c
Tactic: frac_tac
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
frac_tac :
  ∀ (toFractionRing : FractionRing K[X]) (b c : K⟮X⟯),
    ({ toFractionRing := toFractionRing : K⟮X⟯ } + b) * c = { toFractionRing := toFractionRing : K⟮X⟯ } * c + b * c
frac_tac₁ :
  ∀ (toFractionRing toFractionRing_1 : FractionRing K[X]) (c : K⟮X⟯),
    ({ toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing_1 : K⟮X⟯ }) * c =
      { toFractionRing := toFractionRing : K⟮X⟯ } * c + { toFractionRing := toFractionRing_1 : K⟮X⟯ } * c
⊢ ∀ (a b c : K⟮X⟯), (a + b) * c = a * c + b * c
have frac_tac₂ : ∀ (toFractionRing toFractionRing_1 toFractionRing_2 : FractionRing K[X]),
  ({ toFractionRing := toFractionRing : K⟮X⟯ } + { toFractionRing := toFractionRing_1 : K⟮X⟯ }) *
      { toFractionRing := toFractionRing_2 : K⟮X⟯ } =
    { toFractionRing := toFractionRing : K⟮X⟯ } * { toFractionRing := toFractionRing_2 : K⟮X⟯ } +
      { toFractionRing := toFractionRing_1 : K⟮X⟯ } * { toFractionRing := toFractionRing_2 : K⟮X⟯ }
Tactic: frac_tac
-- 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 : 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]⁰)
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_4 + 1} (α := S⟮X⟯)
    ((fun (n d : R[X]) ↦
        (if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              toFractionRing :=
                Localization.mk ((φ : (a : R[X]) → S[X]) n)
                  (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                    ((φ : (a : R[X]) → S[X]) d) h) }
          else 0 :
          S⟮X⟯))
      p q)
    ((fun (n d : R[X]) ↦
        (if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              toFractionRing :=
                Localization.mk ((φ : (a : R[X]) → S[X]) n)
                  (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                    ((φ : (a : R[X]) → S[X]) d) h) }
          else 0 :
          S⟮X⟯))
      p' q')
have simp : (Localization.r S[X]⁰ : (a : S[X] × ↥S[X]⁰) → S[X] × ↥S[X]⁰ → Prop)
  (((φ : (a : R[X]) → S[X]) p,
      Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q) sorry) :
    S[X] × ↥S[X]⁰)
  ((φ : (a : R[X]) → S[X]) p',
    Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q') sorry)
Tactic: simp only [Submonoid.mem_comap.mp (hφ hq), Submonoid.mem_comap.mp (hφ hq'),
        dif_pos, ofFractionRing.injEq, Localization.mk_eq_mk_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]
inst_6 : 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]⁰)
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'
⊢ (Localization.r S[X]⁰ : (a : S[X] × ↥S[X]⁰) → S[X] × ↥S[X]⁰ → Prop)
    (((φ : (a : R[X]) → S[X]) p,
        Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q) ⋯) :
      S[X] × ↥S[X]⁰)
    ((φ : (a : R[X]) → S[X]) p',
      Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q') ⋯)
have refine : HMul.hMul (α := S[X]) (β := S[X])
    ((↑((φ : (a : R[X]) → S[X]) p',
              Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                ((φ : (a : R[X]) → S[X]) q') sorry).2 :
        S[X]) :
      S[X])
    (((φ : (a : R[X]) → S[X]) p,
          Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q)
            sorry).1 :
      S[X]) =
  HMul.hMul (α := S[X]) (β := S[X])
    ((↑((φ : (a : R[X]) → S[X]) p,
              Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                ((φ : (a : R[X]) → S[X]) q) sorry).2 :
        S[X]) :
      S[X])
    (((φ : (a : R[X]) → S[X]) p',
          Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) q')
            sorry).1 :
      S[X])
Tactic: refine Localization.r_of_eq ?_
-- 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 : 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]⁰)
⊢ Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) 1
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯)
    1
have simp_rw : Eq.{u_4 + 1} (α := S⟮X⟯)
  (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) { toFractionRing := 1 }
    (fun (n d : R[X]) ↦
      if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
        {
          toFractionRing :=
            Localization.mk ((φ : (a : R[X]) → S[X]) n)
              (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                ((φ : (a : R[X]) → S[X]) d) h) }
      else 0)
    sorry)
  { toFractionRing := 1 }
Tactic: simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, OneMemClass.one_mem, dite_true, ofFractionRing.injEq,
      Localization.mk_one, Localization.mk_eq_monoidOf_mk', Submonoid.LocalizationMap.mk'_self]
-- 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 : 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]⁰)
simp_rw :
  Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) { toFractionRing := 1 }
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯)
    { toFractionRing := 1 }
⊢ Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) 1
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯)
    1
have simp_rw₁ : Eq.{u_4 + 1} (α := S⟮X⟯)
  (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) { toFractionRing := Localization.mk 1 1 }
    (fun (n d : R[X]) ↦
      if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
        {
          toFractionRing :=
            Localization.mk ((φ : (a : R[X]) → S[X]) n)
              (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                ((φ : (a : R[X]) → S[X]) d) h) }
      else 0)
    sorry)
  { toFractionRing := Localization.mk 1 1 }
Tactic: simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, OneMemClass.one_mem, dite_true, ofFractionRing.injEq,
      Localization.mk_one, Localization.mk_eq_monoidOf_mk', Submonoid.LocalizationMap.mk'_self]
-- 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 : 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]⁰)
simp_rw :
  Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) { toFractionRing := 1 }
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯)
    { toFractionRing := 1 }
simp_rw₁ :
  Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) { toFractionRing := Localization.mk 1 1 }
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯)
    { toFractionRing := Localization.mk 1 1 }
⊢ Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) 1
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯)
    1
have simp_rw₂ : Eq.{u_4 + 1} (α := S⟮X⟯)
  (if h : Membership.mem (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) then
    {
      toFractionRing :=
        Localization.mk ((φ : (a : R[X]) → S[X]) 1)
          (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
            ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) h) }
  else 0)
  { toFractionRing := Localization.mk 1 1 }
Tactic: simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, OneMemClass.one_mem, dite_true, ofFractionRing.injEq,
      Localization.mk_one, Localization.mk_eq_monoidOf_mk', Submonoid.LocalizationMap.mk'_self]
-- 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 : 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]⁰)
simp_rw :
  Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) { toFractionRing := 1 }
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯)
    { toFractionRing := 1 }
simp_rw₁ :
  Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) { toFractionRing := Localization.mk 1 1 }
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯)
    { toFractionRing := Localization.mk 1 1 }
simp_rw₂ :
  Eq.{u_4 + 1} (α := S⟮X⟯)
    (if h : Membership.mem (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) then
      {
        toFractionRing :=
          Localization.mk ((φ : (a : R[X]) → S[X]) 1)
            (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
              ((φ : (a : R[X]) → S[X]) (↑1 : R[X])) h) }
    else 0)
    { toFractionRing := Localization.mk 1 1 }
⊢ Eq.{u_4 + 1} (α := S⟮X⟯)
    (RatFunc.liftOn.{u_3, u_4 + 1} (K := R) 1
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯)
    1
have simp_rw₃ : Eq.{u_4 + 1} (α := S⟮X⟯)
  (if h : Membership.mem (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) 1) then
    {
      toFractionRing :=
        Localization.mk ((φ : (a : R[X]) → S[X]) 1)
          (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x) ((φ : (a : R[X]) → S[X]) 1)
            sorry) }
  else 0)
  { toFractionRing := Localization.mk 1 1 }
Tactic: simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, OneMemClass.one_mem, dite_true, ofFractionRing.injEq,
      Localization.mk_one, Localization.mk_eq_monoidOf_mk', Submonoid.LocalizationMap.mk'_self]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
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 : 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]⁰)
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ ({ toFractionRing := Localization.mk (p, q).1 (p, q).2 : R⟮X⟯ } *
          { toFractionRing := Localization.mk (p', q').1 (p', q').2 : R⟮X⟯ }).liftOn
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯ =
    HMul.hMul (α := S⟮X⟯)
      ({ toFractionRing := Localization.mk (p, q).1 (p, q).2 : R⟮X⟯ }.liftOn
        (fun (n d : R[X]) ↦
          if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              toFractionRing :=
                Localization.mk ((φ : (a : R[X]) → S[X]) n)
                  (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                    ((φ : (a : R[X]) → S[X]) d) h) :
              S⟮X⟯ }
          else 0)
        ⋯)
      ({ toFractionRing := Localization.mk (p', q').1 (p', q').2 : R⟮X⟯ }.liftOn
        (fun (n d : R[X]) ↦
          if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              toFractionRing :=
                Localization.mk ((φ : (a : R[X]) → S[X]) n)
                  (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                    ((φ : (a : R[X]) → S[X]) d) h) :
              S⟮X⟯ }
          else 0)
        ⋯)
have hq : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q : R[X]) : S[X])
Tactic: have hq : φ q ∈ S[X]⁰ := hφ q.prop
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
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 : 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]⁰)
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q : R[X]) : S[X])
⊢ ({ toFractionRing := Localization.mk (p, q).1 (p, q).2 : R⟮X⟯ } *
          { toFractionRing := Localization.mk (p', q').1 (p', q').2 : R⟮X⟯ }).liftOn
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯ =
    HMul.hMul (α := S⟮X⟯)
      ({ toFractionRing := Localization.mk (p, q).1 (p, q).2 : R⟮X⟯ }.liftOn
        (fun (n d : R[X]) ↦
          if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              toFractionRing :=
                Localization.mk ((φ : (a : R[X]) → S[X]) n)
                  (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                    ((φ : (a : R[X]) → S[X]) d) h) :
              S⟮X⟯ }
          else 0)
        ⋯)
      ({ toFractionRing := Localization.mk (p', q').1 (p', q').2 : R⟮X⟯ }.liftOn
        (fun (n d : R[X]) ↦
          if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              toFractionRing :=
                Localization.mk ((φ : (a : R[X]) → S[X]) n)
                  (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                    ((φ : (a : R[X]) → S[X]) d) h) :
              S⟮X⟯ }
          else 0)
        ⋯)
have hq' : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q' : R[X]) : S[X])
Tactic: have hq' : φ q' ∈ S[X]⁰ := hφ q'.prop
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
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 : 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]⁰)
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q : R[X]) : S[X])
hq' : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑q' : R[X]) : S[X])
⊢ ({ toFractionRing := Localization.mk (p, q).1 (p, q).2 : R⟮X⟯ } *
          { toFractionRing := Localization.mk (p', q').1 (p', q').2 : R⟮X⟯ }).liftOn
      (fun (n d : R[X]) ↦
        if h : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
          {
            toFractionRing :=
              Localization.mk ((φ : (a : R[X]) → S[X]) n)
                (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                  ((φ : (a : R[X]) → S[X]) d) h) }
        else 0)
      ⋯ =
    HMul.hMul (α := S⟮X⟯)
      ({ toFractionRing := Localization.mk (p, q).1 (p, q).2 : R⟮X⟯ }.liftOn
        (fun (n d : R[X]) ↦
          if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              toFractionRing :=
                Localization.mk ((φ : (a : R[X]) → S[X]) n)
                  (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                    ((φ : (a : R[X]) → S[X]) d) h) :
              S⟮X⟯ }
          else 0)
        ⋯)
      ({ toFractionRing := Localization.mk (p', q').1 (p', q').2 : R⟮X⟯ }.liftOn
        (fun (n d : R[X]) ↦
          if h :
              Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) d : S[X]) then
            {
              toFractionRing :=
                Localization.mk ((φ : (a : R[X]) → S[X]) n)
                  (Subtype.mk (p := fun (x : S[X]) ↦ Membership.mem (γ := Submonoid S[X]) S[X]⁰ x)
                    ((φ : (a : R[X]) → S[X]) d) h) :
              S⟮X⟯ }
          else 0)
        ⋯)
have hqq' : Membership.mem.{u_4, u_4} (α := S[X]) (γ := Submonoid S[X]) S[X]⁰ ((φ : (a : R[X]) → S[X]) (↑(q * q') : R[X]) : S[X])
Tactic: have hqq' : φ ↑(q * q') ∈ S[X]⁰ := by simpa using Submonoid.mul_mem _ hq hq'
-- 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])
x y : FractionRing R[X]
h :
  Eq.{u_4 + 1} (α := S⟮X⟯) ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := x } : S⟮X⟯)
    ((map φ hφ : (a : R⟮X⟯) → S⟮X⟯) { toFractionRing := y } : S⟮X⟯)
⊢ { toFractionRing := x : R⟮X⟯ } = { toFractionRing := y }
have H : ∀ (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 }
Tactic: induction x using Localization.induction_on
Cleared hypotheses: x, h