-- 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 exists_of_eq.intro.intro.intro.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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
e : ∃ c, ↑c * (x ^ m * (a * g ^ n)) = ↑c * (x ^ n * (b * g ^ m))
⊢ ∃ c, ↑c * Away.mk 𝒜 hf n a ha = ↑c * Away.mk 𝒜 hf m b hb

Tactic:
obtain ⟨⟨_, k, rfl⟩, hc⟩ := e

Result:
case exists_of_eq.intro.intro.intro.intro.intro.intro.intro.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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc : ↑⟨(fun x_1 => x ^ x_1) k, ⋯⟩ * (x ^ m * (a * g ^ n)) = ↑⟨(fun x_1 => x ^ x_1) k, ⋯⟩ * (x ^ n * (b * g ^ m))
⊢ ∃ c, ↑c * Away.mk 𝒜 hf n a ha = ↑c * Away.mk 𝒜 hf m b hb

Proof state:
case h.e'_4.h.e'_1
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))
⊢ (n * (e + 1)) • (d + 1) = n • (d + 1 + e) + (n * d) • e

Tactic:
simp

Result:
case h.e'_4.h.e'_1
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))
⊢ n * (e + 1) * (d + 1) = n * (d + 1 + e) + n * d * e

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
n : ℕ
⊢ g ^ e * f ^ (2 * e + d) ∈ 𝒜 ((d + e) • (d + e))

Tactic:
convert SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg)
  (SetLike.pow_mem_graded (2 * e + d) hf) using 2

Result:
case h.e'_4.h.e'_1
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 : ℕ
⊢ (d + e) • (d + e) = e • e + (2 * e + d) • d

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)) ⋯
⊢ Localization.mk (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d))) (⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩) = 1

Tactic:
rw [← Localization.mk_one, Localization.mk_eq_mk_iff, Localization.r_iff_exists]

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)) ⋯
⊢ ∃ c,
    ↑c * (↑(1, 1).2 * (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)), ⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩).1) =
      ↑c * (↑(g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)), ⟨x ^ e, ⋯⟩ * ⟨x ^ (d + e), ⋯⟩).2 * (1, 1).1)

Proof state:
case exists_of_eq.intro.intro.intro.intro.intro.intro.intro.mk.intro.a.succ
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 : ℕ
a : A
m : ℕ
b : A
k : ℕ
hc : ↑⟨(fun x_1 => x ^ x_1) k, ⋯⟩ * (x ^ m * (a * g ^ n)) = ↑⟨(fun x_1 => x ^ x_1) k, ⋯⟩ * (x ^ n * (b * g ^ m))
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
⊢ (fun x => f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    (fun x => f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))

Tactic:
subst hx

Result:
case exists_of_eq.intro.intro.intro.intro.intro.intro.intro.mk.intro.a.succ
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
n : ℕ
a : A
m : ℕ
b : A
k d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := (awayMap 𝒜 hg ⋯).toAlgebra
hc :
  ↑⟨(fun x => (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ m * (a * g ^ n)) =
    ↑⟨(fun x => (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ n * (b * g ^ m))
⊢ (fun x => f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    (fun x => f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))

Proof state:
case h
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)) ⋯
⊢ g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)) = (f * g) ^ e * (f * g) ^ (d + e)

Tactic:
ring

Result:
no goals

Proof state:
case surj'.intro.intro.intro.succ
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)) ⋯
⊢ Away.mk 𝒜 ⋯ n s hs * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑(t, ⟨(fun x => isLocalizationElem hf hg ^ x) n, ⋯⟩).2 =
    (algebraMap (Away 𝒜 f) (Away 𝒜 x)) (t, ⟨(fun x => isLocalizationElem hf hg ^ x) n, ⋯⟩).1

Tactic:
ext

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)) ⋯
⊢ 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)