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 : ℕ
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))
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ n * (b * g ^ m))

Tactic:
subst hx
-- 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
n : ℕ
a : A
m : ℕ
b : A
k d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := RingHom.toAlgebra (awayMap 𝒜 hg ⋯)
hc :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ n * (b * g ^ m))
⊢ f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) *
      ((↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
              ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
          A) *
        ((f * g) ^ m * (a * g ^ n))) =
    f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) *
      ((↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
              ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
          A) *
        ((f * g) ^ n * (b * g ^ m)))

Tactic:
congr(f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) * $hc)

Premises used: HMul.hMul, congrArg, id, HPow.hPow, HAdd.hAdd
-- 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
n : ℕ
a : A
m : ℕ
b : A
k d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := RingHom.toAlgebra (awayMap 𝒜 hg ⋯)
hc :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ n * (b * g ^ m))
h :
  (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) *
      ((↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
              ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
          A) *
        ((f * g) ^ m * (a * g ^ n)))
h₁ :
  (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b)) =
    f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) *
      ((↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
              ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
          A) *
        ((f * g) ^ n * (b * g ^ m)))
⊢ (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))

Tactic:
convert! congr(f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) * $hc) using 1

Premises used: HMul.hMul, HAdd.hAdd
-- 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
n : ℕ
a : A
m : ℕ
b : A
k d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := RingHom.toAlgebra (awayMap 𝒜 hg ⋯)
hc :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ n * (b * g ^ m))
⊢ (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) *
      ((↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
              ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
          A) *
        ((f * g) ^ m * (a * g ^ n)))

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
n : ℕ
a : A
m : ℕ
b : A
k d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := RingHom.toAlgebra (awayMap 𝒜 hg ⋯)
hc :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ n * (b * g ^ m))
⊢ (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b)) =
    f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) *
      ((↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
              ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
          A) *
        ((f * g) ^ n * (b * g ^ m)))

Tactic:
ring
-- 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
pos :
  ∀ (HH : Subsingleton (Away 𝒜 f)),
    Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
      (Submodule.span ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      ⊤
neg :
  ∀ (HH : ¬Subsingleton (Away 𝒜 f)),
    Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
      (Submodule.span ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      ⊤
⊢ Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    ⊤

Tactic:
by_cases HH : Subsingleton (HomogeneousLocalization.Away 𝒜 f)

Premises used: Subsingleton, HomogeneousLocalization.Away
-- 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : Subsingleton (Away 𝒜 f)
⊢ Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    ⊤

Tactic:
Subsingleton.elim _ _

Premises used: 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : Subsingleton (Away 𝒜 f)
⊢ Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    ⊤

Tactic:
exact Subsingleton.elim _ _

Premises used: 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
neg :
  LE.le (α := Submodule (↥(𝒜 0)) (Away 𝒜 f)) ⊤
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
⊢ Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
x : Away 𝒜 f
neg :
  ∀ (n : ι) (a : A) (ha : a ∈ 𝒜 n) (j : ℕ) (hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n),
    Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
      (Submodule.span ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      (mk
        { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x : ℕ) ↦ f ^ x) j) hb', den_mem := ⋯ })
⊢ Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    x

Tactic:
obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, ⟨j, (rfl : _ = b)⟩⟩, rfl⟩ := mk_surjective x

Premises used: HomogeneousLocalization.mk_surjective, 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
pos :
  ∀ (hfj : f ^ j = 0),
    Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
      (Submodule.span ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      (mk
        { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x : ℕ) ↦ f ^ x) j) hb', den_mem := ⋯ })
neg :
  ∀ (hfj : ¬f ^ j = 0),
    Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
      (Submodule.span ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      (mk
        { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x : ℕ) ↦ f ^ x) j) hb', den_mem := ⋯ })
⊢ Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (mk
      { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x : ℕ) ↦ f ^ x) j) hb', den_mem := ⋯ })

Tactic:
by_cases hfj : f ^ j = 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
hfj : f ^ j = 0
⊢ Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (mk
      { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x : ℕ) ↦ f ^ x) j) hb', den_mem := ⋯ })

Tactic:
(HH (HomogeneousLocalization.subsingleton _ ⟨_, hfj⟩)).elim

Premises used: HomogeneousLocalization.subsingleton, False.elim, Exists.intro
-- 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
hfj : f ^ j = 0
⊢ Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (mk
      { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x : ℕ) ↦ f ^ x) j) hb', den_mem := ⋯ })

Tactic:
exact (HH (HomogeneousLocalization.subsingleton _ ⟨_, hfj⟩)).elim

Premises used: HomogeneousLocalization.subsingleton, False.elim, Exists.intro
-- 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
⊢ (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n =
    Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha

Tactic:
have : DirectSum.decompose 𝒜 a n = ⟨a, ha⟩ := Subtype.ext (DirectSum.decompose_of_mem_same 𝒜 ha)
-- 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
this :
  (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n =
    Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha
neg :
  Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (mk
      { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
⊢ Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (mk
      { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x : ℕ) ↦ f ^ x) j) hb', den_mem := ⋯ })

Tactic:
simp_rw [← this]
-- 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
rw :
  Membership.mem (γ := Submodule (↥(𝒜 0)) A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(𝒜 0)) A) → Submodule (↥(𝒜 0)) A) ⊤) a
⊢ Membership.mem (γ := Submodule (↥(𝒜 0)) A) (Submodule.span ↥(𝒜 0) (↑(Submonoid.closure (Set.range v)) : Set A)) a

Tactic:
rw [← Algebra.adjoin_eq_span, hx]

Premises used: Algebra.adjoin_eq_span
-- 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
⊢ Membership.mem (γ := Submodule (↥(𝒜 0)) A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(𝒜 0)) A) → Submodule (↥(𝒜 0)) A) ⊤) a

Tactic:
trivial
-- 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
⊢ Membership.mem (γ := Submodule (↥(𝒜 0)) A) (Submodule.span ↥(𝒜 0) (↑(Submonoid.closure (Set.range v)) : Set A)) a

Tactic:
have : a ∈ Submodule.span (𝒜 0) (Submonoid.closure (Set.range v)) := by
    rw [← Algebra.adjoin_eq_span, hx]
    trivial
-- 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
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a_1 : A
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
a : A
ha' : a ∈ (↑(Submonoid.closure (Set.range v)) : Set A)
neg :
  ∀ (ai : ι' → ℕ) (ha' : ∏ i : ι', v i ^ ai i ∈ (↑(Submonoid.closure (Set.range v)) : Set A)),
    Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
      (Submodule.span ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      (mk
        { deg := n, num := ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (∏ i : ι', v i ^ ai i) : (a : ι) → ↥(𝒜 a)) n,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
⊢ Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    (mk
      { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })

Tactic:
obtain ⟨ai, rfl⟩ := Submonoid.exists_of_mem_closure_range _ _ ha'

Premises used: Submonoid.exists_of_mem_closure_range, rfl