[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ ∃ a b, (∀ {d : A}, d ∣ a → d ∣ ↑b → IsUnit d) ∧ mk' K a b = x
[PROOFSTEP]
obtain ⟨⟨b, b_nonzero⟩, a, hab⟩ := exists_integer_multiple (nonZeroDivisors A) x
[GOAL]
case intro.mk.intro
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
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 = ↑{ val := b, property := b_nonzero } • x
⊢ ∃ a b, (∀ {d : A}, d ∣ a → d ∣ ↑b → IsUnit d) ∧ mk' K a b = x
[PROOFSTEP]
obtain ⟨a', b', c', no_factor, rfl, rfl⟩ :=
  UniqueFactorizationMonoid.exists_reduced_factors' a b (mem_nonZeroDivisors_iff_ne_zero.mp b_nonzero)
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : ∀ {d : A}, d ∣ a' → d ∣ b' → IsUnit d
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : ↑(algebraMap A K) (c' * a') = ↑{ val := c' * b', property := b_nonzero } • x
⊢ ∃ a b, (∀ {d : A}, d ∣ a → d ∣ ↑b → IsUnit d) ∧ mk' K a b = x
[PROOFSTEP]
obtain ⟨_, b'_nonzero⟩ := mul_mem_nonZeroDivisors.mp b_nonzero
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : ∀ {d : A}, d ∣ a' → d ∣ b' → IsUnit d
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : ↑(algebraMap A K) (c' * a') = ↑{ val := c' * b', property := b_nonzero } • x
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
⊢ ∃ a b, (∀ {d : A}, d ∣ a → d ∣ ↑b → IsUnit d) ∧ mk' K a b = x
[PROOFSTEP]
refine' ⟨a', ⟨b', b'_nonzero⟩, no_factor, _⟩
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : ∀ {d : A}, d ∣ a' → d ∣ b' → IsUnit d
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : ↑(algebraMap A K) (c' * a') = ↑{ val := c' * b', property := b_nonzero } • x
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
⊢ mk' K a' { val := b', property := b'_nonzero } = x
[PROOFSTEP]
refine' mul_left_cancel₀ (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors b_nonzero) _
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : ∀ {d : A}, d ∣ a' → d ∣ b' → IsUnit d
b_nonzero : c' * b' ∈ nonZeroDivisors A
hab : ↑(algebraMap A K) (c' * a') = ↑{ val := c' * b', property := b_nonzero } • x
left✝ : c' ∈ nonZeroDivisors A
b'_nonzero : b' ∈ nonZeroDivisors A
⊢ ↑(algebraMap A K) (c' * b') * mk' K a' { val := b', property := b'_nonzero } = ↑(algebraMap A K) (c' * b') * x
[PROOFSTEP]
simp only [Subtype.coe_mk, RingHom.map_mul, Algebra.smul_def] at *
[GOAL]
case intro.mk.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
a' b' c' : A
no_factor : ∀ {d : A}, d ∣ a' → d ∣ b' → IsUnit d
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' { val := b', property := b'_nonzero } =
    ↑(algebraMap A K) c' * ↑(algebraMap A K) b' * x
[PROOFSTEP]
erw [← hab, mul_assoc, mk'_spec' _ a' ⟨b', b'_nonzero⟩]
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ ↑(algebraMap A K) (num A x) / ↑(algebraMap A K) ↑(den A x) = x
[PROOFSTEP]
rw [← mk'_eq_div]
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
⊢ mk' K (num A x) (den A x) = x
[PROOFSTEP]
apply mk'_num_den
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x * ↑(algebraMap A K) ↑(den A y) = ↑(algebraMap A K) (num A y)
⊢ x = y
[PROOFSTEP]
simpa only [mk'_num_den] using eq_mk'_iff_mul_eq.mpr h
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ x = mk' K (num A y) (den A y)
[PROOFSTEP]
rw [h, mk'_num_den]
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : y * ↑(algebraMap A K) ↑(den A x) = ↑(algebraMap A K) (num A x)
⊢ x = y
[PROOFSTEP]
simpa only [eq_comm, mk'_num_den] using eq_mk'_iff_mul_eq.mpr h
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ y = mk' K (num A x) (den A x)
[PROOFSTEP]
rw [h, mk'_num_den]
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : num A y * ↑(den A x) = num A x * ↑(den A y)
⊢ x = y
[PROOFSTEP]
simpa only [mk'_num_den] using mk'_eq_of_eq' (S := K) h
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x y : K
h : x = y
⊢ num A y * ↑(den A x) = num A x * ↑(den A y)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
h : num A x = 0
⊢ 0 * ↑(algebraMap (?m.160854 h) K) ↑(den (?m.160854 h) x) = ↑(algebraMap (?m.160854 h) K) (num (?m.160854 h) x)
[PROOFSTEP]
rw [zero_mul, h, RingHom.map_zero]
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
h : IsUnit ↑(den A x)
⊢ IsInteger A x
[PROOFSTEP]
cases' h with d hd
[GOAL]
case intro
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
d : Aˣ
hd : ↑d = ↑(den A x)
⊢ IsInteger A x
[PROOFSTEP]
have d_ne_zero : algebraMap A K (den A x) ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (den A x).2
[GOAL]
case intro
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : ↑(algebraMap A K) ↑(den A x) ≠ 0
⊢ IsInteger A x
[PROOFSTEP]
use↑d⁻¹ * num A x
[GOAL]
case h
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : ↑(algebraMap A K) ↑(den A x) ≠ 0
⊢ ↑(algebraMap A K) (↑d⁻¹ * num A x) = x
[PROOFSTEP]
refine' _root_.trans _ (mk'_num_den A x)
[GOAL]
case h
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : ↑(algebraMap A K) ↑(den A x) ≠ 0
⊢ ↑(algebraMap A K) (↑d⁻¹ * num A x) = mk' K (num A x) (den A x)
[PROOFSTEP]
rw [map_mul, map_units_inv, hd]
[GOAL]
case h
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : ↑(algebraMap A K) ↑(den A x) ≠ 0
⊢ (↑(algebraMap A K) ↑(den A x))⁻¹ * ↑(algebraMap A K) (num A x) = mk' K (num A x) (den A x)
[PROOFSTEP]
apply mul_left_cancel₀ d_ne_zero
[GOAL]
case h
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : ↑(algebraMap A K) ↑(den A x) ≠ 0
⊢ ↑(algebraMap A K) ↑(den A x) * ((↑(algebraMap A K) ↑(den A x))⁻¹ * ↑(algebraMap A K) (num A x)) =
    ↑(algebraMap A K) ↑(den A x) * mk' K (num A x) (den A x)
[PROOFSTEP]
rw [← mul_assoc, mul_inv_cancel d_ne_zero, one_mul, mk'_spec']
