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 : ℕ
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 :
  ∃ (c : ↥(Submonoid.powers x)),
    (↑c : A) *
        ((↑(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))) ⋯).2 :
            A) *
          (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).1) =
      (↑c : A) *
        ((↑(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).2 :
            A) *
          (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))) ⋯).1)
⊢ 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)))
        ⋯))

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

Premises used: Localization.r_iff_exists, 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 : ℕ
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)) ⋯
simp : x ^ (n * (e + 1)) * (s * (g ^ (d + 1) * g ^ e) ^ n) = x ^ n * (x ^ e) ^ n * (s * g ^ (n * d) * g ^ (n * (e + 1)))
⊢ (↑1 : A) *
      ((↑(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))) ⋯).2 :
          A) *
        (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).1) =
    (↑1 : A) *
      ((↑(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).2 :
          A) *
        (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))) ⋯).1)

Tactic:
simp
-- 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 ^ (n * (e + 1)) * (s * (g ^ (d + 1) * g ^ e) ^ n) = x ^ n * (x ^ e) ^ n * (s * g ^ (n * d) * g ^ (n * (e + 1)))

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)) ⋯
⊢ ∃ (c : ↥(Submonoid.powers x)),
    (↑c : A) *
        ((↑(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))) ⋯).2 :
            A) *
          (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).1) =
      (↑c : A) *
        ((↑(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).2 :
            A) *
          (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))) ⋯).1)

Tactic:
exact ⟨1, by simp; 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_1 d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
a b : Away 𝒜 f
e :
  Eq (α := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) a : Away 𝒜 x)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) b : Away 𝒜 x)
toIsLocalizationMap :
  ∀ (n : ℕ) (a : A) (ha : a ∈ 𝒜 (n • d))
    (e :
      Eq (α := Away 𝒜 x)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha) : Away 𝒜 x)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) b : Away 𝒜 x)),
    ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))), (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * b
⊢ ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))), (↑c : Away 𝒜 f) * a = (↑c : Away 𝒜 f) * b

Tactic:
obtain ⟨n, a, ha, rfl⟩ := Away.mk_surjective 𝒜 hf a

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_1 d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
b : Away 𝒜 f
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
e :
  Eq (α := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha) : Away 𝒜 x)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) b : Away 𝒜 x)
toIsLocalizationMap :
  ∀ (m : ℕ) (b : A) (hb : b ∈ 𝒜 (m • d))
    (e :
      Eq (α := Away 𝒜 x)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha) : Away 𝒜 x)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf m b hb) : Away 𝒜 x)),
    ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))),
      (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * Away.mk 𝒜 hf m b hb
⊢ ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))), (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * b

Tactic:
obtain ⟨m, b, hb, rfl⟩ := Away.mk_surjective 𝒜 hf b

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_1 d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
e :
  Eq (α := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha) : Away 𝒜 x)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf m b hb) : Away 𝒜 x)
⊢ Eq (α := at Submonoid.powers x)
    (val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha)))
    (val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf m b hb)))

Tactic:
replace e := congr_arg val e
-- 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_1 d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
e :
  Eq (α := at Submonoid.powers x)
    (val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha)))
    (val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf m b hb)))
⊢ ∃ (c : ↥(Submonoid.powers x)), (↑c : A) * (x ^ m * (a * g ^ n)) = (↑c : A) * (x ^ n * (b * g ^ m))

Tactic:
simp only [RingHom.algebraMap_toAlgebra, awayMap_mk, val_mk,
      Localization.mk_eq_mk_iff, Localization.r_iff_exists] at e

Premises used: HomogeneousLocalization.awayMap_mk, Localization.r_iff_exists, HomogeneousLocalization.Away.val_mk, RingHom.algebraMap_toAlgebra, 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_1 d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
e : ∃ (c : ↥(Submonoid.powers x)), (↑c : A) * (x ^ m * (a * g ^ n)) = (↑c : A) * (x ^ n * (b * g ^ m))
toIsLocalizationMap :
  ∀ (k : ℕ)
    (hc :
      (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
            A) *
          (x ^ m * (a * g ^ n)) =
        (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
            A) *
          (x ^ n * (b * g ^ m))),
    ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))),
      (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * Away.mk 𝒜 hf m b hb
⊢ ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * Away.mk 𝒜 hf m b hb

Tactic:
obtain ⟨⟨_, k, rfl⟩, hc⟩ := e

Premises used: 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
⊢ ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * Away.mk 𝒜 hf m b hb

Tactic:
⟨⟨_, k + m + n, rfl⟩, ?_⟩

Premises used: Subtype.mk, HAdd.hAdd, 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 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
toIsLocalizationMap :
  (↑(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) (k + m + n)) ⋯) :
        Away 𝒜 f) *
      Away.mk 𝒜 hf n a ha =
    (↑(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) (k + m + n)) ⋯) :
        Away 𝒜 f) *
      Away.mk 𝒜 hf m b hb
⊢ ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * Away.mk 𝒜 hf m b hb

Tactic:
refine ⟨⟨_, k + m + 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 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
toIsLocalizationMap :
  val
      ((↑(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) (k + m + n)) ⋯) :
          Away 𝒜 f) *
        Away.mk 𝒜 hf n a ha) =
    val
      ((↑(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) (k + m + n)) ⋯) :
          Away 𝒜 f) *
        Away.mk 𝒜 hf m b hb)
⊢ (↑(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) (k + m + n)) ⋯) :
        Away 𝒜 f) *
      Away.mk 𝒜 hf n a ha =
    (↑(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) (k + m + n)) ⋯) :
        Away 𝒜 f) *
      Away.mk 𝒜 hf m b hb

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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
toIsLocalizationMap :
  ∃ (a_1 : A),
    Membership.mem (γ := Submonoid A) (Submonoid.powers f) a_1 ∧
      a_1 * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
        a_1 * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))
⊢ val
      ((↑(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) (k + m + n)) ⋯) :
          Away 𝒜 f) *
        Away.mk 𝒜 hf n a ha) =
    val
      ((↑(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) (k + m + n)) ⋯) :
          Away 𝒜 f) *
        Away.mk 𝒜 hf m b hb)

Tactic:
simp only [val_mul, val_pow, val_mk, Localization.mk_pow,
      Localization.mk_eq_mk_iff, Localization.r_iff_exists, Submonoid.coe_mul, Localization.mk_mul,
      SubmonoidClass.coe_pow, Subtype.exists, exists_prop]

Premises used: HomogeneousLocalization.val_pow, Subtype.exists, HomogeneousLocalization.val_mul, exists_prop, Localization.r_iff_exists, HomogeneousLocalization.Away.val_mk, Localization.mk_pow, SubmonoidClass.coe_pow, Localization.mk_mul, Submonoid.coe_mul, 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
⊢ ∃ (a_1 : A),
    Membership.mem (γ := Submonoid A) (Submonoid.powers f) a_1 ∧
      a_1 * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
        a_1 * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))

Tactic:
⟨_, ⟨k, rfl⟩, ?_⟩

Premises used: And.intro, 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 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
toIsLocalizationMap :
  (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))
⊢ ∃ (a_1 : A),
    Membership.mem (γ := Submonoid A) (Submonoid.powers f) a_1 ∧
      a_1 * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
        a_1 * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))

Tactic:
refine ⟨_, ⟨k, 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
toIsLocalizationMap :
  ∀ (hf : f ∈ 𝒜 0) (hd : Ne (α := ℕ) 0 0) (ha : a ∈ 𝒜 (HSMul.hSMul (β := ℕ) n 0))
    (hb : b ∈ 𝒜 (HSMul.hSMul (β := ℕ) m 0)),
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * (HPow.hPow (β := ℕ) g 0 ^ (k + m + n) * a)) =
      (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * (HPow.hPow (β := ℕ) g 0 ^ (k + m + n) * b))
toIsLocalizationMap₁ :
  ∀ (d : ℕ) (hf : f ∈ 𝒜 (d + 1)) (hd : d + 1 ≠ 0) (ha : a ∈ 𝒜 (n • (d + 1))) (hb : b ∈ 𝒜 (m • (d + 1))),
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
      (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))
⊢ (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))

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 : ℕ
a : A
m : ℕ
b : A
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
hf : f ∈ 𝒜 0
hd : Ne (α := ℕ) 0 0
ha : a ∈ 𝒜 (HSMul.hSMul (β := ℕ) n 0)
hb : b ∈ 𝒜 (HSMul.hSMul (β := ℕ) m 0)
⊢ (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * (HPow.hPow (β := ℕ) g 0 ^ (k + m + n) * a)) =
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * (HPow.hPow (β := ℕ) g 0 ^ (k + m + n) * b))

Tactic:
contradiction