-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem isUnit_iff_isUnit_val (f : HomogeneousLocalization.AtPrime 𝒜 𝔭) :
    IsUnit f.val ↔ IsUnit f

Proof state:
case intro.mk.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
𝒜 : ι → Submodule R A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedAlgebra 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
c : ↥𝔭.primeCompl
hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)
this : ↑f.num ∉ 𝔭
⊢ mk f * Quotient.mk'' { deg := f.deg, num := f.den, den := f.num, den_mem := this } = 1

Tactic:
rw [← mk_mul, ext_iff_val, val_mk]

Result:
case intro.mk.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
𝒜 : ι → Submodule R A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedAlgebra 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
c : ↥𝔭.primeCompl
hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)
this : ↑f.num ∉ 𝔭
⊢ Localization.mk ↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).num
      ⟨↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).den, ⋯⟩ =
    val 1

Proof state:
case intro.mk.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
𝒜 : ι → Submodule R A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedAlgebra 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
c : ↥𝔭.primeCompl
hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)
this : ↑f.num ∉ 𝔭
⊢ Localization.mk ↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).num
      ⟨↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).den, ⋯⟩ =
    val 1

Tactic:
simp [mul_comm f.den.1, Localization.mk_eq_monoidOf_mk']

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
𝒜 : ι → Submodule R A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedAlgebra 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
c : ↥𝔭.primeCompl
hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)
⊢ ↑f.num ∉ 𝔭

Tactic:
exact fun h ↦ mul_mem c.2 (mul_mem f.den_mem s.2)
  (hc ▸ Ideal.mul_mem_left _ c.1 (Ideal.mul_mem_right b _ h))

Result:
no goals

Proof state:
case intro.mk
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
𝒜 : ι → Submodule R A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedAlgebra 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
f : AtPrime 𝒜 𝔭
b : at 𝔭.primeCompl
eq0 : val f * b = 1
eq1 : b * val f = 1
⊢ IsUnit f

Tactic:
obtain ⟨f, rfl⟩ := mk_surjective f

Result:
case intro.mk.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
𝒜 : ι → Submodule R A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedAlgebra 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
b : at 𝔭.primeCompl
f : NumDenSameDeg 𝒜 𝔭.primeCompl
eq0 : (mk f).val * b = 1
eq1 : b * (mk f).val = 1
⊢ IsUnit (mk f)