-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem Away.eventually_smul_mem {m} (hf : f ∈ 𝒜 m) (z : Away 𝒜 f) :
    ∀ᶠ n in Filter.atTop, f ^ n • z.val ∈ algebraMap _ _ '' (𝒜 (n • m) : Set A)

Proof state:
case neg
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) * num z)

Tactic:
rw [← smul_eq_mul, add_smul,
  DirectSum.degree_eq_of_mem_mem 𝒜 (SetLike.pow_mem_graded _ hf) (hk.symm ▸ z.den_mem_deg) hfk]

Result:
case neg
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k) • m + deg z),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) • num z)

Proof state:
case pos
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
⊢ (algebraMap A (at Submonoid.powers f)) 0 = f ^ k' • val z

Tactic:
rw [← tsub_add_cancel_of_le hk', map_zero, pow_add, hfk, mul_zero, zero_smul]

Result:
no goals

Proof state:
case neg
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k) • m + deg z),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) • num z)

Tactic:
exact ⟨_, SetLike.mul_mem_graded (SetLike.pow_mem_graded _ hf) z.num_mem_deg, rfl⟩

Result:
no goals

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
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
⊢ Set.Ici k ⊆ {x | (fun n => f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))) x}

Tactic:
rintro k' (hk' : k ≤ k')

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
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
⊢ k' ∈ {x | (fun n => f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))) x}

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
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
⊢ k' ∈ {x | (fun n => f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))) x}

Tactic:
simp only [Set.mem_image, SetLike.mem_coe, Set.mem_setOf_eq]

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
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f)) x = f ^ k' • val z

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
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))

Tactic:
apply Filter.mem_of_superset (Filter.Ici_mem_atTop k)

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
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
⊢ Set.Ici k ⊆ {x | (fun n => f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))) x}

Proof state:
case pos
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f)) x = f ^ k' • val z

Tactic:
refine ⟨0, zero_mem _, ?_⟩

Result:
case pos
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
⊢ (algebraMap A (at Submonoid.powers f)) 0 = f ^ k' • val z

Proof state:
case neg
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f)) x = f ^ k' • val z

Tactic:
rw [← tsub_add_cancel_of_le hk', pow_add, mul_smul, hk, den_smul_val,
  Algebra.smul_def, ← _root_.map_mul]

Result:
case neg
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m),
    (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) * num z)

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
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f)) x = f ^ k' • val z

Tactic:
by_cases hfk : f ^ k = 0

Result:
case pos
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f)) x = f ^ k' • val z

case neg
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
f : A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f)) x = f ^ k' • val z