awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun (x : ℕ) ↦ f ^ x) n ∈ 𝒜 N
pos :
  ∀ (hfn : f ^ n = 0),
    ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
      Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
        (mk
          { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })
neg :
  ∀ (hfn : ¬f ^ n = 0),
    ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
      Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
        (mk
          { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })
⊢ ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })

Tactic:
by_cases hfn : f ^ n = 0
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun (x : ℕ) ↦ f ^ x) n ∈ 𝒜 N
hfn : f ^ n = 0
⊢ Subsingleton (HomogeneousLocalization 𝒜 (Submonoid.powers f))

Tactic:
have := HomogeneousLocalization.subsingleton 𝒜 (x := .powers f) ⟨n, hfn⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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 : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })

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

Premises used: Exists.intro, ZeroMemClass.zero_mem, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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 : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })

Tactic:
exact ⟨0, 0, zero_mem _, Subsingleton.elim _ _⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun (x : ℕ) ↦ f ^ x) n ∈ 𝒜 N
hfn : ¬f ^ n = 0
neg :
  ∀ (hs : s ∈ 𝒜 (n • d)) (hn : (fun (x : ℕ) ↦ f ^ x) n ∈ 𝒜 (n • d)),
    ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
      Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
        (mk
          { deg := n • d, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) s hs,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })
⊢ ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((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

Premises used: DirectSum.degree_eq_of_mem_mem, SetLike.pow_mem_graded, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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)
a :
  Eq (α := at Submonoid.powers f) (val (Away.mk 𝒜 hf n s hs))
    (val
      (mk
        { deg := n • d, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) }))
⊢ Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n s hs)
    (mk
      { deg := n • d, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) s hs,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })

Tactic:
ext
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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)
⊢ Eq (α := at Submonoid.powers f) (val (Away.mk 𝒜 hf n s hs))
    (val
      (mk
        { deg := n • d, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) }))

Tactic:
simp
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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 : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := n • d, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })

Tactic:
exact ⟨n, s, hs, by ext; simp⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
obtain :
  ∀ (k : ℕ) (hk : f ^ k = den z),
    ∀ᶠ (n : ℕ) in Filter.atTop,
      Membership.mem (γ := Set (at Submonoid.powers f))
        ((⇑(algebraMap A (at Submonoid.powers f)) : (a : A) → at Submonoid.powers f) '' (↑(𝒜 (n • m)) : Set A))
        (f ^ n • val z)
⊢ ∀ᶠ (n : ℕ) in Filter.atTop,
    Membership.mem (γ := Set (at Submonoid.powers f))
      ((⇑(algebraMap A (at Submonoid.powers f)) : (a : A) → at Submonoid.powers f) '' (↑(𝒜 (n • m)) : Set A))
      (f ^ n • val z)

Tactic:
obtain ⟨k, hk : f ^ k = _⟩ := z.den_mem

Premises used: HomogeneousLocalization.den_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
apply :
  Set.Ici k ⊆
    {x : ℕ |
      (fun (n : ℕ) ↦
          Membership.mem (γ := Set (at Submonoid.powers f))
            ((⇑(algebraMap A (at Submonoid.powers f)) : (a : A) → at Submonoid.powers f) '' (↑(𝒜 (n • m)) : Set A))
            (f ^ n • val z))
        x}
⊢ ∀ᶠ (n : ℕ) in Filter.atTop,
    Membership.mem (γ := Set (at Submonoid.powers f))
      ((⇑(algebraMap A (at Submonoid.powers f)) : (a : A) → at Submonoid.powers f) '' (↑(𝒜 (n • m)) : Set A))
      (f ^ n • val z)

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

Premises used: Filter.Ici_mem_atTop, Filter.mem_of_superset
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
pos :
  ∀ (hfk : f ^ k = 0),
    ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z
neg :
  ∀ (hfk : ¬f ^ k = 0),
    ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z

Tactic:
by_cases hfk : f ^ k = 0
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
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) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z

Tactic:
⟨0, zero_mem _, ?_⟩

Premises used: And.intro, Exists.intro, ZeroMemClass.zero_mem, OfNat.ofNat
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
pos : (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ k' • val z
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z

Tactic:
refine ⟨0, zero_mem _, ?_⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
pos : (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ (k' - k + k) • val z
pos₁ : 0 = f ^ (k' - k + k) • val z
pos₂ : 0 = (f ^ (k' - k) * f ^ k) • val z
pos₃ : 0 = (f ^ (k' - k) * 0) • val z
pos₄ : 0 = HSMul.hSMul (α := A) 0 (val z)
pos₅ pos₆ : Eq.{u_2 + 1} (α := at Submonoid.powers f) 0 0
⊢ (algebraMap A (at Submonoid.powers f) : (a : 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]

Premises used: pow_add, map_zero, tsub_add_cancel_of_le, MulZeroClass.mul_zero, zero_smul
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
neg :
  ∃ x ∈ 𝒜 ((k' - k + k) • m),
    Eq (α := at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x : at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) (f ^ (k' - k) * num z) :
        at Submonoid.powers f)
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : 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, ← map_mul]

Premises used: pow_add, tsub_add_cancel_of_le, map_mul, HomogeneousLocalization.den_smul_val, Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
neg :
  ∃ x ∈ 𝒜 ((k' - k) • m + deg z),
    Eq (α := at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x : at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) (f ^ (k' - k) • num z) :
        at Submonoid.powers f)
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m),
    Eq (α := at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x : at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) (f ^ (k' - k) * num z) :
        at Submonoid.powers f)

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]

Premises used: DirectSum.degree_eq_of_mem_mem, add_smul, SetLike.pow_mem_graded, smul_eq_mul
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
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),
    Eq (α := at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x : at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) (f ^ (k' - k) • num z) :
        at Submonoid.powers f)

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

Premises used: HomogeneousLocalization.num_mem_deg, SetLike.mul_mem_graded, And.intro, SetLike.pow_mem_graded, Exists.intro, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
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),
    Eq (α := at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x : at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) (f ^ (k' - k) • num z) :
        at Submonoid.powers f)

Tactic:
exact ⟨_, SetLike.mul_mem_graded (SetLike.pow_mem_graded _ hf) z.num_mem_deg, rfl⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
e : embedding 𝒜 P x = embedding 𝒜 P y
⊢ Eq.{u_4 + 1} (α := Localization (M := B) Q)
    (((IsLocalization.map (Localization (M := B) Q) (↑g : A →+* B) comap_le :
            RingHom.{u_2, u_4} (Localization (M := A) P) (Localization (M := B) Q)) :
          (a : at P) → at Q)
        (embedding 𝒜 P x) :
      Localization (M := B) Q)
    (((IsLocalization.map (Localization (M := B) Q) (↑g : A →+* B) comap_le :
            RingHom.{u_2, u_4} (Localization (M := A) P) (Localization (M := B) Q)) :
          (a : at P) → at Q)
        (embedding 𝒜 P y) :
      Localization (M := B) Q)

Tactic:
apply_fun IsLocalization.map (Localization Q) g.toRingHom comap_le at e

Premises used: IsLocalization.map, Localization, GradedRingHom.toRingHom
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
e :
  Eq.{u_4 + 1} (α := Localization (M := B) Q)
    (((IsLocalization.map (Localization (M := B) Q) (↑g : A →+* B) comap_le :
            RingHom.{u_2, u_4} (Localization (M := A) P) (Localization (M := B) Q)) :
          (a : at P) → at Q)
        (embedding 𝒜 P x) :
      Localization (M := B) Q)
    (((IsLocalization.map (Localization (M := B) Q) (↑g : A →+* B) comap_le :
            RingHom.{u_2, u_4} (Localization (M := A) P) (Localization (M := B) Q)) :
          (a : at P) → at Q)
        (embedding 𝒜 P y) :
      Localization (M := B) Q)
⊢ Eq.{u_4 + 1} (α := Localization (M := B) Q)
    (Localization.mk (((↑g : A →+* B) : (a : A) → B) (↑x.num : A))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ Q) (((↑g : A →+* B) : (a : A) → B) (↑x.den : A)) ⋯) :
      Localization (M := B) Q)
    (Localization.mk (((↑g : A →+* B) : (a : A) → B) (↑y.num : A))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ Q) (((↑g : A →+* B) : (a : A) → B) (↑y.den : A)) ⋯) :
      Localization (M := B) Q)

Tactic:
simp_rw [HomogeneousLocalization.NumDenSameDeg.embedding, Localization.mk_eq_mk',
        IsLocalization.map_mk', ← Localization.mk_eq_mk'] at e

Premises used: IsLocalization.map_mk', Localization.mk_eq_mk', HomogeneousLocalization.NumDenSameDeg.embedding
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
e :
  Eq.{u_4 + 1} (α := Localization (M := B) Q)
    (Localization.mk (((↑g : A →+* B) : (a : A) → B) (↑x.num : A))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ Q) (((↑g : A →+* B) : (a : A) → B) (↑x.den : A)) ⋯) :
      Localization (M := B) Q)
    (Localization.mk (((↑g : A →+* B) : (a : A) → B) (↑y.num : A))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ Q) (((↑g : A →+* B) : (a : A) → B) (↑y.den : A)) ⋯) :
      Localization (M := B) Q)
⊢ (Setoid.ker (embedding ℬ Q) : NumDenSameDeg ℬ Q → NumDenSameDeg ℬ Q → Prop)
    ((fun (x : NumDenSameDeg 𝒜 P) ↦
        ({ deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ } :
          NumDenSameDeg ℬ Q))
      x)
    ((fun (x : NumDenSameDeg 𝒜 P) ↦
        ({ deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ } :
          NumDenSameDeg ℬ Q))
      y)

Tactic:
e

Premises used: Set.Mem, HomogeneousLocalization.NumDenSameDeg.embedding
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
e :
  Eq.{u_4 + 1} (α := Localization (M := B) Q)
    (Localization.mk (((↑g : A →+* B) : (a : A) → B) (↑x.num : A))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ Q) (((↑g : A →+* B) : (a : A) → B) (↑x.den : A)) ⋯) :
      Localization (M := B) Q)
    (Localization.mk (((↑g : A →+* B) : (a : A) → B) (↑y.num : A))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ Q) (((↑g : A →+* B) : (a : A) → B) (↑y.den : A)) ⋯) :
      Localization (M := B) Q)
⊢ (Setoid.ker (embedding ℬ Q) : NumDenSameDeg ℬ Q → NumDenSameDeg ℬ Q → Prop)
    ((fun (x : NumDenSameDeg 𝒜 P) ↦
        ({ deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ } :
          NumDenSameDeg ℬ Q))
      x)
    ((fun (x : NumDenSameDeg 𝒜 P) ↦
        ({ deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ } :
          NumDenSameDeg ℬ Q))
      y)

Tactic:
exact e
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
simp :
  Eq (α := HomogeneousLocalization ℬ Q)
    (Quotient.mk''
      { deg := NumDenSameDeg.deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := P) 1,
        num :=
          Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ (NumDenSameDeg.deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := P) 1)) 1 ⋯,
        den :=
          Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ (NumDenSameDeg.deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := P) 1)) 1 ⋯,
        den_mem := ⋯ })
    1
⊢ Eq (α := HomogeneousLocalization ℬ Q)
    (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
      (fun (x : NumDenSameDeg 𝒜 P) ↦
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ })
      ⋯ 1)
    1

Tactic:
simp only [← mk_one (𝒜 := 𝒜), Quotient.map'_mk'',
    num_one, den_one, map_one]

Premises used: HomogeneousLocalization.mk_one, HomogeneousLocalization.NumDenSameDeg.num_one, map_one, HomogeneousLocalization.NumDenSameDeg.den_one, Quotient.map'_mk''