awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
⊢ Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
have a₁ : Eq (α := Localization.Away f)
  ((algebraMap (Away 𝒜 f) (Localization.Away f) : (a : Away 𝒜 f) → Localization.Away f)
      (Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry) :
    Localization.Away f)
  ((algebraMap (Away 𝒜 f) (Localization.Away f) : (a : Away 𝒜 f) → Localization.Away f)
      (HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) sorry)
        (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf sorry) (ai i / d))) :
    Localization.Away f)
Tactic: apply (show Function.Injective (algebraMap (Away 𝒜 f) (Localization.Away f))
      from val_injective _)
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
⊢ Eq (α := Localization.Away f)
    ((algebraMap (Away 𝒜 f) (Localization.Away f) : (a : Away 𝒜 f) → Localization.Away f)
        (Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯) :
      Localization.Away f)
    ((algebraMap (Away 𝒜 f) (Localization.Away f) : (a : Away 𝒜 f) → Localization.Away f)
        (HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
          (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))) :
      Localization.Away f)
have a₁ : (algebraMap (Away 𝒜 f) (Localization.Away f) : (a : Away 𝒜 f) → Localization.Away f)
    (Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry) =
  HMul.hMul (α := Localization.Away f) (β := Localization.Away f)
    ((algebraMap (Away 𝒜 f) (Localization.Away f) : (a : Away 𝒜 f) → Localization.Away f)
        (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) sorry) :
      Localization.Away f)
    (∏ x : ι',
        HPow.hPow (α := Localization.Away f)
          ((algebraMap (Away 𝒜 f) (Localization.Away f) : (a : Away 𝒜 f) → Localization.Away f)
              (isLocalizationElem hf sorry) :
            Localization.Away f)
          (ai x / d) :
      Localization.Away f)
Tactic: simp only [map_pow, map_prod, map_mul]
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
⊢ (algebraMap (Away 𝒜 f) (Localization.Away f) : (a : Away 𝒜 f) → Localization.Away f)
      (Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯) =
    HMul.hMul (α := Localization.Away f) (β := Localization.Away f)
      ((algebraMap (Away 𝒜 f) (Localization.Away f) : (a : Away 𝒜 f) → Localization.Away f)
          (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯) :
        Localization.Away f)
      (∏ x : ι',
          HPow.hPow (α := Localization.Away f)
            ((algebraMap (Away 𝒜 f) (Localization.Away f) : (a : Away 𝒜 f) → Localization.Away f)
                (isLocalizationElem hf ⋯) :
              Localization.Away f)
            (ai x / d) :
        Localization.Away f)
have a₁ : Eq.{u_2 + 1} (α := Localization.Away f)
  (Localization.mk (∏ i : ι', v i ^ ai i)
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ a) sorry))
  (Localization.mk (∏ x : ι', v x ^ (ai x % d + d * (ai x / d)))
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
        (f ^ (a - ∑ i : ι', dv i * (ai i / d))) sorry *
      ∏ i : ι',
        Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ dv i) sorry ^
          (ai i / d)))
Tactic: simp only [HomogeneousLocalization.algebraMap_apply, val_mk,
      Localization.mk_pow, Localization.mk_prod, Localization.mk_mul,
      ← Finset.prod_mul_distrib, ← pow_add, ← pow_mul]
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
⊢ Eq.{u_2 + 1} (α := Localization.Away f)
    (Localization.mk (∏ i : ι', v i ^ ai i)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ a) ⋯))
    (Localization.mk (∏ x : ι', v x ^ (ai x % d + d * (ai x / d)))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
          (f ^ (a - ∑ i : ι', dv i * (ai i / d))) ⋯ *
        ∏ i : ι',
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ dv i) ⋯ ^
            (ai i / d)))
have a₁ : Eq (α := ι' → A) (fun (i : ι') ↦ v i ^ ai i) fun (x : ι') ↦ v x ^ (ai x % d + d * (ai x / d))
Tactic: congr
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
a₁ : Eq (α := ι' → A) (fun (i : ι') ↦ v i ^ ai i) fun (x : ι') ↦ v x ^ (ai x % d + d * (ai x / d))
⊢ Eq.{u_2 + 1} (α := Localization.Away f)
    (Localization.mk (∏ i : ι', v i ^ ai i)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ a) ⋯))
    (Localization.mk (∏ x : ι', v x ^ (ai x % d + d * (ai x / d)))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
          (f ^ (a - ∑ i : ι', dv i * (ai i / d))) ⋯ *
        ∏ i : ι',
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ dv i) ⋯ ^
            (ai i / d)))
have a₂ : f ^ a =
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
          (f ^ (a - ∑ i : ι', dv i * (ai i / d))) sorry) :
      A) *
    (↑(∏ i : ι',
          Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ dv i) sorry ^
            (ai i / d)) :
      A)
Tactic: congr
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
⊢ Eq (α := ι' → A) (fun (i : ι') ↦ v i ^ ai i) fun (x : ι') ↦ v x ^ (ai x % d + d * (ai x / d))
have a₁ : ∀ (i : ι'), v i ^ ai i = v i ^ (ai i % d + d * (ai i / d))
Tactic: ext 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
i : ι'
⊢ v i ^ ai i = v i ^ (ai i % d + d * (ai i / d))
have a₁ : ai i = ai i % d + d * (ai i / d)
Tactic: congr
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
⊢ f ^ a =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
            (f ^ (a - ∑ i : ι', dv i * (ai i / d))) ⋯) :
        A) *
      (↑(∏ i : ι',
            Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ dv i) ⋯ ^
              (ai i / d)) :
        A)
have a₁ : f ^ a = f ^ (a - ∑ i : ι', dv i * (ai i / d) + ∑ i : ι', dv i * (ai i / d))
Tactic: simp only [SubmonoidClass.coe_finsetProd, ← pow_add, ← pow_mul,
        Finset.prod_pow_eq_pow_sum, SubmonoidClass.coe_pow]
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
⊢ f ^ a = f ^ (a - ∑ i : ι', dv i * (ai i / d) + ∑ i : ι', dv i * (ai i / d))
have a₁ : ∑ i : ι', dv i * (ai i / d) ≤ a
Tactic: rw [tsub_add_cancel_of_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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
⊢ ∑ i : ι', dv i * (ai i / d) ≤ a
have a₁ : ∀ (hd : d = 0), ∑ i : ι', dv i * (ai i / d) ≤ a
Tactic: rcases d.eq_zero_or_pos with hd | hd
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
a₁ : ∀ (hd : d = 0), ∑ i : ι', dv i * (ai i / d) ≤ a
⊢ ∑ i : ι', dv i * (ai i / d) ≤ a
have a₂ : ∀ (hd : d > 0), ∑ i : ι', dv i * (ai i / d) ≤ a
Tactic: rcases d.eq_zero_or_pos with hd | hd
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
hd : d > 0
⊢ ∑ i : ι', dv i * (ai i / d) ≤ a
have a₁ : LE.le (α := ℕ) (∑ i : ι', dv i * (ai i / d) * d) (∑ i : ι', ai i • dv i)
Tactic: rw [← mul_le_mul_iff_of_pos_right hd, ← smul_eq_mul (a := a), ← hai, Finset.sum_mul]
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
hd : d > 0
⊢ LE.le (α := ℕ) (∑ i : ι', dv i * (ai i / d) * d) (∑ i : ι', ai i • dv i)
have a₁ : LE.le (α := ℕ) (∑ x : ι', dv x * (ai x / d * d)) (∑ x : ι', dv x * ai x)
Tactic: simp_rw [smul_eq_mul, mul_comm (ai _), mul_assoc]
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
hd : d > 0
⊢ LE.le (α := ℕ) (∑ x : ι', dv x * (ai x / d * d)) (∑ x : ι', dv x * ai x)
have a₁ : ∀ (i : ι'), Membership.mem (γ := Finset ι') Finset.univ i → ai i / d * d ≤ ai i
Tactic: gcongr
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
⊢ 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 : Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry =
  HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) sorry)
    (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf sorry) (ai i / d))
Tactic: have H : Away.mk 𝒜 hf a (∏ i, v i ^ ai i)
      (hai ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i) =
      Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i, v i ^ (ai i % d))
      (H₀ ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i) *
      ∏ i, Away.isLocalizationElem hf (hxd i) ^ (ai i / d) := by
    apply (show Function.Injective (algebraMap (Away 𝒜 f) (Localization.Away f))
      from val_injective _)
    simp only [map_pow, map_prod, map_mul]
    simp only [HomogeneousLocalization.algebraMap_apply, val_mk,
      Localization.mk_pow, Localization.mk_prod, Localization.mk_mul,
      ← Finset.prod_mul_distrib, ← pow_add, ← pow_mul]
    congr
    · ext i
      congr
      exact Eq.symm (Nat.mod_add_div (ai i) d)
    · simp only [SubmonoidClass.coe_finsetProd, ← pow_add, ← pow_mul,
        Finset.prod_pow_eq_pow_sum, SubmonoidClass.coe_pow]
      rw [tsub_add_cancel_of_le]
      rcases d.eq_zero_or_pos with hd | hd
      · simp [hd]
      rw [← mul_le_mul_iff_of_pos_right hd, ← smul_eq_mul (a := a), ← hai, Finset.sum_mul]
      simp_rw [smul_eq_mul, mul_comm (ai _), mul_assoc]
      gcongr
      exact Nat.div_mul_le_self (ai _) 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / 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 rw : Membership.mem (γ := 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) sorry = x}) :
    Submodule (↥(𝒜 0)) (Away 𝒜 f))
  (HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) sorry)
    (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf sorry) (ai i / d)))
Tactic: rw [H, SetLike.mem_coe]
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
⊢ Membership.mem (γ := 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))
    (HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d)))
have hx₁ : Membership.mem (γ := 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})
  (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) sorry)
Tactic: apply (Algebra.adjoin (𝒜 0) _).mul_mem
-- 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
H₀ : (a - ∑ i : ι', dv i * (ai i / d)) • d = ∑ k : ι', (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ =
    HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d))
hx₁ :
  Membership.mem (γ := 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})
    (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
⊢ Membership.mem (γ := 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))
    (HMul.hMul (α := Away 𝒜 f) (Away.mk 𝒜 hf (a - ∑ i : ι', dv i * (ai i / d)) (∏ i : ι', v i ^ (ai i % d)) ⋯)
      (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf ⋯) (ai i / d)))
have hy : Membership.mem (γ := 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})
  (∏ i : ι', HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf sorry) (ai i / d))
Tactic: apply (Algebra.adjoin (𝒜 0) _).mul_mem