-- 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)
⊢ IsUnit (mk f)

Tactic:
have : f.num.1 ∉ 𝔭 := by
  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:
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 ∉ 𝔭
⊢ IsUnit (mk f)

Proof state:
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)

Tactic:
obtain ⟨b, s, rfl⟩ := IsLocalization.mk'_surjective 𝔭.primeCompl b

Result:
case intro.mk.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
eq0 : (mk f).val * IsLocalization.mk' (at 𝔭.primeCompl) b s = 1
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)

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 : AtPrime 𝒜 𝔭
h1 : IsUnit (val f)
⊢ IsUnit f

Tactic:
rcases h1 with ⟨⟨a, b, eq0, eq1⟩, rfl : a = f.val⟩

Result:
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

Proof state:
case intro.mk.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
eq0 : (mk f).val * IsLocalization.mk' (at 𝔭.primeCompl) b s = 1
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)

Tactic:
rw [val_mk, Localization.mk_eq_mk', ← IsLocalization.mk'_mul, IsLocalization.mk'_eq_iff_eq_mul,
  one_mul, IsLocalization.eq_iff_exists (M := 𝔭.primeCompl)] at eq0

Result:
case intro.mk.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
eq0 : ∃ c, ↑c * (↑f.num * b) = ↑c * ↑(⟨↑f.den, ⋯⟩ * s)
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)

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 : AtPrime 𝒜 𝔭
⊢ IsUnit (val f) ↔ IsUnit f

Tactic:
refine ⟨fun h1 ↦ ?_, IsUnit.map (algebraMap _ _)⟩

Result:
ι : 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 𝒜 𝔭
h1 : IsUnit (val f)
⊢ IsUnit f

Proof state:
case intro.mk.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
eq0 : ∃ c, ↑c * (↑f.num * b) = ↑c * ↑(⟨↑f.den, ⋯⟩ * s)
eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)

Tactic:
obtain ⟨c, hc : _ = c.1 * (f.den.1 * s.1)⟩ := eq0

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)
⊢ IsUnit (mk 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 ∉ 𝔭
⊢ IsUnit (mk f)

Tactic:
refine isUnit_of_mul_eq_one _ (Quotient.mk'' ⟨f.1, f.3, f.2, this⟩) ?_

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 ∉ 𝔭
⊢ mk f * Quotient.mk'' { deg := f.deg, num := f.den, den := f.num, den_mem := this } = 1