-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
protected
lemma Away.mk_surjective {d : ι} (hf : f ∈ 𝒜 d) (x : Away 𝒜 f) :
    ∃ n a ha, Away.mk 𝒜 hf n a ha = x

Proof state:
case a
ι : 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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
s : A
n : ℕ
hfn : ¬f ^ n = 0
hs : s ∈ 𝒜 (n • d)
hn : (fun x => f ^ x) n ∈ 𝒜 (n • d)
⊢ val (Away.mk 𝒜 hf n s hs) = (mk { deg := n • d, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }).val

Tactic:
simp

Result:
no goals

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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
x : Away 𝒜 f
⊢ ∃ n a, ∃ (ha : a ∈ 𝒜 (n • d)), Away.mk 𝒜 hf n a ha = x

Tactic:
obtain ⟨⟨N, ⟨s, hs⟩, ⟨b, hn⟩, ⟨n, (rfl : _ = b)⟩⟩, rfl⟩ := mk_surjective x

Result:
case 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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x => f ^ x) n ∈ 𝒜 N
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }

Proof state:
case 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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x => f ^ x) n ∈ 𝒜 N
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }

Tactic:
by_cases hfn : f ^ n = 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
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x => f ^ x) n ∈ 𝒜 N
hfn : f ^ n = 0
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }

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
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x => f ^ x) n ∈ 𝒜 N
hfn : ¬f ^ n = 0
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }

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
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x => f ^ x) n ∈ 𝒜 N
hfn : f ^ n = 0
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }

Tactic:
have := HomogeneousLocalization.subsingleton 𝒜 (x := .powers f) ⟨n, hfn⟩

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
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x => f ^ x) n ∈ 𝒜 N
hfn : f ^ n = 0
this : Subsingleton (HomogeneousLocalization 𝒜 (Submonoid.powers f))
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }

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
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x => f ^ x) n ∈ 𝒜 N
hfn : f ^ n = 0
this : Subsingleton (HomogeneousLocalization 𝒜 (Submonoid.powers f))
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }

Tactic:
exact ⟨0, 0, zero_mem _, Subsingleton.elim _ _⟩

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
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
s : A
n : ℕ
hfn : ¬f ^ n = 0
hs : s ∈ 𝒜 (n • d)
hn : (fun x => f ^ x) n ∈ 𝒜 (n • d)
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := n • d, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }

Tactic:
exact ⟨n, s, hs, by ext; simp⟩

Result:
no goals

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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
s : A
n : ℕ
hfn : ¬f ^ n = 0
hs : s ∈ 𝒜 (n • d)
hn : (fun x => f ^ x) n ∈ 𝒜 (n • d)
⊢ Away.mk 𝒜 hf n s hs = mk { deg := n • d, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }

Tactic:
ext

Result:
case a
ι : 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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
s : A
n : ℕ
hfn : ¬f ^ n = 0
hs : s ∈ 𝒜 (n • d)
hn : (fun x => f ^ x) n ∈ 𝒜 (n • d)
⊢ val (Away.mk 𝒜 hf n s hs) = (mk { deg := n • d, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }).val

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
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x => f ^ x) n ∈ 𝒜 N
hfn : ¬f ^ n = 0
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }

Tactic:
obtain rfl := DirectSum.degree_eq_of_mem_mem 𝒜 hn (SetLike.pow_mem_graded n hf) hfn

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
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
s : A
n : ℕ
hfn : ¬f ^ n = 0
hs : s ∈ 𝒜 (n • d)
hn : (fun x => f ^ x) n ∈ 𝒜 (n • d)
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := n • d, num := ⟨s, hs⟩, den := ⟨(fun x => f ^ x) n, hn⟩, den_mem := ⋯ }