R : Type ?u.275932
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I : Ideal A
hI : I ≠ ⊥
⊢ ∀ (y : K), y ∈ ↑I → 1 * y ∈ 1
R : Type ?u.275932
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I : Ideal A
hI : I ≠ ⊥
⊢ 1 ∈ (↑I)⁻¹
rw [mem_inv_iff (coeIdeal_ne_zero.mpr hI)]
R : Type ?u.275932
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ 1 * y ∈ 1
R : Type ?u.275932
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I : Ideal A
hI : I ≠ ⊥
⊢ ∀ (y : K), y ∈ ↑I → 1 * y ∈ 1
intro y hy
R : Type ?u.275932
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ y ∈ 1
R : Type ?u.275932
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ 1 * y ∈ 1
rw [one_mul]
no goals
R : Type ?u.275932
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I : Ideal A
hI : I ≠ ⊥
y : K
hy : y ∈ ↑I
⊢ y ∈ 1
exact coeIdeal_le_one hy