awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
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
ai : ι' → ℕ
H : ¬∑ i : ι', ai i • dv i = n
⊢ Eq (α := Away 𝒜 f)
    (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 := ⋯ })
    0
have h : Eq (α := at Submonoid.powers f)
  (val
    (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 := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) }))
  (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
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
ai : ι' → ℕ
H : ¬∑ i : ι', ai i • dv i = n
⊢ (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (∏ i : ι', v i ^ ai i) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
have refine : ∏ i : ι', v i ^ ai i ∈ 𝒜 (∑ i : ι', ai i • dv i)
Tactic: refine DirectSum.decompose_of_mem_ne _ ?_ H
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (hypothesis)
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
ai : ι' → ℕ
H : ¬∑ i : ι', ai i • dv i = n
⊢ Eq (α := at Submonoid.powers f)
    (val
      (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 := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) }))
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) 0)
have this : (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (∏ i : ι', v i ^ ai i) : (a : ι) → ↥(𝒜 a)) n) : A) = 0
Tactic: have : (DirectSum.decompose 𝒜 (∏ i : ι', v i ^ ai i) n).1 = 0 := by
        refine DirectSum.decompose_of_mem_ne _ ?_ H
        exact SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
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)) (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)) 0 : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
have h : Eq (α := Away 𝒜 f)
  (mk
    { deg := n, num := ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) n,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry })
  0
Tactic: convert! zero_mem (Submodule.span (𝒜 0) _)
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
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
⊢ Eq (α := Away 𝒜 f)
    (mk
      { deg := n, num := ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
    0
have h : Eq (α := at Submonoid.powers f)
  (val
    (mk
      { deg := n, num := ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) }))
  (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
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
s t : A
hs : Membership.mem (γ := Submodule (↥(𝒜 0)) A) (Submodule.span ↥(𝒜 0) (↑(Submonoid.closure (Set.range v)) : Set A)) s
ht : Membership.mem (γ := Submodule (↥(𝒜 0)) A) (Submodule.span ↥(𝒜 0) (↑(Submonoid.closure (Set.range v)) : Set A)) t
hs' :
  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)) s : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
ht' :
  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)) t : ⨁ (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 := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (s + t) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
have h : mk
    { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (s + t) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry } =
  HAdd.hAdd (α := Away 𝒜 f)
    (mk
      { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) s : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) })
    (mk
      { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) t : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) })
Tactic: convert! add_mem hs' ht'
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
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_1 : 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
r : ↥(𝒜 0)
x : A
hx : Membership.mem (γ := Submodule (↥(𝒜 0)) A) (Submodule.span ↥(𝒜 0) (↑(Submonoid.closure (Set.range v)) : Set A)) x
hx' :
  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)) x : ⨁ (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 := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (r • x) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
have h : mk
    { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (r • x) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry } =
  HSMul.hSMul (β := Away 𝒜 f) r
    (mk
      { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) })
Tactic: convert! Submodule.smul_mem _ r hx'
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
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_1 : 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
r : ↥(𝒜 0)
x : A
hx : Membership.mem (γ := Submodule (↥(𝒜 0)) A) (Submodule.span ↥(𝒜 0) (↑(Submonoid.closure (Set.range v)) : Set A)) x
hx' :
  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)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
⊢ mk
      { deg := n,
        num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (r • x) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ } =
    HSMul.hSMul (β := Away 𝒜 f) r
      (mk
        { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
have h : val
    (mk
      { deg := n,
        num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (r • x) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) }) =
  val
    (HSMul.hSMul (β := Away 𝒜 f) r
      (mk
        { deg := n, num := (((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry :
          NumDenSameDeg 𝒜 (Submonoid.powers f) }))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
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
this : Membership.mem (γ := Submodule (↥(𝒜 0)) A) (Submodule.span ↥(𝒜 0) (↑(Submonoid.closure (Set.range v)) : Set A)) 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)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
have neg : ∀ (a : A) (ha' : a ∈ (↑(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) sorry = 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 := sorry })
Tactic: induction this using Submodule.span_induction with
  | mem a ha' =>
    obtain ⟨ai, rfl⟩ := Submonoid.exists_of_mem_closure_range _ _ ha'
    clear ha'
    by_cases H : ∑ i, ai i • dv i = n
    · apply Submodule.subset_span
      refine ⟨j, ai, H.trans ?_, ?_⟩
      · exact DirectSum.degree_eq_of_mem_mem 𝒜 hb'
          (SetLike.pow_mem_graded j hf) hfj
      · ext
        simp only [val_mk, Away.val_mk]
        congr
        refine (DirectSum.decompose_of_mem_same _ ?_).symm
        exact H ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i
    · convert! zero_mem (Submodule.span (𝒜 0) _)
      ext
      have : (DirectSum.decompose 𝒜 (∏ i : ι', v i ^ ai i) n).1 = 0 := by
        refine DirectSum.decompose_of_mem_ne _ ?_ H
        exact SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i
      simp [this, Localization.mk_zero]
  | zero =>
    convert! zero_mem (Submodule.span (𝒜 0) _)
    ext; simp [Localization.mk_zero]
  | add s t hs ht hs' ht' =>
    convert! add_mem hs' ht'
    ext; simp [← Localization.add_mk_self]
  | smul r x hx hx' =>
    convert! Submodule.smul_mem _ r hx'
    ext
    simp [Algebra.smul_def, algebraMap_eq, fromZeroRingHom, Localization.mk_mul,
      -decompose_mul, coe_decompose_mul_of_left_mem_zero 𝒜 r.2]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
⊢ Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f))
    (Algebra.adjoin ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    ⊤
have rw : LE.le.{u_2} (α := Subalgebra (↥(𝒜 0)) (Away 𝒜 f)) ⊤
  (Algebra.adjoin ↥(𝒜 0)
    {x : Away 𝒜 f |
      ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
        Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x})
Tactic: rw [← top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
⊢ LE.le.{u_2} (α := Submodule (↥(𝒜 0)) (Away 𝒜 f)) (⊤ : Submodule (↥(𝒜 0)) (Away 𝒜 f))
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(𝒜 0)) (Away 𝒜 f)) → Submodule (↥(𝒜 0)) (Away 𝒜 f))
        (Algebra.adjoin ↥(𝒜 0)
          {x : Away 𝒜 f |
            ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
              Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x}) :
      Submodule (↥(𝒜 0)) (Away 𝒜 f))
have rw : {x : Away 𝒜 f |
    ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x} ⊆
  (↑((Subalgebra.toSubmodule : (a : Subalgebra (↥(𝒜 0)) (Away 𝒜 f)) → Submodule (↥(𝒜 0)) (Away 𝒜 f))
          (Algebra.adjoin ↥(𝒜 0)
            {x : Away 𝒜 f |
              ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
                Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x}) :
        Submodule (↥(𝒜 0)) (Away 𝒜 f)) :
    Set (Away 𝒜 f))
Tactic: rw [← HomogeneousLocalization.Away.span_mk_prod_pow_eq_top hf v hx dv hxd, Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
⊢ (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
have rw : ∑ i : ι', ai i • dv i - (∑ i : ι', dv i * (ai i / d)) * d = ∑ k : ι', (ai k % d) • dv k
Tactic: rw [smul_eq_mul, tsub_mul, ← smul_eq_mul, ← hai]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
| ∑ i : ι', ai i • dv i - (∑ i : ι', dv i * (ai i / d)) * d = ∑ k : ι', (ai k % d) • dv k
have h : ∀ (i : ι'), ai i • dv i
Tactic: enter [1, 1, 2, i]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
i : ι'
| ai i • dv i
have h : (ai i % d + d * (ai i / d)) • dv i
Tactic: rw [← Nat.mod_add_div (ai i) d]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
| ∑ i : ι', ai i • dv i - (∑ i : ι', dv i * (ai i / d)) * d = ∑ k : ι', (ai k % d) • dv k
have h : ∀ (i : ι'), (ai i % d + d * (ai i / d)) • dv i
Tactic: enter [1, 1, 2, i]; rw [← Nat.mod_add_div (ai i) d]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
⊢ ∑ i : ι', ai i • dv i - (∑ i : ι', dv i * (ai i / d)) * d = ∑ k : ι', (ai k % d) • dv k
have conv : ∑ i : ι', (ai i % d + d * (ai i / d)) • dv i - (∑ i : ι', dv i * (ai i / d)) * d = ∑ k : ι', (ai k % d) • dv k
Tactic: conv => enter [1, 1, 2, i]; rw [← Nat.mod_add_div (ai i) d]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
⊢ ∑ i : ι', (ai i % d + d * (ai i / d)) • dv i - (∑ i : ι', dv i * (ai i / d)) * d = ∑ k : ι', (ai k % d) • dv k
have simp_rw : ∑ x : ι', ai x % d * dv x + (∑ x : ι', dv x * (ai x / d)) * d - (∑ i : ι', dv i * (ai i / d)) * d =
  ∑ x : ι', ai x % d * dv x
Tactic: simp_rw [smul_eq_mul, add_mul, Finset.sum_add_distrib,
      mul_assoc, ← Finset.mul_sum, mul_comm d, mul_comm (_ / _)]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (hypothesis)
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_4 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i : ι', ai i • dv i = a • d
⊢ Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ ∈
    (↑((Subalgebra.toSubmodule : (a : Subalgebra (↥(𝒜 0)) (Away 𝒜 f)) → Submodule (↥(𝒜 0)) (Away 𝒜 f))
            (Algebra.adjoin ↥(𝒜 0)
              {x : Away 𝒜 f |
                ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
                  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x}) :
          Submodule (↥(𝒜 0)) (Away 𝒜 f)) :
      Set (Away 𝒜 f))
have H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
Tactic: have H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k := by
    rw [smul_eq_mul, tsub_mul, ← smul_eq_mul, ← hai]
    conv => enter [1, 1, 2, i]; rw [← Nat.mod_add_div (ai i) d]
    simp_rw [smul_eq_mul, add_mul, Finset.sum_add_distrib,
      mul_assoc, ← Finset.mul_sum, mul_comm d, mul_comm (_ / _)]
    simp only [add_tsub_cancel_right]