case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
d : Aˣ
hd : ↑d = ↑(den A x)
⊢ IsInteger A x
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
h : IsUnit ↑(den A x)
⊢ IsInteger A x
cases' h with d hd
case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : ↑(algebraMap A K) ↑(den A x) ≠ 0
⊢ IsInteger A x
case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
d : Aˣ
hd : ↑d = ↑(den A x)
⊢ IsInteger A x
have d_ne_zero : algebraMap A K (den A x) ≠ 0 :=
  IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (den A x).2
case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
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
case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
d : Aˣ
hd : ↑d = ↑(den A x)
d_ne_zero : ↑(algebraMap A K) ↑(den A x) ≠ 0
⊢ IsInteger A x
use ↑d⁻¹ * num A x
case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
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)
case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
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
refine' _root_.trans _ (mk'_num_den A x)
case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
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)
case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
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)
rw [map_mul, map_units_inv, hd]
case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
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)
case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
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)
apply mul_left_cancel₀ d_ne_zero
no goals
case intro
R : Type ?u.153107
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.153313
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.153567
inst✝⁶ : CommRing P
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
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)
rw [← mul_assoc, mul_inv_cancel d_ne_zero, one_mul, mk'_spec']