awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
⊢ g ^ e * f ^ (2 * e + d) ∈ 𝒜 (e • e + (2 * e + d) • d)

Tactic:
SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg)
          (SetLike.pow_mem_graded (2 * e + d) hf)

Premises used: HMul.hMul, SetLike.mul_mem_graded, HAdd.hAdd, SetLike.pow_mem_graded, OfNat.ofNat
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
h : (d + e) • (d + e) = e • e + (2 * e + d) • d
⊢ g ^ e * f ^ (2 * e + d) ∈ 𝒜 ((d + e) • (d + e))

Tactic:
convert!
        SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg)
          (SetLike.pow_mem_graded (2 * e + d) hf) using 2

Premises used: HMul.hMul, SetLike.mul_mem_graded, HAdd.hAdd, SetLike.pow_mem_graded, OfNat.ofNat
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
⊢ (d + e) • (d + e) = e • e + (2 * e + d) • d

Tactic:
ring
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ IsUnit
    (HPow.hPow (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x) n)

Tactic:
(isUnit_iff_exists_inv.mpr ⟨z, ?_⟩).pow _

Premises used: Iff.mpr, isUnit_iff_exists_inv, IsUnit.pow, Exists.intro
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
toIsLocalizationMap :
  HMul.hMul (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x) z = 1
⊢ IsUnit
    (HPow.hPow (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x) n)

Tactic:
refine (isUnit_iff_exists_inv.mpr ⟨z, ?_⟩).pow _

Premises used: Iff.mpr, isUnit_iff_exists_inv, IsUnit.pow, Exists.intro
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
toIsLocalizationMap :
  val
      (HMul.hMul (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x)
        z) =
    val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) 1
⊢ HMul.hMul (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x) z = 1

Tactic:
ext
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
toIsLocalizationMap :
  Eq (α := at Submonoid.powers x)
    (Localization.mk (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)))
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (d + e)) ⋯))
    1
⊢ val
      (HMul.hMul (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x)
        z) =
    val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) 1

Tactic:
simp only [val_mul, val_one, awayMap_mk, Away.val_mk, z, Localization.mk_mul]

Premises used: HomogeneousLocalization.awayMap_mk, HomogeneousLocalization.val_one, HomogeneousLocalization.val_mul, HomogeneousLocalization.Away.val_mk, Localization.mk_mul
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
toIsLocalizationMap :
  ∃ (c : ↥(Submonoid.powers x)),
    (↑c : A) *
        ((↑(1, 1).2 : A) *
          (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                  (x ^ (d + e)) ⋯).1) =
      (↑c : A) *
        ((↑(g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e)
                      ⋯ *
                    Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                      (x ^ (d + e)) ⋯).2 :
            A) *
          (1, 1).1)
⊢ Eq (α := at Submonoid.powers x)
    (Localization.mk (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)))
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (d + e)) ⋯))
    1

Tactic:
rw [← Localization.mk_one, Localization.mk_eq_mk_iff, Localization.r_iff_exists]

Premises used: Localization.r_iff_exists, Localization.mk_one, Localization.mk_eq_mk_iff
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
h :
  (↑1 : A) *
      ((↑(1, 1).2 : A) *
        (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (d + e))
                ⋯).1) =
    (↑1 : A) *
      ((↑(g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                    (x ^ (d + e)) ⋯).2 :
          A) *
        (1, 1).1)
⊢ ∃ (c : ↥(Submonoid.powers x)),
    (↑c : A) *
        ((↑(1, 1).2 : A) *
          (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                  (x ^ (d + e)) ⋯).1) =
      (↑c : A) *
        ((↑(g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e)
                      ⋯ *
                    Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                      (x ^ (d + e)) ⋯).2 :
            A) *
          (1, 1).1)

Tactic:
use 1
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
h : g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)) = (f * g) ^ e * (f * g) ^ (d + e)
⊢ (↑1 : A) *
      ((↑(1, 1).2 : A) *
        (g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (d + e))
                ⋯).1) =
    (↑1 : A) *
      ((↑(g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)),
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ *
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                    (x ^ (d + e)) ⋯).2 :
          A) *
        (1, 1).1)

Tactic:
simp only [OneMemClass.coe_one, one_mul, Submonoid.coe_mul, mul_one, hx]

Premises used: OneMemClass.coe_one, mul_one, one_mul, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ g ^ d * g ^ e * (g ^ e * f ^ (2 * e + d)) = (f * g) ^ e * (f * g) ^ (d + e)

Tactic:
ring
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
z : Away 𝒜 x
toIsLocalizationMap :
  ∀ (n : ℕ) (s : A) (hs : s ∈ 𝒜 (n • (d + e))),
    ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
      HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
          ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
        (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
⊢ ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (β := Away 𝒜 x) z
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1

Tactic:
obtain ⟨n, s, hs, rfl⟩ := Away.mk_surjective 𝒜 (hx ▸ SetLike.mul_mem_graded hf hg) z

Premises used: HomogeneousLocalization.Away.mk_surjective, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
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) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
hs : s ∈ 𝒜 (n • (d + e))
toIsLocalizationMap :
  ∀ (hf : f ∈ 𝒜 0) (hd : Ne (α := ℕ) 0 0) (hs : s ∈ 𝒜 (n • (0 + e))),
    ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
      HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
          ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
        (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
toIsLocalizationMap₁ :
  ∀ (d : ℕ) (hf : f ∈ 𝒜 (d + 1)) (hd : d + 1 ≠ 0) (hs : s ∈ 𝒜 (n • (d + 1 + e))),
    ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
      HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
          ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
        (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
⊢ ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1

Tactic:
rcases d with - | d
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
hf : f ∈ 𝒜 0
hd : Ne (α := ℕ) 0 0
hs : s ∈ 𝒜 (n • (0 + e))
⊢ ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1

Tactic:
contradiction
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
⊢ s * g ^ (n * d) ∈ 𝒜 (n • (d + 1 + e) + (n * d) • e)

Tactic:
SetLike.mul_mem_graded hs (SetLike.pow_mem_graded _ hg)

Premises used: SetLike.mul_mem_graded, SetLike.pow_mem_graded
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
h : (n * (e + 1)) • (d + 1) = n • (d + 1 + e) + (n * d) • e
⊢ s * g ^ (n * d) ∈ 𝒜 ((n * (e + 1)) • (d + 1))

Tactic:
convert! SetLike.mul_mem_graded hs (SetLike.pow_mem_graded _ hg) using 2

Premises used: SetLike.mul_mem_graded, SetLike.pow_mem_graded
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
⊢ n * (e + 1) * (d + 1) = n * (d + 1 + e) + n * d * e

Tactic:
ring
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
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 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1

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

Premises used: Prod.mk, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
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)) ⋯
toIsLocalizationMap :
  HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
          (↑(t,
                  Subtype.mk (p := fun (x : Away 𝒜 f) ↦
                    Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
                    ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).2 :
            Away 𝒜 f) :
        Away 𝒜 x) =
    (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
      (t,
          Subtype.mk (p := fun (x : Away 𝒜 f) ↦
            Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
            ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).1
⊢ ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1

Tactic:
refine ⟨⟨t, ⟨_, ⟨n, rfl⟩⟩⟩, ?_⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
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)) ⋯
toIsLocalizationMap :
  val
      (HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
            (↑(t,
                    Subtype.mk (p := fun (x : Away 𝒜 f) ↦
                      Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
                      ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).2 :
              Away 𝒜 f) :
          Away 𝒜 x)) =
    val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
        (t,
            Subtype.mk (p := fun (x : Away 𝒜 f) ↦
              Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).1)
⊢ HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
          (↑(t,
                  Subtype.mk (p := fun (x : Away 𝒜 f) ↦
                    Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
                    ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).2 :
            Away 𝒜 f) :
        Away 𝒜 x) =
    (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
      (t,
          Subtype.mk (p := fun (x : Away 𝒜 f) ↦
            Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
            ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).1

Tactic:
ext
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
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)) ⋯
toIsLocalizationMap :
  Eq (α := at Submonoid.powers x)
    (Localization.mk (s * (g ^ (d + 1) * g ^ e) ^ n)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ n) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ e) ⋯ ^ n))
    (Localization.mk (s * g ^ (n * d) * g ^ (n * (e + 1)))
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (n * (e + 1)))
        ⋯))
⊢ val
      (HMul.hMul (α := Away 𝒜 x) (β := Away 𝒜 x) (Away.mk 𝒜 ⋯ n s hs)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
            (↑(t,
                    Subtype.mk (p := fun (x : Away 𝒜 f) ↦
                      Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
                      ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).2 :
              Away 𝒜 f) :
          Away 𝒜 x)) =
    val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
        (t,
            Subtype.mk (p := fun (x : Away 𝒜 f) ↦
              Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯).1)

Tactic:
simp only [RingHom.algebraMap_toAlgebra, map_pow, awayMap_mk, val_mul, val_mk, val_pow,
      Localization.mk_pow, Localization.mk_mul, t]

Premises used: HomogeneousLocalization.awayMap_mk, HomogeneousLocalization.val_pow, map_pow, HomogeneousLocalization.val_mul, HomogeneousLocalization.Away.val_mk, Localization.mk_pow, Localization.mk_mul, RingHom.algebraMap_toAlgebra