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
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 := ⋯ })
have 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) sorry = 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 := sorry })
Tactic: by_cases hfj : f ^ j = 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
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 := ⋯ })
⊢ 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 := ⋯ })
have 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) sorry = 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 := sorry })
Tactic: by_cases hfj : f ^ j = 0
-- 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
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 := ⋯ })
have this : (((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)
-- 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
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
⊢ 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 := ⋯ })
have 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) 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: simp_rw [← this]
-- 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)) A) (Submodule.span ↥(𝒜 0) (↑(Submonoid.closure (Set.range v)) : Set A)) a
have rw : Membership.mem (γ := Submodule (↥(𝒜 0)) A)
  ((Subalgebra.toSubmodule : (a : Subalgebra (↥(𝒜 0)) A) → Submodule (↥(𝒜 0)) A) ⊤) a
Tactic: rw [← Algebra.adjoin_eq_span, hx]
-- 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
⊢ 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 this : 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
-- 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_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)
⊢ 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 : ∀ (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) sorry = 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 := sorry })
Tactic: obtain ⟨ai, rfl⟩ := Submonoid.exists_of_mem_closure_range _ _ ha'
Cleared hypotheses: a, ha'
-- 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 : ι' → ℕ
⊢ 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 := ⋯ })
have pos : ∀ (H : ∑ i : ι', ai i • dv i = 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) sorry = 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 := sorry })
Tactic: by_cases H : ∑ i, ai i • dv i = n
-- 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 : ι' → ℕ
pos :
  ∀ (H : ∑ i : ι', ai i • dv i = 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 := ((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)) (∏ i : ι', v i ^ ai i) : (a : ι) → ↥(𝒜 a)) n,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := ⋯ })
have neg : ∀ (H : ¬∑ i : ι', ai i • dv i = 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) sorry = 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 := sorry })
Tactic: by_cases H : ∑ i, ai i • dv i = n
-- 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
⊢ 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 := ⋯ })
have pos : Membership.mem (γ := Set (Away 𝒜 f))
  {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)) (∏ i : ι', v i ^ ai i) : (a : ι) → ↥(𝒜 a)) n,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ j) hb', den_mem := sorry })
Tactic: apply Submodule.subset_span
-- 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
⊢ Membership.mem (γ := Set (Away 𝒜 f))
    {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 := ⋯ })
have pos : n = j • d
Tactic: refine ⟨j, ai, H.trans ?_, ?_⟩
-- 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
pos : n = j • d
⊢ Membership.mem (γ := Set (Away 𝒜 f))
    {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 := ⋯ })
have pos₁ : Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf j (∏ i : ι', v i ^ ai i) sorry)
  (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 })
Tactic: refine ⟨j, ai, H.trans ?_, ?_⟩
-- 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) (Away.mk 𝒜 hf j (∏ i : ι', v i ^ ai i) ⋯)
    (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 := ⋯ })
have pos : Eq (α := at Submonoid.powers f) (val (Away.mk 𝒜 hf j (∏ i : ι', v i ^ ai i) sorry))
  (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) }))
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
⊢ Eq (α := at Submonoid.powers f) (val (Away.mk 𝒜 hf j (∏ i : ι', v i ^ ai i) ⋯))
    (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) }))
have pos : Eq (α := at Submonoid.powers f)
  (Localization.mk (∏ i : ι', v i ^ ai i)
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ j) sorry))
  (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) }))
Tactic: simp only [val_mk, Away.val_mk]
-- 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 (α := at Submonoid.powers f)
    (Localization.mk (∏ i : ι', v i ^ ai i)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ j) ⋯))
    (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) }))
have pos : ∏ i : ι', v i ^ ai i =
  (↑(NumDenSameDeg.num
        { 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) }) :
    A)
Tactic: congr
-- 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
⊢ ∏ i : ι', v i ^ ai i =
    (↑(NumDenSameDeg.num
          { 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) }) :
      A)
have pos : ∏ i : ι', v i ^ ai i ∈ 𝒜 n
Tactic: refine (DirectSum.decompose_of_mem_same _ ?_).symm
-- 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
⊢ 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 := ⋯ })
have h : 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 := sorry })
  0
Tactic: convert! zero_mem (Submodule.span (𝒜 0) _)