awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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)
⊢ 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
have 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)
Tactic: rw [← hab, mul_assoc, mk'_spec' _ a' ⟨b', b'_nonzero⟩]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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)
⊢ 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
have 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)
Tactic: rw [← hab, mul_assoc, mk'_spec' _ a' ⟨b', b'_nonzero⟩]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ 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
have rw : mk' K (num A x) (den A x) = x
Tactic: rw [← mk'_eq_div]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ x = mk' K (num A y) (den A y)
have rw : y = mk' K (num A y) (den A y)
Tactic: rw [h, mk'_num_den]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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)
⊢ x = mk' K (num A y) (den A y)
have rw₁ : y = y
Tactic: rw [h, mk'_num_den]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ y = mk' K (num A x) (den A x)
have rw : y = mk' K (num A y) (den A y)
Tactic: rw [h, mk'_num_den]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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)
⊢ y = mk' K (num A x) (den A x)
have rw₁ : y = y
Tactic: rw [h, mk'_num_den]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ num A y * (↑(den A x) : A) = num A x * (↑(den A y) : A)
have rw : num A y * (↑(den A y) : A) = num A y * (↑(den A y) : A)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ 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)
have rw : Eq.{u_2 + 1} (α := K) (0 : K) ((algebraMap A K : (a : A) → K) (num A x) : K)
Tactic: rw [zero_mul, h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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)
⊢ 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)
have rw₁ : Eq.{u_2 + 1} (α := K) (0 : K) ((algebraMap A K : (a : A) → K) 0 : K)
Tactic: rw [zero_mul, h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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)
⊢ 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)
have rw₂ : Eq.{u_2 + 1} (α := K) 0 0
Tactic: rw [zero_mul, h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (hypothesis)
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
⊢ num.{u_1, u_2} A (K := K) 0 = 0
have 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
Tactic: have := mk'_num_den' A (0 : K)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (hypothesis)
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
⊢ num.{u_1, u_2} A (K := K) 0 = 0
have 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)
Tactic: simp only [div_eq_zero_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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)
⊢ IsInteger A x
have obtain : ∀ (d : Aˣ) (hd : (↑d : A) = (↑(den A x) : A)), IsInteger A x
Tactic: obtain ⟨d, hd⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (hypothesis)
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)
⊢ IsInteger A x
have d_ne_zero : 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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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)
⊢ IsInteger A x
have h : (algebraMap A K : (a : A) → K) ((↑d⁻¹ : A) * num A x) = x
Tactic: use ↑d⁻¹ * num A x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
have h : (algebraMap A K : (a : A) → K) ((↑d⁻¹ : A) * num A x) = mk' K (num A x) (den A x)
Tactic: refine _root_.trans ?_ (mk'_num_den A x)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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) = mk' K (num A x) (den A x)
have 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)
Tactic: rw [map_mul, map_units_inv, hd]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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)
⊢ 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)
have 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))
Tactic: apply mul_left_cancel₀ d_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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)
⊢ 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))
have 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))
Tactic: rw [← mul_assoc, mul_inv_cancel₀ d_ne_zero, one_mul, mk'_spec']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← mul_assoc, mul_inv_cancel₀ d_ne_zero, one_mul, mk'_spec']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← mul_assoc, mul_inv_cancel₀ d_ne_zero, one_mul, mk'_spec']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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))
⊢ 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))
have 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)
Tactic: rw [← mul_assoc, mul_inv_cancel₀ d_ne_zero, one_mul, mk'_spec']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ IsUnit (↑(den A x) : A)
have have : ∀ (v : A) (h : (algebraMap A K : (a : A) → K) v = x), IsUnit (↑(den A x) : A)
Tactic: have ⟨v, h⟩ := h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ IsUnit (↑(den A x) : A)
have apply : (↑(den A x) : A) ∣ num A x
Tactic: apply IsRelPrime.isUnit_of_dvd (num_den_reduced A x).symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ (↑(den A x) : A) ∣ num A x
have h₁ : num A x = (↑(den A x) : A) * v
Tactic: use v
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ num A x = (↑(den A x) : A) * v
have 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)
Tactic: apply_fun algebraMap A K
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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)
⊢ num A x = (↑(den A x) : A) * v
have h₂ : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := K) (⇑(algebraMap A K) : (a : A) → K)
Tactic: apply_fun algebraMap A K
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ 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)
have 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
Tactic: simp only [map_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ (algebraMap A K : (a : A) → K) (num A x) = HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) x
have 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
Tactic: rw [mul_comm, ← div_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (goal)
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
⊢ (algebraMap A K : (a : A) → K) (num A x) = HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) x
have h₂ : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A x) : A) : K) (0 : K)
Tactic: rw [mul_comm, ← div_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (hypothesis)
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
⊢ Associated (num A x) (↑(den A x⁻¹) : A)
have this : Associated (num A x⁻¹⁻¹) (↑(den A x⁻¹) : A)
Tactic: have : Associated (num A x⁻¹⁻¹ : A) (den A x⁻¹) :=
    (associated_den_num_inv x⁻¹ (inv_ne_zero hx)).symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.NumDen (hypothesis)
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
n : A
d : ↥(nonZeroDivisors A)
pr : IsRelPrime n (↑d : A)
h : mk' K n d = x
⊢ Associated (num A x) n ∧ Associated (↑(den A x) : A) (↑d : A)
have h₁ : n * (↑(den A x) : A) = num A x * (↑d : A)
Tactic: rw [← IsFractionRing.mk'_num_den A x, IsLocalization.mk'_eq_iff_eq',
    (FaithfulSMul.algebraMap_injective _ _).eq_iff] at h
Cleared hypotheses: h