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

Tactic:
simp only [OneMemClass.coe_one, one_mul, Submonoid.coe_mul, mul_one, hx]

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

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 : ℕ
z : Away 𝒜 x := Away.mk 𝒜 ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ (awayMap 𝒜 hg hx) (isLocalizationElem hf hg) * z = 1

Tactic:
ext

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)) ⋯
⊢ val ((awayMap 𝒜 hg hx) (isLocalizationElem hf hg) * z) = val 1

Proof state:
case exists_of_eq.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
b : Away 𝒜 f
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
e : (algebraMap (Away 𝒜 f) (Away 𝒜 x)) (Away.mk 𝒜 hf n a ha) = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) b
⊢ ∃ c, ↑c * Away.mk 𝒜 hf n a ha = ↑c * b

Tactic:
obtain ⟨m, b, hb, rfl⟩ := Away.mk_surjective 𝒜 hf b

Result:
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 : (algebraMap (Away 𝒜 f) (Away 𝒜 x)) (Away.mk 𝒜 hf n a ha) = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) (Away.mk 𝒜 hf m b hb)
⊢ ∃ c, ↑c * Away.mk 𝒜 hf n a ha = ↑c * Away.mk 𝒜 hf m b hb

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

Tactic:
rcases d with - | d

Result:
case surj'.intro.intro.intro.zero
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
hf : f ∈ 𝒜 0
hd : 0 ≠ 0
hs : s ∈ 𝒜 (n • (0 + e))
⊢ ∃ x_1, Away.mk 𝒜 ⋯ n s hs * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑x_1.2 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1.1

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))
⊢ ∃ 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:
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
⊢ IsLocalization.Away (isLocalizationElem hf hg) (Away 𝒜 x)

Tactic:
letI := (awayMap 𝒜 hg hx).toAlgebra

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

Proof state:
case exists_of_eq.intro.intro.intro.intro.intro.intro.intro.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 : ℕ
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))
⊢ (fun x => f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
    (fun x => f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))

Tactic:
rcases d with - | d

Result:
case exists_of_eq.intro.intro.intro.intro.intro.intro.intro.mk.intro.a.zero
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))
hf : f ∈ 𝒜 0
hd : 0 ≠ 0
ha : a ∈ 𝒜 (n • 0)
hb : b ∈ 𝒜 (m • 0)
⊢ (fun x => f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ 0) ^ (k + m + n) * a)) =
    (fun x => f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ 0) ^ (k + m + n) * b))

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