awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) (c' * b')
hab :
  (algebraMap A K : (a : A) → K) (c' * a') =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) (c' * b')
            b_nonzero) :
        A) •
      x
left : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) c'
b'_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b'
refine :
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c' * b') : K)
      (mk' K a'
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero)) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c' * b') : K) x
⊢ mk' K a' (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero) = x

Tactic:
refine mul_left_cancel₀ (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors b_nonzero) ?_

Premises used: mul_left_cancel₀, IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) (c' * b')
hab :
  (algebraMap A K : (a : A) → K) (c' * a') =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) (c' * b')
            b_nonzero) :
        A) •
      x
left : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) c'
b'_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b'
simp :
  ∀
    (hab :
      HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) a' : K) =
        HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) *
          x),
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) *
        mk' K a'
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero) =
      HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) * x
⊢ HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c' * b') : K)
      (mk' K a'
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero)) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (c' * b') : K) x

Tactic:
simp only [map_mul, Algebra.smul_def] at *

Premises used: map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) (c' * b')
left : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) c'
b'_nonzero : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) b'
hab :
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) a' : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) * x
rw :
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) *
      mk' K a' (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) a' : K)
rw₁ :
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) c' : K)
      (HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) b' : K)
        (mk' K a'
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero))) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) a' : K)
rw₂ rw₃ :
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) a' : K) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) a' : K)
⊢ HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) *
      mk' K a' (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) x) b' b'_nonzero) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) c' : K) ((algebraMap A K : (a : A) → K) b' : K) * x

Tactic:
rw [← hab, mul_assoc, mk'_spec' _ a' ⟨b', b'_nonzero⟩]

Premises used: mul_assoc, IsLocalization.mk'_spec', Subtype.mk
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
⊢ IsRelPrime (num A x) (↑(den A x) : A)

Tactic:
(Classical.choose_spec (Classical.choose_spec (exists_reduced_fraction A x))).1

Premises used: IsFractionRing.exists_reduced_fraction, Classical.choose_spec, And.left, IsFractionRing.num
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
⊢ mk' K (num A x) (den A x) = x

Tactic:
(Classical.choose_spec (Classical.choose_spec (exists_reduced_fraction A x))).2

Premises used: IsFractionRing.exists_reduced_fraction, IsFractionRing.den, Classical.choose_spec, And.right, IsFractionRing.num
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
rw : mk' K (num A x) (den A x) = x
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A x) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) =
    x

Tactic:
rw [← mk'_eq_div]

Premises used: IsFractionRing.mk'_eq_div
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
⊢ mk' K (num A x) (den A x) = x

Tactic:
apply mk'_num_den

Premises used: IsFractionRing.mk'_num_den
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  HMul.hMul (β := K) x ((algebraMap A K : (a : A) → K) (↑(den A y) : A) : K) = (algebraMap A K : (a : A) → K) (num A y)
⊢ x = y

Tactic:
simpa only [mk'_num_den] using eq_mk'_iff_mul_eq.mpr h

Premises used: Iff.mpr, IsFractionRing.mk'_num_den, IsLocalization.eq_mk'_iff_mul_eq
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h : x = y
rw : y = mk' K (num A y) (den A y)
rw₁ rw₂ : y = y
⊢ x = mk' K (num A y) (den A y)

Tactic:
rw [h, mk'_num_den]

Premises used: IsFractionRing.mk'_num_den
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  HMul.hMul (β := K) y ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) = (algebraMap A K : (a : A) → K) (num A x)
⊢ x = y

Tactic:
simpa only [eq_comm, mk'_num_den] using eq_mk'_iff_mul_eq.mpr h

Premises used: Iff.mpr, eq_comm, IsFractionRing.mk'_num_den, IsLocalization.eq_mk'_iff_mul_eq
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h : x = y
rw : y = mk' K (num A y) (den A y)
rw₁ rw₂ : y = y
⊢ y = mk' K (num A x) (den A x)

Tactic:
rw [h, mk'_num_den]

Premises used: IsFractionRing.mk'_num_den
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h : num A y * (↑(den A x) : A) = num A x * (↑(den A y) : A)
⊢ x = y

Tactic:
simpa only [mk'_num_den] using mk'_eq_of_eq' (S := K) h

Premises used: IsFractionRing.mk'_num_den, IsLocalization.mk'_eq_of_eq'
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h : x = y
rw rw₁ : num A y * (↑(den A y) : A) = num A y * (↑(den A y) : A)
⊢ num A y * (↑(den A x) : A) = num A x * (↑(den A y) : A)

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h : num A x = 0
rw : Eq.{u_2 + 1} (α := K) (0 : K) ((algebraMap A K : (a : A) → K) (num A x) : K)
rw₁ : Eq.{u_2 + 1} (α := K) (0 : K) ((algebraMap A K : (a : A) → K) 0 : K)
rw₂ rw₃ : Eq.{u_2 + 1} (α := K) 0 0
⊢ HMul.hMul (α := K) (β := K) (0 : K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) =
    (algebraMap A K : (a : A) → K) (num A x)

Tactic:
rw [zero_mul, h, map_zero]

Premises used: MulZeroClass.zero_mul, map_zero
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num.{u_1, u_2} A (K := K) 0) : K)
      ((algebraMap A K : (a : A) → K) (↑(den.{u_1, u_2} A (K := K) 0) : A) : K) =
    0

Tactic:
have := mk'_num_den' A (0 : K)
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
this :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num.{u_1, u_2} A (K := K) 0) : K)
      ((algebraMap A K : (a : A) → K) (↑(den.{u_1, u_2} A (K := K) 0) : A) : K) =
    0
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (num.{u_1, u_2} A (K := K) 0) : K) (0 : K) ∨
    Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den.{u_1, u_2} A (K := K) 0) : A) : K) (0 : K)

Tactic:
simp only [div_eq_zero_iff] at this

Premises used: div_eq_zero_iff
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
this :
  Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (num.{u_1, u_2} A (K := K) 0) : K) (0 : K) ∨
    Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den.{u_1, u_2} A (K := K) 0) : A) : K) (0 : K)
⊢ num.{u_1, u_2} A (K := K) 0 = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
⊢ num A x = 0 ↔ x = 0

Tactic:
⟨eq_zero_of_num_eq_zero, fun h ↦ h ▸ num_zero⟩

Premises used: Eq.rec, IsFractionRing.eq_zero_of_num_eq_zero, IsFractionRing.num_zero, Iff.intro, Eq.symm
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h : IsUnit (↑(den A x) : A)
obtain : ∀ (d : Aˣ) (hd : (↑d : A) = (↑(den A x) : A)), IsInteger A x
⊢ IsInteger A x

Tactic:
obtain ⟨d, hd⟩ := h
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
d : Aˣ
hd : (↑d : A) = (↑(den A x) : A)
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (0 : K)

Tactic:
have d_ne_zero : algebraMap A K (den A x) ≠ 0 :=
    IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (den A x).2
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
d : Aˣ
hd : (↑d : A) = (↑(den A x) : A)
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (0 : K)
h : (algebraMap A K : (a : A) → K) ((↑d⁻¹ : A) * num A x) = x
⊢ IsInteger A x

Tactic:
use ↑d⁻¹ * num A x

Premises used: IsFractionRing.num
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
d : Aˣ
hd : (↑d : A) = (↑(den A x) : A)
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (0 : K)
⊢ (algebraMap A K : (a : A) → K) ((↑d⁻¹ : A) * num A x) = x

Tactic:
_root_.trans ?_ (mk'_num_den A x)

Premises used: trans, IsFractionRing.mk'_num_den
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
d : Aˣ
hd : (↑d : A) = (↑(den A x) : A)
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (0 : K)
h : (algebraMap A K : (a : A) → K) ((↑d⁻¹ : A) * num A x) = mk' K (num A x) (den A x)
⊢ (algebraMap A K : (a : A) → K) ((↑d⁻¹ : A) * num A x) = x

Tactic:
refine _root_.trans ?_ (mk'_num_den A x)

Premises used: trans, IsFractionRing.mk'_num_den
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
d : Aˣ
hd : (↑d : A) = (↑(den A x) : A)
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (0 : K)
h :
  HMul.hMul (α := K) (β := K) (((algebraMap A K : (a : A) → K) (↑(den A x) : A))⁻¹ : K)
      ((algebraMap A K : (a : A) → K) (num A x) : K) =
    mk' K (num A x) (den A x)
⊢ (algebraMap A K : (a : A) → K) ((↑d⁻¹ : A) * num A x) = mk' K (num A x) (den A x)

Tactic:
rw [map_mul, map_units_inv, hd]

Premises used: map_units_inv, map_mul
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
d : Aˣ
hd : (↑d : A) = (↑(den A x) : A)
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (0 : K)
h :
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K)
      (HMul.hMul (α := K) (β := K) (((algebraMap A K : (a : A) → K) (↑(den A x) : A))⁻¹ : K)
        ((algebraMap A K : (a : A) → K) (num A x) : K)) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (mk' K (num A x) (den A x))
⊢ HMul.hMul (α := K) (β := K) (((algebraMap A K : (a : A) → K) (↑(den A x) : A))⁻¹ : K)
      ((algebraMap A K : (a : A) → K) (num A x) : K) =
    mk' K (num A x) (den A x)

Tactic:
apply mul_left_cancel₀ d_ne_zero

Premises used: mul_left_cancel₀
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
d : Aˣ
hd : (↑d : A) = (↑(den A x) : A)
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (0 : K)
h :
  HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K)
        (((algebraMap A K : (a : A) → K) (↑(den A x) : A))⁻¹ : K))
      ((algebraMap A K : (a : A) → K) (num A x) : K) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (mk' K (num A x) (den A x))
h₁ :
  HMul.hMul (α := K) (β := K) (1 : K) ((algebraMap A K : (a : A) → K) (num A x) : K) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (mk' K (num A x) (den A x))
h₂ :
  (algebraMap A K : (a : A) → K) (num A x) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (mk' K (num A x) (den A x))
h₃ h₄ :
  Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (num A x) : K) ((algebraMap A K : (a : A) → K) (num A x) : K)
⊢ HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K)
      (HMul.hMul (α := K) (β := K) (((algebraMap A K : (a : A) → K) (↑(den A x) : A))⁻¹ : K)
        ((algebraMap A K : (a : A) → K) (num A x) : K)) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (mk' K (num A x) (den A x))

Tactic:
rw [← mul_assoc, mul_inv_cancel₀ d_ne_zero, one_mul, mk'_spec']

Premises used: mul_inv_cancel₀, mul_assoc, IsLocalization.mk'_spec', one_mul
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h : IsInteger A x
have : ∀ (v : A) (h : (algebraMap A K : (a : A) → K) v = x), IsUnit (↑(den A x) : A)
⊢ IsUnit (↑(den A x) : A)

Tactic:
have ⟨v, h⟩ := h
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h_1 : IsInteger A x
v : A
h : (algebraMap A K : (a : A) → K) v = x
apply : (↑(den A x) : A) ∣ num A x
⊢ IsUnit (↑(den A x) : A)

Tactic:
apply IsRelPrime.isUnit_of_dvd (num_den_reduced A x).symm

Premises used: IsRelPrime.symm, IsRelPrime.isUnit_of_dvd, IsFractionRing.num_den_reduced
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h_1 : IsInteger A x
v : A
h : (algebraMap A K : (a : A) → K) v = x
h₁ : num A x = (↑(den A x) : A) * v
⊢ (↑(den A x) : A) ∣ num A x

Tactic:
use v
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h_1 : IsInteger A x
v : A
h : (algebraMap A K : (a : A) → K) v = x
h₁ :
  Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (num A x) : K)
    ((algebraMap A K : (a : A) → K) ((↑(den A x) : A) * v) : K)
h₂ : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := K) (⇑(algebraMap A K) : (a : A) → K)
⊢ num A x = (↑(den A x) : A) * v

Tactic:
apply_fun algebraMap A K

Premises used: Algebra.algebraMap
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h_1 : IsInteger A x
v : A
h : (algebraMap A K : (a : A) → K) v = x
h₁ :
  (algebraMap A K : (a : A) → K) (num A x) = HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) x
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (num A x) : K)
    ((algebraMap A K : (a : A) → K) ((↑(den A x) : A) * v) : K)

Tactic:
simp only [map_mul, h]

Premises used: map_mul
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h_1 : IsInteger A x
v : A
h : (algebraMap A K : (a : A) → K) v = x
h₁ :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A x) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) =
    x
h₂ : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (0 : K)
⊢ (algebraMap A K : (a : A) → K) (num A x) = HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) x

Tactic:
rw [mul_comm, ← div_eq_iff]

Premises used: div_eq_iff, mul_comm
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h_1 : IsInteger A x
v : A
h : (algebraMap A K : (a : A) → K) v = x
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A x) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) =
    x

Tactic:
simp only [mk'_num_den']

Premises used: IsFractionRing.mk'_num_den'
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h_1 : IsInteger A x
v : A
h : (algebraMap A K : (a : A) → K) v = x
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (0 : K)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h_1 : IsInteger A x
v : A
h : (algebraMap A K : (a : A) → K) v = x
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := K) (⇑(algebraMap A K) : (a : A) → K)

Tactic:
FaithfulSMul.algebraMap_injective A K

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h_1 : IsInteger A x
v : A
h : (algebraMap A K : (a : A) → K) v = x
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := K) (⇑(algebraMap A K) : (a : A) → K)

Tactic:
exact FaithfulSMul.algebraMap_injective A K

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
⊢ IsUnit (↑(den.{u_1, u_2} A (K := K) 0) : A)

Tactic:
simp [isUnit_den_iff, IsLocalization.isInteger_zero]

Premises used: IsLocalization.isInteger_zero, IsFractionRing.isUnit_den_iff
-- Module: Mathlib.RingTheory.Localization.NumDen
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
K : Type u_2
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A x⁻¹ * num A x) : K)
      ((algebraMap A K : (a : A) → K) ((↑(den A x⁻¹) : A) * (↑(den A x) : A)) : K) =
    1

Tactic:
simp [mul_div_mul_comm, hx]

Premises used: mul_div_mul_comm