-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem Away.isLocalization_mul (hd : d ≠ 0) :
    letI := (awayMap 𝒜 hg hx).toAlgebra
    IsLocalization.Away (isLocalizationElem hf hg) (Away 𝒜 x)

Proof state:
case map_units'.mk.intro.a
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ val ((awayMap 𝒜 hg hx) (isLocalizationElem hf hg) * z) = val 1

Tactic:
simp only [val_mul, val_one, awayMap_mk, Away.val_mk, z, Localization.mk_mul]

Result:
case map_units'.mk.intro.a
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ Localization.mk (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d))) (⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩) = 1

Proof state:
case surj'
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
z : Away 𝒜 x
⊢ ∃ x_1, z * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑x_1.2 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1.1

Tactic:
obtain ⟨n, s, hs, rfl⟩ := Away.mk_surjective 𝒜 (hx ▸ SetLike.mul_mem_graded hf hg) z

Result:
case surj'.intro.intro.intro
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
s : A
hs : s ∈ 𝒜 (n • (d + e))
⊢ ∃ x_1, Away.mk 𝒜 ⋯ n s hs * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑x_1.2 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1.1

Proof state:
case surj'.intro.intro.intro.succ.a
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) ⋯
⊢ ∃ c,
    ↑c *
        (↑(s * g ^ (n * d) * g ^ (n * (e + 1)), ⟨x ^ (n * (e + 1)), ⋯⟩).2 *
          (s * (g ^ (d + 1) * g ^ e) ^ n, ⟨x ^ n, ⋯⟩ * ⟨x ^ e, ⋯⟩ ^ n).1) =
      ↑c *
        (↑(s * (g ^ (d + 1) * g ^ e) ^ n, ⟨x ^ n, ⋯⟩ * ⟨x ^ e, ⋯⟩ ^ n).2 *
          (s * g ^ (n * d) * g ^ (n * (e + 1)), ⟨x ^ (n * (e + 1)), ⋯⟩).1)

Tactic:
exact ⟨1, by simp; ring⟩

Result:
no goals

Proof state:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
⊢ IsLocalization.Away (isLocalizationElem hf hg) (Away 𝒜 x)

Tactic:
constructor

Result:
case map_units'
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
⊢ ∀ (y : ↥(Submonoid.powers (isLocalizationElem hf hg))), IsUnit ((algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑y)

case surj'
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
⊢ ∀ (z : Away 𝒜 x), ∃ x_1, z * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑x_1.2 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1.1

case exists_of_eq
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
⊢ ∀ {x_1 y : Away 𝒜 f},
    (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) y → ∃ c, ↑c * x_1 = ↑c * y

Proof state:
case map_units'.mk.intro
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
⊢ IsUnit ((awayMap 𝒜 hg hx) (isLocalizationElem hf hg) ^ n)

Tactic:
let z : Away 𝒜 x := Away.mk 𝒜 (hx ▸ SetLike.mul_mem_graded hf hg) (d + e)
    (g ^ e * f ^ (2 * e + d)) <| by
  convert SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg)
    (SetLike.pow_mem_graded (2 * e + d) hf) using 2
  ring

Result:
case map_units'.mk.intro
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ IsUnit ((awayMap 𝒜 hg hx) (isLocalizationElem hf hg) ^ n)

Proof state:
case surj'.intro.intro.intro.succ.a
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) ⋯
⊢ val (Away.mk 𝒜 ⋯ n s hs * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑(t, ⟨(fun x => isLocalizationElem hf hg ^ x) n, ⋯⟩).2) =
    val ((algebraMap (Away 𝒜 f) (Away 𝒜 x)) (t, ⟨(fun x => isLocalizationElem hf hg ^ x) n, ⋯⟩).1)

Tactic:
simp only [RingHom.algebraMap_toAlgebra, map_pow, awayMap_mk, val_mul, val_mk, val_pow,
  Localization.mk_pow, Localization.mk_mul, t]

Result:
case surj'.intro.intro.intro.succ.a
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) ⋯
⊢ Localization.mk (s * (g ^ (d + 1) * g ^ e) ^ n) (⟨x ^ n, ⋯⟩ * ⟨x ^ e, ⋯⟩ ^ n) =
    Localization.mk (s * g ^ (n * d) * g ^ (n * (e + 1))) ⟨x ^ (n * (e + 1)), ⋯⟩