-- Mathlib/RingTheory/Localization/NumDen.lean
theorem exists_reduced_fraction (x : K) :
    ∃ (a : A) (b : nonZeroDivisors A), IsRelPrime a b ∧ mk' K a b = x

Proof state:
case intro.mk.intro.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : (algebraMap A K) (c' * a') = ↑⟨c' * b', b_nonzero⟩ • x
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
⊢ (algebraMap A K) (c' * b') * mk' K a' ⟨b', b'_nonzero⟩ = (algebraMap A K) (c' * b') * x

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

Result:
case intro.mk.intro.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
hab : (algebraMap A K) c' * (algebraMap A K) a' = (algebraMap A K) c' * (algebraMap A K) b' * x
⊢ (algebraMap A K) c' * (algebraMap A K) b' * mk' K a' ⟨b', b'_nonzero⟩ = (algebraMap A K) c' * (algebraMap A K) b' * x

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ ∃ a b, IsRelPrime a ↑b ∧ mk' K a b = x

Tactic:
obtain ⟨⟨b, b_nonzero⟩, a, hab⟩ := exists_integer_multiple (nonZeroDivisors A) x

Result:
case intro.mk.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
b : A
b_nonzero : b ∈ nonZeroDivisors A
a : A
hab : (algebraMap A K) a = ↑⟨b, b_nonzero⟩ • x
⊢ ∃ a b, IsRelPrime a ↑b ∧ mk' K a b = x

Proof state:
case intro.mk.intro.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : (algebraMap A K) (c' * a') = ↑⟨c' * b', b_nonzero⟩ • x
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
⊢ mk' K a' ⟨b', b'_nonzero⟩ = x

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

Result:
case intro.mk.intro.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : (algebraMap A K) (c' * a') = ↑⟨c' * b', b_nonzero⟩ • x
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
⊢ (algebraMap A K) (c' * b') * mk' K a' ⟨b', b'_nonzero⟩ = (algebraMap A K) (c' * b') * x

Proof state:
case intro.mk.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : (algebraMap A K) (c' * a') = ↑⟨c' * b', b_nonzero⟩ • x
⊢ ∃ a b, IsRelPrime a ↑b ∧ mk' K a b = x

Tactic:
obtain ⟨_, b'_nonzero⟩ := mul_mem_nonZeroDivisors.mp b_nonzero

Result:
case intro.mk.intro.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : (algebraMap A K) (c' * a') = ↑⟨c' * b', b_nonzero⟩ • x
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
⊢ ∃ a b, IsRelPrime a ↑b ∧ mk' K a b = x

Proof state:
case intro.mk.intro.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
hab : (algebraMap A K) c' * (algebraMap A K) a' = (algebraMap A K) c' * (algebraMap A K) b' * x
⊢ (algebraMap A K) c' * (algebraMap A K) b' * mk' K a' ⟨b', b'_nonzero⟩ = (algebraMap A K) c' * (algebraMap A K) b' * x

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

Result:
no goals

Proof state:
case intro.mk.intro.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : (algebraMap A K) (c' * a') = ↑⟨c' * b', b_nonzero⟩ • x
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
⊢ ∃ a b, IsRelPrime a ↑b ∧ mk' K a b = x

Tactic:
refine ⟨a', ⟨b', b'_nonzero⟩, no_factor, ?_⟩

Result:
case intro.mk.intro.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : (algebraMap A K) (c' * a') = ↑⟨c' * b', b_nonzero⟩ • x
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
⊢ mk' K a' ⟨b', b'_nonzero⟩ = x

Proof state:
case intro.mk.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
b : A
b_nonzero : b ∈ nonZeroDivisors A
a : A
hab : (algebraMap A K) a = ↑⟨b, b_nonzero⟩ • x
⊢ ∃ a b, IsRelPrime a ↑b ∧ mk' K a b = x

Tactic:
obtain ⟨a', b', c', no_factor, rfl, rfl⟩ :=
  UniqueFactorizationMonoid.exists_reduced_factors' a b
    (mem_nonZeroDivisors_iff_ne_zero.mp b_nonzero)

Result:
case intro.mk.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : IsRelPrime a' b'
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : (algebraMap A K) (c' * a') = ↑⟨c' * b', b_nonzero⟩ • x
⊢ ∃ a b, IsRelPrime a ↑b ∧ mk' K a b = x