awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
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)
⊢ (↑(↑(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

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]

Premises used: AlgHom.coe_toRingHom, RatFunc.liftRingHom_apply_div, RingHom.toFun_eq_coe, map_one, AlgHom.toRingHom_eq_coe, AlgHom.commutes, RatFunc.algebraMap_apply, div_one
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
S : Type u_3
inst_2 : Field L
inst_3 : CommSemiring S
inst_4 : Algebra.{u_3, u} S K[X]
inst_5 : Algebra S L
φ : AlgHom.{u_3, u, u_1} S K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
n : K[X]
d : ↥K[X]⁰
⊢ (liftAlgHom φ hφ : (a : K⟮X⟯) → L) { toFractionRing := Localization.mk n d : K⟮X⟯ } =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) n : L) ((φ : (a : K[X]) → L) (↑d : K[X]) : L)

Tactic:
liftMonoidWithZeroHom_apply_ofFractionRing_mk _ hφ _ _

Premises used: RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
S : Type u_3
inst_2 : Field L
inst_3 : CommSemiring S
inst_4 : Algebra.{u_3, u} S K[X]
inst_5 : Algebra S L
φ : AlgHom.{u_3, u, u_1} S K[X] L
hφ : Function.Injective.{u + 1, u_1 + 1} (α := K[X]) (β := L) (⇑φ : (a : K[X]) → L)
hφ' : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
⊢ Function.Injective.{u + 1, u_1 + 1} (α := K⟮X⟯) (β := L) (⇑(liftAlgHom φ hφ') : (a : K⟮X⟯) → L)

Tactic:
liftMonoidWithZeroHom_injective _ hφ

Premises used: nonZeroDivisors_le_comap_nonZeroDivisors_of_injective, RatFunc.liftMonoidWithZeroHom_injective
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
S : Type u_3
inst_2 : Field L
inst_3 : CommSemiring S
inst_4 : Algebra.{u_3, u} S K[X]
inst_5 : Algebra S L
φ : AlgHom.{u_3, u, u_1} S K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
p q : K[X]
⊢ HDiv.hDiv (α := L) (β := L)
      ((liftAlgHom φ hφ : (a : K⟮X⟯) → L) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) : L)
      ((liftAlgHom φ hφ : (a : K⟮X⟯) → L) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : L) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) q : L)

Tactic:
liftMonoidWithZeroHom_apply_div' _ hφ _ _

Premises used: RatFunc.liftMonoidWithZeroHom_apply_div'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
L : Type u_1
S : Type u_3
inst_2 : Field L
inst_3 : CommSemiring S
inst_4 : Algebra.{u_3, u} S K[X]
inst_5 : Algebra S L
φ : AlgHom.{u_3, u, u_1} S K[X] L
hφ : LE.le (α := Submonoid K[X]) K[X]⁰ (Submonoid.comap φ L⁰)
p q : K[X]
⊢ (liftAlgHom φ hφ : (a : K⟮X⟯) → L)
      (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⟯)) =
    HDiv.hDiv (α := L) (β := L) ((φ : (a : K[X]) → L) p : L) ((φ : (a : K[X]) → L) q : L)

Tactic:
liftMonoidWithZeroHom_apply_div _ hφ _ _

Premises used: RatFunc.liftMonoidWithZeroHom_apply_div
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
y : ↥K[X]⁰
rw :
  IsUnit.{u} (M := K⟮X⟯)
    { toFractionRing := (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑y : K[X]) }
⊢ IsUnit (M := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (↑y : K[X]) : K⟮X⟯)

Tactic:
rw [← ofFractionRing_algebraMap]

Premises used: RatFunc.ofFractionRing_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
y : ↥K[X]⁰
⊢ IsUnit.{u} (M := K⟮X⟯)
    { toFractionRing := (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑y : K[X]) }

Tactic:
(toFractionRingRingEquiv K).symm.toRingHom.isUnit_map (IsLocalization.map_units _ y)

Premises used: RingEquiv.toRingHom, RatFunc.toFractionRingRingEquiv, IsLocalization.map_units, RingHom.isUnit_map, RingEquiv.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
y : ↥K[X]⁰
⊢ IsUnit.{u} (M := K⟮X⟯)
    { toFractionRing := (algebraMap K[X] (FractionRing K[X]) : (a : K[X]) → FractionRing K[X]) (↑y : K[X]) }

Tactic:
exact (toFractionRingRingEquiv K).symm.toRingHom.isUnit_map (IsLocalization.map_units _ y)

Premises used: RingEquiv.toRingHom, RatFunc.toFractionRingRingEquiv, IsLocalization.map_units, RingHom.isUnit_map, RingEquiv.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
z : FractionRing K[X]
⊢ ∃ (x : K[X] × ↥K[X]⁰),
    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:
IsLocalization.surj K[X]⁰ z

Premises used: IsLocalization.surj, nonZeroDivisors, Polynomial
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
z : FractionRing K[X]
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
⊢ ∃ (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

Tactic:
convert! IsLocalization.surj K[X]⁰ z

Premises used: IsLocalization.surj, nonZeroDivisors, Polynomial
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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 ↔
    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:
simp only [← ofFractionRing_algebraMap, ← ofFractionRing_mul,
      ofFractionRing.injEq]

Premises used: RatFunc.ofFractionRing.injEq, RatFunc.ofFractionRing_algebraMap, RatFunc.ofFractionRing_mul
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x y : K[X]
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
⊢ 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

Tactic:
rw [← ofFractionRing_algebraMap, ← ofFractionRing_algebraMap]

Premises used: RatFunc.ofFractionRing_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x y : K[X]
⊢ 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:
fun h ↦ IsLocalization.exists_of_eq ((toFractionRingRingEquiv K).symm.injective h)

Premises used: Set.Mem, RingEquiv.injective, RatFunc.toFractionRingRingEquiv, RingEquiv.symm, IsLocalization.exists_of_eq
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x y : K[X]
⊢ 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:
exact fun h ↦ IsLocalization.exists_of_eq ((toFractionRingRingEquiv K).symm.injective h)

Premises used: RingEquiv.injective, RatFunc.toFractionRingRingEquiv, RingEquiv.symm, IsLocalization.exists_of_eq
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x : K[X]
hx : x ≠ 0
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) x : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
simpa
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
rw₁ rw₂ : 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

Tactic:
rw [← mk_eq_div, liftOn_mk _ _ f f0 @H']

Premises used: RatFunc.mk_eq_div, nonZeroDivisors.ne_zero, RatFunc.liftOn_mk
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
rw : ∀ {p q p' q' : K[X]} (_hq : q ≠ 0) (_hq' : q' ≠ 0), 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

Tactic:
rw [RatFunc.liftOn', liftOn_div _ _ _ f0]

Premises used: RatFunc.liftOn_div, nonZeroDivisors.ne_zero, RatFunc.liftOn'
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
⊢ ∀ {p q p' q' : K[X]} (_hq : q ≠ 0) (_hq' : q' ≠ 0), q' * p = q * p' → f p q = f p' q'

Tactic:
apply liftOn_condition_of_liftOn'_condition H

Premises used: RatFunc.liftOn_condition_of_liftOn'_condition
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
P : K⟮X⟯ → Prop
x : K⟮X⟯
f :
  ∀ (p q : K[X]),
    q ≠ 0 →
      P
        (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⟯))
p q : K[X]
hq : q ≠ 0
⊢ P (RatFunc.mk p q)

Tactic:
simpa using f p q hq
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯)
rw₃ rw₄ : RatFunc.mk x (↑y : K[X]) = RatFunc.mk x (↑y : K[X])
⊢ Eq (α := K⟮X⟯) { toFractionRing := IsLocalization.mk' (FractionRing K[X]) x y } (IsLocalization.mk' K⟮X⟯ x y)

Tactic:
rw [IsFractionRing.mk'_eq_div, IsFractionRing.mk'_eq_div, ← mk_eq_div', ← mk_eq_div]

Premises used: IsFractionRing.mk'_eq_div, RatFunc.mk_eq_div', RatFunc.mk_eq_div
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
f g : K[X]
hg : g ≠ 0
⊢ RatFunc.mk f g =
    IsLocalization.mk' K⟮X⟯ f (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) K[X]⁰ x) g ⋯)

Tactic:
simp only [mk_eq_div, IsFractionRing.mk'_eq_div]

Premises used: IsFractionRing.mk'_eq_div, RatFunc.mk_eq_div
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x_1 : FractionRing K[X]
x : K[X] × ↥K[X]⁰
⊢ { toFractionRing := Localization.mk x.1 x.2 : K⟮X⟯ } =
    (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) K⟮X⟯ : (a : FractionRing K[X]) → K⟮X⟯) (Localization.mk x.1 x.2)

Tactic:
simp only [Localization.mk_eq_mk'_apply, ofFractionRing_mk', IsLocalization.algEquiv_apply,
        IsLocalization.map_mk', RingHom.id_apply]

Premises used: RatFunc.ofFractionRing_mk', IsLocalization.map_mk', IsLocalization.algEquiv_apply, RingHom.id_apply, Localization.mk_eq_mk'_apply
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
x_1 : K⟮X⟯
x_2 : FractionRing K[X]
x : K[X] × ↥K[X]⁰
⊢ { toFractionRing := Localization.mk x.1 x.2 : K⟮X⟯ }.toFractionRing =
    (IsLocalization.algEquiv K[X]⁰ K⟮X⟯ (FractionRing K[X]) : (a : K⟮X⟯) → FractionRing K[X])
      { toFractionRing := Localization.mk x.1 x.2 }

Tactic:
simp only [Localization.mk_eq_mk'_apply, ofFractionRing_mk', IsLocalization.algEquiv_apply,
        IsLocalization.map_mk', RingHom.id_apply]

Premises used: RatFunc.ofFractionRing_mk', IsLocalization.map_mk', IsLocalization.algEquiv_apply, RingHom.id_apply, Localization.mk_eq_mk'_apply
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
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⟯)
⊢ Eq (α := FractionRing K[X] ≃+* K⟮X⟯) (RingEquiv.symm (toFractionRingRingEquiv K))
    (AlgEquiv.toRingEquiv (R := K[X]) (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) K⟮X⟯))

Tactic:
ext x
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
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:
simp [toFractionRingRingEquiv, ofFractionRing_eq]

Premises used: RatFunc.toFractionRingRingEquiv, RatFunc.ofFractionRing_eq
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R : Type u_1
L : Type u_2
inst_2 : CommRing R
inst_3 : Field L
inst_4 : IsDomain R
inst_5 : Algebra.{u_1, u_2} R[X] L
inst_6 : FaithfulSMul.{u_1, u_2} R[X] L
⊢ IsScalarTower.{u_1, u_1, u_2} R[X] R⟮X⟯ L

Tactic:
IsScalarTower.of_algebraMap_eq fun x =>
    (IsFractionRing.lift_algebraMap (FaithfulSMul.algebraMap_injective R[X] L) x).symm

Premises used: Polynomial, FaithfulSMul.algebraMap_injective, IsScalarTower.of_algebraMap_eq, Eq.symm, IsFractionRing.lift_algebraMap
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K_1 : Type u
inst : CommRing K_1
inst_1 : IsDomain K_1
R : Type u_1
L : Type u_2
inst_2 : CommRing R
inst_3 : Field L
inst_4 : IsDomain R
inst_5 : Algebra.{u_1, u_2} R[X] L
inst_6 : FaithfulSMul.{u_1, u_2} R[X] L
K : Type u_3
E : Type u_4
inst_7 : Field K
inst_8 : Field E
inst_9 : Algebra K E
inst_10 : FaithfulSMul K E
⊢ FaithfulSMul.{u_3, u_4} K[X] E⟮X⟯

Tactic:
(faithfulSMul_iff_algebraMap_injective ..).mpr <|
    (IsFractionRing.injective E[X] _).comp
      (Polynomial.map_injective _ <| FaithfulSMul.algebraMap_injective K E)

Premises used: Iff.mpr, faithfulSMul_iff_algebraMap_injective, IsFractionRing.injective, Polynomial.map_injective, Polynomial, Function.Injective.comp, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
rw₁ rw₂ : Module.rank k K = Module.rank k K
⊢ 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]

Premises used: rank_polynomial_polynomial, Polynomial, RatFunc, Algebra.IsAlgebraic.rank_of_isFractionRing
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
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
⊢ Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K

Tactic:
by_cases hf : Module.Finite k⟮X⟯ K⟮X⟯

Premises used: RatFunc, Module.Finite
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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.rank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.rank k K

Tactic:
have hrank := rank_ratFunc_ratFunc k K
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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⟯) : Cardinal.{u_4}) = Module.rank k K

Tactic:
rw [← Module.finrank_eq_rank] at hrank

Premises used: Module.finrank_eq_rank
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯) : Cardinal.{u_4}) = Module.rank k K
⊢ Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K

Tactic:
(Module.finrank_eq_of_rank_eq hrank.symm).symm

Premises used: Module.finrank_eq_of_rank_eq, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯) : Cardinal.{u_4}) = Module.rank k K
⊢ Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K

Tactic:
exact (Module.finrank_eq_of_rank_eq hrank.symm).symm

Premises used: Module.finrank_eq_of_rank_eq, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
rwa₁ : ¬Module.rank.{u_3, u_4} k⟮X⟯ K⟮X⟯ < Cardinal.aleph0
rwa₂ rwa₃ rwa₄ rwa₅ : ¬Module.Finite.{u_3, u_4} k⟮X⟯ K⟮X⟯
⊢ ¬Module.Finite k K

Tactic:
rwa [← Module.rank_lt_aleph0_iff, ← rank_ratFunc_ratFunc, Module.rank_lt_aleph0_iff]

Premises used: Module.rank_lt_aleph0_iff, RatFunc.rank_ratFunc_ratFunc
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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

Tactic:
have hf' : ¬ Module.Finite k K := by
      rwa [← Module.rank_lt_aleph0_iff, ← rank_ratFunc_ratFunc, Module.rank_lt_aleph0_iff]
-- Module: Mathlib.FieldTheory.RatFunc.Basic
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
neg₁ neg₂ : Eq (α := ℕ) 0 0
⊢ Module.finrank.{u_3, u_4} k⟮X⟯ K⟮X⟯ = Module.finrank k K

Tactic:
rw [Module.finrank_of_not_finite hf, Module.finrank_of_not_finite hf']

Premises used: Module.finrank_of_not_finite
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
R₀ : Type u_1
R : Type u_2
A : Type u_3
inst_2 : CommSemiring R₀
inst_3 : CommSemiring R
inst_4 : CommRing A
inst_5 : IsDomain A
inst_6 : Algebra.{u_1, u_3} R₀ A[X]
inst_7 : SMul R₀ R
inst_8 : Algebra.{u_2, u_3} R A[X]
inst_9 : IsScalarTower.{u_1, u_2, u_3} R₀ R A[X]
⊢ IsScalarTower.{u_1, u_2, u_3} R₀ R A⟮X⟯

Tactic:
IsScalarTower.to₁₂₄ _ _ A[X] _

Premises used: Polynomial, IsScalarTower.to₁₂₄
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K_1 : Type u
inst : CommRing K_1
inst_1 : IsDomain K_1
R : Type u_1
A : Type u_2
K : Type u_3
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Field K
inst_5 : Algebra.{u_2, u_3} A[X] K
inst_6 : FaithfulSMul.{u_2, u_3} A[X] K
inst_7 : CommSemiring R
inst_8 : Algebra.{u_1, u_2} R A[X]
inst_9 : SMul R K
inst_10 : IsScalarTower.{u_1, u_2, u_3} R A[X] K
⊢ IsScalarTower.{u_1, u_2, u_3} R A⟮X⟯ K

Tactic:
IsScalarTower.to₁₃₄ _ A[X] _ _

Premises used: IsScalarTower.to₁₃₄, Polynomial