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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
h :
  Eq (α := Localization.Away x)
    (val
      (mk
        { deg := n + j • e, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n + j • e)) (a * g ^ j) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n + j • e)) (x ^ j) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers x) }))
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away 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 (α := Localization.Away x) (γ := Set (Localization.Away x))
    (Set.range (ι := HomogeneousLocalization 𝒜 (Submonoid.powers x)) val)
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away 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 := ⋯ }) :
      Localization.Away x)
have w : a * g ^ j ∈ 𝒜 (n + j • e)
Tactic: use mk ⟨n+j•e,⟨a*g^j, ?_⟩, ⟨x^j, ?_⟩, j, rfl⟩
-- 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
h :
  Eq (α := Localization.Away x)
    (val
      (mk
        { deg := n + j • e, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n + j • e)) (a * g ^ j) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n + j • e)) (x ^ j) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers x) }))
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away 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 := ⋯ }))
w : a * g ^ j ∈ 𝒜 (n + j • e)
⊢ Membership.mem (α := Localization.Away x) (γ := Set (Localization.Away x))
    (Set.range (ι := HomogeneousLocalization 𝒜 (Submonoid.powers x)) val)
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away 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 := ⋯ }) :
      Localization.Away x)
have w₁ : x ^ j ∈ 𝒜 (n + j • e)
Tactic: use mk ⟨n+j•e,⟨a*g^j, ?_⟩, ⟨x^j, ?_⟩, j, rfl⟩
-- 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
⊢ a * g ^ j ∈ 𝒜 (n + j • e)
have w : g ^ j ∈ 𝒜 (j • e)
Tactic: apply SetLike.mul_mem_graded 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
⊢ x ^ j ∈ 𝒜 (n + j • e)
have w : f ^ j * g ^ j ∈ 𝒜 (n + j • e)
Tactic: rw [hx, mul_pow]
-- 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
⊢ f ^ j * g ^ j ∈ 𝒜 (n + j • e)
have w : g ^ j ∈ 𝒜 (j • e)
Tactic: apply SetLike.mul_mem_graded hb'
-- 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 𝒜
e_1 : ι
f g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
e : Away 𝒜 x ≃+* ↥(RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) :=
  RingEquiv.ofLeftInverse (g :=
    Exists.choose (p := fun (finv : (at Submonoid.powers x) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) ↦
      Function.LeftInverse finv val) ⋯)
    ⋯
⊢ Away 𝒜 f →+* Away 𝒜 x
have refine : LE.le.{u_2} (α := Subring (Localization.Away x)) (RingHom.range (R := Away 𝒜 f) (awayMapAux 𝒜 sorry))
  (RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x)))
Tactic: refine RingHom.comp (e.symm.toRingHom.comp (Subring.inclusion ?_))
    (awayMapAux 𝒜 (f := f) ⟨_, hx⟩).rangeRestrict
-- 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 𝒜
e_1 : ι
f g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) :=
  RingEquiv.ofLeftInverse (g :=
    Exists.choose (p := fun (finv : (at Submonoid.powers x) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) ↦
      Function.LeftInverse finv val) ⋯)
    ⋯
⊢ Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (Exists.choose (p := fun (finv : (at Submonoid.powers x) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) ↦
        Function.LeftInverse finv val) ⋯
        (↑((Subring.inclusion ⋯ : (a : ↥(awayMapAux 𝒜 ⋯).range) → ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range)
              ((RingHom.rangeRestrict (awayMapAux 𝒜 ⋯) : (a : Away 𝒜 f) → ↥(awayMapAux 𝒜 ⋯).range) a)) :
          Localization.Away x)))
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a)
have convert_2 : Eq.{u_2 + 1} (α := Localization.Away x)
  ((↑((e : (a : Away 𝒜 x) → ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range)
          ((e.symm : (a : ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range) → Away 𝒜 x)
            (Subtype.mk (p := fun (x_1 : Localization.Away x) ↦
              Membership.mem (γ := Subring (Localization.Away x))
                (RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) x_1)
              ((awayMapAux 𝒜 sorry : (a : Away 𝒜 f) → Localization.Away x) a) sorry))) :
      Localization.Away x) :
    Localization.Away x)
  ((awayMapAux 𝒜 sorry : (a : Away 𝒜 f) → Localization.Away x) a : Localization.Away x)
Tactic: convert_to (e (e.symm ⟨awayMapAux 𝒜 (f := f) ⟨_, hx⟩ a,
    range_awayMapAux_subset 𝒜 hg hx ⟨_, rfl⟩⟩)).1 = _
-- 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 𝒜
e_1 : ι
f g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) :=
  RingEquiv.ofLeftInverse (g :=
    Exists.choose (p := fun (finv : (at Submonoid.powers x) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) ↦
      Function.LeftInverse finv val) ⋯)
    ⋯
⊢ Eq.{u_2 + 1} (α := Localization.Away x)
    ((↑((e : (a : Away 𝒜 x) → ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range)
            ((e.symm : (a : ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range) → Away 𝒜 x)
              (Subtype.mk (p := fun (x_1 : Localization.Away x) ↦
                Membership.mem (γ := Subring (Localization.Away x))
                  (RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) x_1)
                ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a) ⋯))) :
        Localization.Away x) :
      Localization.Away x)
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a : Localization.Away x)
have convert_2 : Eq.{u_2 + 1} (α := Localization.Away x)
  ((↑(Subtype.mk (p := fun (x_1 : Localization.Away x) ↦
          Membership.mem (γ := Subring (Localization.Away x))
            (RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) x_1)
          ((awayMapAux 𝒜 sorry : (a : Away 𝒜 f) → Localization.Away x) a) sorry) :
      Localization.Away x) :
    Localization.Away x)
  ((awayMapAux 𝒜 sorry : (a : Away 𝒜 f) → Localization.Away x) a : Localization.Away x)
Tactic: rw [e.apply_symm_apply]
-- 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : Away 𝒜 f
⊢ Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) a))
    ((Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯ :
        (a : Localization.Away f) → at Submonoid.powers x)
      (val a))
have rw : Eq.{u_2 + 1} (α := at Submonoid.powers x)
  ((awayMapAux 𝒜 sorry : (a : Away 𝒜 f) → Localization.Away x) a : Localization.Away x)
  ((Localization.awayLift (algebraMap A (at Submonoid.powers x)) f sorry :
        (a : Localization.Away f) → at Submonoid.powers x)
      (val a) :
    at Submonoid.powers x)
Tactic: rw [val_awayMap_eq_aux]
-- 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ Eq (α := Away 𝒜 x)
    ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x)
        ((fromZeroRingHom 𝒜 (Submonoid.powers f) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers f)) a) :
      Away 𝒜 x)
    ((fromZeroRingHom 𝒜 (Submonoid.powers x) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) a :
      HomogeneousLocalization 𝒜 (Submonoid.powers x))
have a₁ : Eq (α := at Submonoid.powers x)
  (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
    ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x)
      ((fromZeroRingHom 𝒜 (Submonoid.powers f) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers f)) a)))
  (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
    ((fromZeroRingHom 𝒜 (Submonoid.powers x) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) a))
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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x)
        ((fromZeroRingHom 𝒜 (Submonoid.powers f) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers f)) a)))
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((fromZeroRingHom 𝒜 (Submonoid.powers x) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) a))
have a₁ : Eq (α := at Submonoid.powers x)
  ((Localization.awayLift (algebraMap A (at Submonoid.powers x)) f sorry :
        (a : Localization.Away f) → at Submonoid.powers x)
      (Localization.mk (↑a : A)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (↑1 : A) sorry)) :
    at Submonoid.powers x)
  (Localization.mk (↑a : A)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (↑1 : A) sorry) :
    at Submonoid.powers x)
Tactic: simp only [fromZeroRingHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    val_awayMap, 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x)
        (mk { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ i) hi, den_mem := ⋯ })))
    (Localization.mk ((↑a : A) * g ^ i)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) ⋯))
have rw : Eq.{u_2 + 1} (α := at Submonoid.powers x)
  ((awayMapAux 𝒜 sorry : (a : Away 𝒜 f) → Localization.Away x)
      (mk { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ i) hi, den_mem := sorry }) :
    Localization.Away x)
  (Localization.mk ((↑a : A) * g ^ i)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) sorry) :
    at Submonoid.powers x)
Tactic: rw [val_awayMap_eq_aux, awayMapAux_mk 𝒜 (hx := 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
rw :
  Eq.{u_2 + 1} (α := at Submonoid.powers x)
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x)
        (mk { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ i) hi, den_mem := ⋯ }) :
      Localization.Away x)
    (Localization.mk ((↑a : A) * g ^ i)
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) ⋯) :
      at Submonoid.powers x)
⊢ Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x)
        (mk { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ i) hi, den_mem := ⋯ })))
    (Localization.mk ((↑a : A) * g ^ i)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) ⋯))
have rw₁ : Eq (α := at Submonoid.powers x)
  (Localization.mk ((↑a : A) * g ^ i)
    (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) sorry))
  (Localization.mk ((↑a : A) * g ^ i)
    (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) sorry))
Tactic: rw [val_awayMap_eq_aux, awayMapAux_mk 𝒜 (hx := 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ a * g ^ n ∈ 𝒜 (n • (d + e))
have rw : a * g ^ n ∈ 𝒜 (n • d + n • e)
Tactic: rw [smul_add]
-- 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ Eq (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha) : Away 𝒜 x)
    (Away.mk 𝒜 ⋯ n (a * g ^ n) ⋯ : Away 𝒜 x)
have a₁ : Eq (α := at Submonoid.powers x)
  (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha)))
  (val (Away.mk 𝒜 sorry n (a * g ^ n) sorry))
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 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
⊢ g ^ d ∈ 𝒜 (e • d)
have h : e • d = d • e
Tactic: convert! SetLike.pow_mem_graded d hg using 2
-- 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 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
⊢ IsLocalization.Away (R := Away 𝒜 f) (isLocalizationElem hf hg) (Away 𝒜 x)
have toIsLocalizationMap : Submonoid.IsLocalizationMap (M := Away 𝒜 f) (N := Away 𝒜 x) (Submonoid.powers (isLocalizationElem hf hg))
  (⇑(algebraMap (Away 𝒜 f) (Away 𝒜 x)) : (a : Away 𝒜 f) → Away 𝒜 x)
Tactic: constructor
-- 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 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
⊢ Submonoid.IsLocalizationMap (M := Away 𝒜 f) (N := Away 𝒜 x) (Submonoid.powers (isLocalizationElem hf hg))
    (⇑(algebraMap (Away 𝒜 f) (Away 𝒜 x)) : (a : Away 𝒜 f) → Away 𝒜 x)
have toIsLocalizationMap : ∀ (y : ↥(Submonoid.powers (isLocalizationElem hf hg))),
  IsUnit (M := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑y : Away 𝒜 f) : Away 𝒜 x)
Tactic: constructor
-- 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 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
toIsLocalizationMap :
  ∀ (y : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    IsUnit (M := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑y : Away 𝒜 f) : Away 𝒜 x)
⊢ Submonoid.IsLocalizationMap (M := Away 𝒜 f) (N := Away 𝒜 x) (Submonoid.powers (isLocalizationElem hf hg))
    (⇑(algebraMap (Away 𝒜 f) (Away 𝒜 x)) : (a : Away 𝒜 f) → Away 𝒜 x)
have toIsLocalizationMap₁ : ∀ (z : Away 𝒜 x),
  ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
    HMul.hMul (β := Away 𝒜 x) z
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
      (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
Tactic: constructor
-- 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 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
toIsLocalizationMap :
  ∀ (y : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    IsUnit (M := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑y : Away 𝒜 f) : Away 𝒜 x)
toIsLocalizationMap₁ :
  ∀ (z : Away 𝒜 x),
    ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
      HMul.hMul (β := Away 𝒜 x) z
          ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
        (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
⊢ Submonoid.IsLocalizationMap (M := Away 𝒜 f) (N := Away 𝒜 x) (Submonoid.powers (isLocalizationElem hf hg))
    (⇑(algebraMap (Away 𝒜 f) (Away 𝒜 x)) : (a : Away 𝒜 f) → Away 𝒜 x)
have toIsLocalizationMap₂ : ∀ {x_1 y : Away 𝒜 f},
  Eq (α := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1 : Away 𝒜 x)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) y : Away 𝒜 x) →
    ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))), (↑c : Away 𝒜 f) * x_1 = (↑c : Away 𝒜 f) * y
Tactic: constructor
-- 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 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
⊢ IsUnit (M := Away 𝒜 x)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
        (↑(Subtype.mk (p := fun (x : Away 𝒜 f) ↦
              Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯) :
          Away 𝒜 f) :
      Away 𝒜 x)
have toIsLocalizationMap : IsUnit
  (HPow.hPow (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x) n)
Tactic: rw [map_pow, RingHom.algebraMap_toAlgebra]
-- 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 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
⊢ g ^ e * f ^ (2 * e + d) ∈ 𝒜 ((d + e) • (d + e))
have h : (d + e) • (d + e) = e • e + (2 * e + d) • d
Tactic: convert!
        SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg)
          (SetLike.pow_mem_graded (2 * e + d) hf) using 2
-- 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 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
z : Away 𝒜 x := Away.mk 𝒜 (d := d + e) ⋯ (d + e) (g ^ e * f ^ (2 * e + d)) ⋯
⊢ IsUnit
    (HPow.hPow (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x) n)
have toIsLocalizationMap : HMul.hMul (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x) z = 1
Tactic: refine (isUnit_iff_exists_inv.mpr ⟨z, ?_⟩).pow _