-- 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
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
a b : Away 𝒜 f
e : (algebraMap (Away 𝒜 f) (Away 𝒜 x)) a = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) b
⊢ ∃ c, ↑c * a = ↑c * b

Tactic:
obtain ⟨n, a, ha, rfl⟩ := Away.mk_surjective 𝒜 hf a

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

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

Tactic:
convert congr(f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) * $hc) using 1 <;> ring

Result:
no goals

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

Tactic:
replace e := congr_arg val e

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 :
  val ((algebraMap (Away 𝒜 f) (Away 𝒜 x)) (Away.mk 𝒜 hf n a ha)) =
    val ((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 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))
⊢ val (↑⟨(fun x => isLocalizationElem hf hg ^ x) (k + m + n), ⋯⟩ * Away.mk 𝒜 hf n a ha) =
    val (↑⟨(fun x => isLocalizationElem hf hg ^ x) (k + m + n), ⋯⟩ * Away.mk 𝒜 hf m b hb)

Tactic:
simp only [OneMemClass.coe_one, one_mul, val_mul, val_pow, val_mk, Localization.mk_pow,
  Localization.mk_eq_mk_iff, Localization.r_iff_exists, Submonoid.coe_mul, Localization.mk_mul,
  SubmonoidClass.coe_pow, Subtype.exists, exists_prop]

Result:
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))
⊢ ∃ a_1 ∈ Submonoid.powers f,
    a_1 * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
      a_1 * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))

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))
⊢ ∃ x_1, Away.mk 𝒜 ⋯ n s hs * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑x_1.2 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1.1

Tactic:
let t : Away 𝒜 f := Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) <| by
  convert SetLike.mul_mem_graded hs (SetLike.pow_mem_graded _ hg) using 2; simp; ring

Result:
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)) ⋯
⊢ ∃ 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
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)) ⋯
⊢ ∃ x_1, Away.mk 𝒜 ⋯ n s hs * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑x_1.2 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1.1

Tactic:
refine ⟨⟨t, ⟨_, ⟨n, rfl⟩⟩⟩, ?_⟩

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

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

Tactic:
ring

Result:
no goals