awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst_2 : Field L
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : CommSemiring S
inst_6 : Algebra.{u_3, u} S K[X]
inst_7 : Algebra S L
inst_8 : Algebra.{u_3, u_2} S R[X]
φ : AlgHom.{u_3, u, u_1} S K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
r : S
simp_rw :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom φ.toRingHom hφ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₁ :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom (↑φ : K[X] →+* L) ⋯ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
    ((algebraMap S L : (a : S) → L) r : L)
⊢ (↑(↑(liftRingHom φ.toRingHom hφ) : K⟮X⟯ →* L) : OneHom K⟮X⟯ L).toFun ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r) =
    (algebraMap S L : (a : S) → L) r
have simp_rw₂ : Eq.{u_1 + 1} (α := L)
  ((liftRingHom (↑φ : K[X] →+* L) sorry : (a : K⟮X⟯) → L)
      (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((algebraMap S K[X] : (a : S) → K[X]) r) : K⟮X⟯)
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1 : K⟮X⟯)) :
    L)
  ((algebraMap S L : (a : S) → L) r : L)
Tactic: simp_rw [RingHom.toFun_eq_coe, AlgHom.toRingHom_eq_coe, algebraMap_apply r,
        liftRingHom_apply_div, AlgHom.coe_toRingHom, map_one, div_one, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst_2 : Field L
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : CommSemiring S
inst_6 : Algebra.{u_3, u} S K[X]
inst_7 : Algebra S L
inst_8 : Algebra.{u_3, u_2} S R[X]
φ : AlgHom.{u_3, u, u_1} S K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
r : S
simp_rw :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom φ.toRingHom hφ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₁ :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom (↑φ : K[X] →+* L) ⋯ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₂ :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom (↑φ : K[X] →+* L) ⋯ : (a : K⟮X⟯) → L)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((algebraMap S K[X] : (a : S) → K[X]) r) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1 : K⟮X⟯)) :
      L)
    ((algebraMap S L : (a : S) → L) r : L)
⊢ (↑(↑(liftRingHom φ.toRingHom hφ) : K⟮X⟯ →* L) : OneHom K⟮X⟯ L).toFun ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r) =
    (algebraMap S L : (a : S) → L) r
have simp_rw₃ : HDiv.hDiv (α := L) (β := L) (((↑φ : K[X] →+* L) : (a : K[X]) → L) ((algebraMap S K[X] : (a : S) → K[X]) r : K[X]) : L)
    (((↑φ : K[X] →+* L) : (a : K[X]) → L) 1 : L) =
  (algebraMap S L : (a : S) → L) r
Tactic: simp_rw [RingHom.toFun_eq_coe, AlgHom.toRingHom_eq_coe, algebraMap_apply r,
        liftRingHom_apply_div, AlgHom.coe_toRingHom, map_one, div_one, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst_2 : Field L
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : CommSemiring S
inst_6 : Algebra.{u_3, u} S K[X]
inst_7 : Algebra S L
inst_8 : Algebra.{u_3, u_2} S R[X]
φ : AlgHom.{u_3, u, u_1} S K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
r : S
simp_rw :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom φ.toRingHom hφ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₁ :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom (↑φ : K[X] →+* L) ⋯ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₂ :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom (↑φ : K[X] →+* L) ⋯ : (a : K⟮X⟯) → L)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((algebraMap S K[X] : (a : S) → K[X]) r) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1 : K⟮X⟯)) :
      L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₃ :
  HDiv.hDiv (α := L) (β := L) (((↑φ : K[X] →+* L) : (a : K[X]) → L) ((algebraMap S K[X] : (a : S) → K[X]) r : K[X]) : L)
      (((↑φ : K[X] →+* L) : (a : K[X]) → L) 1 : L) =
    (algebraMap S L : (a : S) → L) r
⊢ (↑(↑(liftRingHom φ.toRingHom hφ) : K⟮X⟯ →* L) : OneHom K⟮X⟯ L).toFun ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r) =
    (algebraMap S L : (a : S) → L) r
have simp_rw₄ : HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) ((algebraMap S K[X] : (a : S) → K[X]) r : K[X]) : L)
    ((φ : (a : K[X]) → L) 1 : L) =
  (algebraMap S L : (a : S) → L) r
Tactic: simp_rw [RingHom.toFun_eq_coe, AlgHom.toRingHom_eq_coe, algebraMap_apply r,
        liftRingHom_apply_div, AlgHom.coe_toRingHom, map_one, div_one, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst_2 : Field L
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : CommSemiring S
inst_6 : Algebra.{u_3, u} S K[X]
inst_7 : Algebra S L
inst_8 : Algebra.{u_3, u_2} S R[X]
φ : AlgHom.{u_3, u, u_1} S K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
r : S
simp_rw :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom φ.toRingHom hφ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₁ :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom (↑φ : K[X] →+* L) ⋯ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₂ :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom (↑φ : K[X] →+* L) ⋯ : (a : K⟮X⟯) → L)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((algebraMap S K[X] : (a : S) → K[X]) r) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1 : K⟮X⟯)) :
      L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₃ :
  HDiv.hDiv (α := L) (β := L) (((↑φ : K[X] →+* L) : (a : K[X]) → L) ((algebraMap S K[X] : (a : S) → K[X]) r : K[X]) : L)
      (((↑φ : K[X] →+* L) : (a : K[X]) → L) 1 : L) =
    (algebraMap S L : (a : S) → L) r
simp_rw₄ :
  HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) ((algebraMap S K[X] : (a : S) → K[X]) r : K[X]) : L)
      ((φ : (a : K[X]) → L) 1 : L) =
    (algebraMap S L : (a : S) → L) r
⊢ (↑(↑(liftRingHom φ.toRingHom hφ) : K⟮X⟯ →* L) : OneHom K⟮X⟯ L).toFun ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r) =
    (algebraMap S L : (a : S) → L) r
have simp_rw₅ : HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) ((algebraMap S K[X] : (a : S) → K[X]) r : K[X]) : L) (1 : L) =
  (algebraMap S L : (a : S) → L) r
Tactic: simp_rw [RingHom.toFun_eq_coe, AlgHom.toRingHom_eq_coe, algebraMap_apply r,
        liftRingHom_apply_div, AlgHom.coe_toRingHom, map_one, div_one, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst_2 : Field L
inst_3 : CommRing R
inst_4 : IsDomain R
inst_5 : CommSemiring S
inst_6 : Algebra.{u_3, u} S K[X]
inst_7 : Algebra S L
inst_8 : Algebra.{u_3, u_2} S R[X]
φ : AlgHom.{u_3, u, u_1} S K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
r : S
simp_rw :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom φ.toRingHom hφ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₁ :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom (↑φ : K[X] →+* L) ⋯ : (a : K⟮X⟯) → L) ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r : K⟮X⟯) : L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₂ :
  Eq.{u_1 + 1} (α := L)
    ((liftRingHom (↑φ : K[X] →+* L) ⋯ : (a : K⟮X⟯) → L)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((algebraMap S K[X] : (a : S) → K[X]) r) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) 1 : K⟮X⟯)) :
      L)
    ((algebraMap S L : (a : S) → L) r : L)
simp_rw₃ :
  HDiv.hDiv (α := L) (β := L) (((↑φ : K[X] →+* L) : (a : K[X]) → L) ((algebraMap S K[X] : (a : S) → K[X]) r : K[X]) : L)
      (((↑φ : K[X] →+* L) : (a : K[X]) → L) 1 : L) =
    (algebraMap S L : (a : S) → L) r
simp_rw₄ :
  HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) ((algebraMap S K[X] : (a : S) → K[X]) r : K[X]) : L)
      ((φ : (a : K[X]) → L) 1 : L) =
    (algebraMap S L : (a : S) → L) r
simp_rw₅ :
  HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) ((algebraMap S K[X] : (a : S) → K[X]) r : K[X]) : L) (1 : L) =
    (algebraMap S L : (a : S) → L) r
⊢ (↑(↑(liftRingHom φ.toRingHom hφ) : K⟮X⟯ →* L) : OneHom K⟮X⟯ L).toFun ((algebraMap S K⟮X⟯ : (a : S) → K⟮X⟯) r) =
    (algebraMap S L : (a : S) → L) r
have simp_rw₆ : Eq.{u_1 + 1} (α := L) ((φ : (a : K[X]) → L) ((algebraMap S K[X] : (a : S) → K[X]) r : K[X]) : L)
  ((algebraMap S L : (a : S) → L) r : L)
Tactic: simp_rw [RingHom.toFun_eq_coe, AlgHom.toRingHom_eq_coe, algebraMap_apply r,
        liftRingHom_apply_div, AlgHom.coe_toRingHom, map_one, div_one, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
y : ↥K[X]⁰
⊢ IsUnit (M := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (↑y : K[X]) : K⟮X⟯)
have rw : IsUnit.{u} (M := K⟮X⟯)
  { toFractionRing := (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑y : K[X]) }
Tactic: rw [← ofFractionRing_algebraMap]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
z : FractionRing K[X]
⊢ ∃ (x : K[X] × ↥K[X]⁰),
    HMul.hMul (β := K⟮X⟯) { toFractionRing := z : K⟮X⟯ }
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (↑x.2 : K[X]) : K⟮X⟯) =
      (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.1
have h : ∀ (x : K[X] × ↥K[X]⁰),
  HMul.hMul (β := K⟮X⟯) { toFractionRing := z : K⟮X⟯ }
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (↑x.2 : K[X]) : K⟮X⟯) =
      (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x.1 ↔
    HMul.hMul (β := FractionRing K[X]) z
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑x.2 : K[X]) : FractionRing K[X]) =
      (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) x.1
Tactic: convert! IsLocalization.surj K[X]⁰ z
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x y : K[X]
⊢ Eq (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) y : K⟮X⟯) →
    ∃ (c : ↥K[X]⁰), (↑c : K[X]) * x = (↑c : K[X]) * y
have rw : Eq.{u + 1} (α := K⟮X⟯) { toFractionRing := (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) x }
    { toFractionRing := (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) y } →
  ∃ (c : ↥K[X]⁰), (↑c : K[X]) * x = (↑c : K[X]) * y
Tactic: rw [← ofFractionRing_algebraMap, ← ofFractionRing_algebraMap]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]} (_hq : q ≠ 0) (_hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q'
H :
  ∀ {p q p' q' : K[X]} (_hq : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q)
    (_hq' : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q'), q' * p = q * p' → f p q = f p' q'
⊢ (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).liftOn
      f @H =
    f p q
have rw : (RatFunc.mk p q).liftOn f @H = f p q
Tactic: rw [← mk_eq_div, liftOn_mk _ _ f f0 @H']
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]} (_hq : q ≠ 0) (_hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q'
H :
  ∀ {p q p' q' : K[X]} (_hq : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q)
    (_hq' : Membership.mem (γ := Submonoid K[X]) K[X]⁰ q'), q' * p = q * p' → f p q = f p' q'
rw : (RatFunc.mk p q).liftOn f @H = f p q
⊢ (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).liftOn
      f @H =
    f p q
have rw₁ : f p q = f p q
Tactic: rw [← mk_eq_div, liftOn_mk _ _ f f0 @H']
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]} (_hq : q ≠ 0) (_ha : a ≠ 0), f (a * p) (a * q) = f p q
⊢ (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)).liftOn'
      f @H =
    f p q
have rw : ∀ {p q p' q' : K[X]} (_hq : q ≠ 0) (_hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q'
Tactic: rw [RatFunc.liftOn', liftOn_div _ _ _ f0]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x : K[X]
y : ↥K[X]⁰
⊢ Eq (α := K⟮X⟯) { toFractionRing := IsLocalization.mk' (FractionRing K[X]) x y } (IsLocalization.mk' K⟮X⟯ x y)
have rw : {
    toFractionRing :=
      HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) x : FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑y : K[X]) : FractionRing K[X]) :
    K⟮X⟯ } =
  IsLocalization.mk' K⟮X⟯ x y
Tactic: rw [IsFractionRing.mk'_eq_div, IsFractionRing.mk'_eq_div, ← mk_eq_div', ← mk_eq_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x : K[X]
y : ↥K[X]⁰
rw :
  {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) x : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑y : K[X]) : FractionRing K[X]) :
      K⟮X⟯ } =
    IsLocalization.mk' K⟮X⟯ x y
⊢ Eq (α := K⟮X⟯) { toFractionRing := IsLocalization.mk' (FractionRing K[X]) x y } (IsLocalization.mk' K⟮X⟯ x y)
have rw₁ : {
    toFractionRing :=
      HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) x : FractionRing K[X])
        ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑y : K[X]) : FractionRing K[X]) :
    K⟮X⟯ } =
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (↑y : K[X]) : K⟮X⟯)
Tactic: rw [IsFractionRing.mk'_eq_div, IsFractionRing.mk'_eq_div, ← mk_eq_div', ← mk_eq_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x : K[X]
y : ↥K[X]⁰
rw :
  {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) x : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑y : K[X]) : FractionRing K[X]) :
      K⟮X⟯ } =
    IsLocalization.mk' K⟮X⟯ x y
rw₁ :
  {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) x : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑y : K[X]) : FractionRing K[X]) :
      K⟮X⟯ } =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (↑y : K[X]) : K⟮X⟯)
⊢ Eq (α := K⟮X⟯) { toFractionRing := IsLocalization.mk' (FractionRing K[X]) x y } (IsLocalization.mk' K⟮X⟯ x y)
have rw₂ : RatFunc.mk x (↑y : K[X]) =
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x : K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (↑y : K[X]) : K⟮X⟯)
Tactic: rw [IsFractionRing.mk'_eq_div, IsFractionRing.mk'_eq_div, ← mk_eq_div', ← mk_eq_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x : K[X]
y : ↥K[X]⁰
rw :
  {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) x : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑y : K[X]) : FractionRing K[X]) :
      K⟮X⟯ } =
    IsLocalization.mk' K⟮X⟯ x y
rw₁ :
  {
      toFractionRing :=
        HDiv.hDiv (α := FractionRing K[X]) (β := FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) x : FractionRing K[X])
          ((algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑y : K[X]) : FractionRing K[X]) :
      K⟮X⟯ } =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (↑y : K[X]) : K⟮X⟯)
rw₂ :
  RatFunc.mk x (↑y : K[X]) =
    HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (↑y : K[X]) : K⟮X⟯)
⊢ Eq (α := K⟮X⟯) { toFractionRing := IsLocalization.mk' (FractionRing K[X]) x y } (IsLocalization.mk' K⟮X⟯ x y)
have rw₃ : RatFunc.mk x (↑y : K[X]) = RatFunc.mk x (↑y : K[X])
Tactic: rw [IsFractionRing.mk'_eq_div, IsFractionRing.mk'_eq_div, ← mk_eq_div', ← mk_eq_div]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Eq (α := FractionRing K[X] ≃+* K⟮X⟯) (RingEquiv.symm (toFractionRingRingEquiv K))
    (AlgEquiv.toRingEquiv (R := K[X]) (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) K⟮X⟯))
have h : ∀ (x : FractionRing K[X]),
  Eq (α := K⟮X⟯) ((RingEquiv.symm (toFractionRingRingEquiv K) : (a : FractionRing K[X]) → K⟮X⟯) x : K⟮X⟯)
    ((AlgEquiv.toRingEquiv (R := K[X]) (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) K⟮X⟯) :
          (a : FractionRing K[X]) → K⟮X⟯)
        x :
      K⟮X⟯)
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
⊢ Module.rank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.rank k K
have rw : Module.rank.{u_3, u_4} k[X] K[X] = Module.rank k K
Tactic: rw [Algebra.IsAlgebraic.rank_of_isFractionRing k[X] k⟮X⟯ K[X] K⟮X⟯,
    rank_polynomial_polynomial]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
rw : Module.rank.{u_3, u_4} k[X] K[X] = Module.rank k K
⊢ Module.rank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.rank k K
have rw₁ : Module.rank k K = Module.rank k K
Tactic: rw [Algebra.IsAlgebraic.rank_of_isFractionRing k[X] k⟮X⟯ K[X] K⟮X⟯,
    rank_polynomial_polynomial]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
⊢ Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K
have pos : ∀ (hf : Module.Finite.{u_3, u_4} k⟮X⟯ K⟮X⟯), Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K
Tactic: by_cases hf : Module.Finite k⟮X⟯ K⟮X⟯
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
pos : ∀ (hf : Module.Finite.{u_3, u_4} k⟮X⟯ K⟮X⟯), Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K
⊢ Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K
have neg : ∀ (hf : ¬Module.Finite.{u_3, u_4} k⟮X⟯ K⟮X⟯), Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K
Tactic: by_cases hf : Module.Finite k⟮X⟯ K⟮X⟯
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
hf : Module.Finite.{u_3, u_4} k⟮X⟯ K⟮X⟯
⊢ Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K
have hrank : Module.rank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.rank k K
Tactic: have hrank := rank_ratFunc_ratFunc k K
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
hf : Module.Finite.{u_3, u_4} k⟮X⟯ K⟮X⟯
hrank : Module.rank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.rank k K
⊢ Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K
have hrank₁ : (↑(Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯) : Cardinal.{u_4}) = Module.rank k K
Tactic: rw [← Module.finrank_eq_rank] at hrank
Cleared hypotheses: hrank
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
hf : ¬Module.Finite.{u_3, u_4} k⟮X⟯ K⟮X⟯
⊢ ¬Module.Finite k K
have rwa : ¬Module.rank k K < Cardinal.aleph0
Tactic: rwa [← Module.rank_lt_aleph0_iff, ← rank_ratFunc_ratFunc, Module.rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
hf : ¬Module.Finite.{u_3, u_4} k⟮X⟯ K⟮X⟯
rwa : ¬Module.rank k K < Cardinal.aleph0
⊢ ¬Module.Finite k K
have rwa₁ : ¬Module.rank.{u_3, u_4} k⟮X⟯ K⟮X⟯ < Cardinal.aleph0
Tactic: rwa [← Module.rank_lt_aleph0_iff, ← rank_ratFunc_ratFunc, Module.rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (hypothesis)
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
hf : ¬Module.Finite.{u_3, u_4} k⟮X⟯ K⟮X⟯
⊢ Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K
have hf' : ¬Module.Finite k K
Tactic: have hf' : ¬ Module.Finite k K := by
      rwa [← Module.rank_lt_aleph0_iff, ← rank_ratFunc_ratFunc, Module.rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
hf : ¬Module.Finite.{u_3, u_4} k⟮X⟯ K⟮X⟯
hf' : ¬Module.Finite k K
⊢ Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K
have neg : 0 = Module.finrank k K
Tactic: rw [Module.finrank_of_not_finite hf, Module.finrank_of_not_finite hf']
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Basic (goal)
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
hf : ¬Module.Finite.{u_3, u_4} k⟮X⟯ K⟮X⟯
hf' : ¬Module.Finite k K
neg : 0 = Module.finrank k K
⊢ Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K
have neg₁ : Eq (α := ℕ) 0 0
Tactic: rw [Module.finrank_of_not_finite hf, Module.finrank_of_not_finite hf']