-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
lemma range_awayMapAux_subset :
    Set.range (awayMapAux 𝒜 (f := f) ⟨_, hx⟩) ⊆ Set.range (val (𝒜 := 𝒜))

Proof state:
case w.refine_2
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ f ^ j * g ^ j ∈ 𝒜 (n + j • e)

Tactic:
apply SetLike.mul_mem_graded hb'

Result:
case w.refine_2
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ g ^ j ∈ 𝒜 (j • e)

Proof state:
case intro.intro.mk.mk.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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ (HomogeneousLocalization.awayMapAux 𝒜 ⋯)
      (mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x => f ^ x) j, hb'⟩, den_mem := ⋯ }) ∈
    Set.range val

Tactic:
use mk ⟨n+j•e,⟨a*g^j, ?_⟩ ,⟨x^j, ?_⟩, j, rfl⟩

Result:
case h
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ (mk { deg := n + j • e, num := ⟨a * g ^ j, ?w.refine_1⟩, den := ⟨x ^ j, ?w.refine_2⟩, den_mem := ⋯ }).val =
    (HomogeneousLocalization.awayMapAux 𝒜 ⋯)
      (mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x => f ^ x) j, hb'⟩, den_mem := ⋯ })

case w.refine_1
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ a * g ^ j ∈ 𝒜 (n + j • e)

case w.refine_2
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ x ^ j ∈ 𝒜 (n + j • e)

Proof state:
case w.refine_2
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ g ^ j ∈ 𝒜 (j • e)

Tactic:
exact SetLike.pow_mem_graded _ hg

Result:
no goals

Proof state:
case w.refine_2
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ x ^ j ∈ 𝒜 (n + j • e)

Tactic:
rw [hx, mul_pow]

Result:
case w.refine_2
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ f ^ j * g ^ j ∈ 𝒜 (n + j • e)

Proof state:
case 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
z : Away 𝒜 f
⊢ (HomogeneousLocalization.awayMapAux 𝒜 ⋯) z ∈ Set.range val

Tactic:
obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, j, rfl : _ = b⟩, rfl⟩ := mk_surjective z

Result:
case intro.intro.mk.mk.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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ (HomogeneousLocalization.awayMapAux 𝒜 ⋯)
      (mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x => f ^ x) j, hb'⟩, den_mem := ⋯ }) ∈
    Set.range val

Proof state:
case w.refine_1
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ g ^ j ∈ 𝒜 (j • e)

Tactic:
exact SetLike.pow_mem_graded _ hg

Result:
no goals

Proof state:
case w.refine_1
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ a * g ^ j ∈ 𝒜 (n + j • e)

Tactic:
apply SetLike.mul_mem_graded ha

Result:
case w.refine_1
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ g ^ j ∈ 𝒜 (j • e)

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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
⊢ Set.range ⇑(HomogeneousLocalization.awayMapAux 𝒜 ⋯) ⊆ Set.range val

Tactic:
rintro _ ⟨z, rfl⟩

Result:
case 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
z : Away 𝒜 f
⊢ (HomogeneousLocalization.awayMapAux 𝒜 ⋯) z ∈ Set.range val

Proof state:
case h
ι : 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x => f ^ x) j ∈ 𝒜 n
⊢ (mk { deg := n + j • e, num := ⟨a * g ^ j, ?w.refine_1⟩, den := ⟨x ^ j, ?w.refine_2⟩, den_mem := ⋯ }).val =
    (HomogeneousLocalization.awayMapAux 𝒜 ⋯)
      (mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x => f ^ x) j, hb'⟩, den_mem := ⋯ })

Tactic:
simp [awayMapAux_mk 𝒜 (hx := hx)]

Result:
no goals