awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
s : A
x : Away 𝒜 s
⊢ Eq (α := Away.{u_1, u_6, u_7} (A := C) 𝒞 ((g : (a : B) → C) ((f : (a : A) → B) s : B) : C))
    ((Away.map g ((f : (a : A) → B) s) :
          (a : Away ℬ ((f : (a : A) → B) s)) → Away 𝒞 ((g : (a : B) → C) ((f : (a : A) → B) s)))
        ((Away.map f s : (a : Away 𝒜 s) → Away ℬ ((f : (a : A) → B) s)) x) :
      Away.{u_1, u_6, u_7} (A := C) 𝒞 ((g : (a : B) → C) ((f : (a : A) → B) s : B) : C))
    ((Away.map (g.comp f) s : (a : Away 𝒜 s) → Away 𝒞 ((g.comp f : (a : A) → C) s)) x :
      Away.{u_1, u_6, u_7} (A := C) 𝒞 ((g.comp f : (a : A) → C) s : C))

Tactic:
HomogeneousLocalization.map_map ..

Premises used: HomogeneousLocalization.map_map
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
I : Ideal A
inst_10 : I.IsPrime
J : Ideal B
inst_11 : J.IsPrime
hIJ : I = Ideal.comap f J
x : AtPrime 𝒜 I
obtain :
  ∀ (i : ι) (x s : ↥(𝒜 i)) (hs : (↑s : A) ∈ I.primeCompl),
    Eq (α := Localization (M := B) J.primeCompl)
      (val.{u_1, u_4, u_5} (ι := ι) (σ := τ) (𝒜 := ℬ)
        ((localRingHom f I J hIJ : (a : AtPrime 𝒜 I) → AtPrime ℬ J)
          (mk { deg := i, num := x, den := s, den_mem := hs })))
      (((Localization.localRingHom I J (↑f : A →+* B) hIJ :
            RingHom.{u_2, u_4} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        (mk { deg := i, num := x, den := s, den_mem := hs : NumDenSameDeg 𝒜 I.primeCompl }).val)
⊢ Eq (α := Localization (M := B) J.primeCompl)
    (val.{u_1, u_4, u_5} (ι := ι) (σ := τ) (𝒜 := ℬ) ((localRingHom f I J hIJ : (a : AtPrime 𝒜 I) → AtPrime ℬ J) x))
    (((Localization.localRingHom I J (↑f : A →+* B) hIJ :
          RingHom.{u_2, u_4} (Localization.AtPrime I) (Localization.AtPrime J)) :
        (a : Localization.AtPrime I) → Localization.AtPrime J)
      (val x))

Tactic:
obtain ⟨⟨i, x, s, hs⟩, rfl⟩ := x.mk_surjective

Premises used: HomogeneousLocalization.mk_surjective, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
I : Ideal A
inst_10 : I.IsPrime
J : Ideal B
inst_11 : J.IsPrime
hIJ : I = Ideal.comap f J
i : ι
x s : ↥(𝒜 i)
hs : (↑s : A) ∈ I.primeCompl
⊢ Eq (α := Localization (M := B) J.primeCompl)
    (val.{u_1, u_4, u_5} (ι := ι) (σ := τ) (𝒜 := ℬ)
      ((localRingHom f I J hIJ : (a : AtPrime 𝒜 I) → AtPrime ℬ J) (mk { deg := i, num := x, den := s, den_mem := hs })))
    (((Localization.localRingHom I J (↑f : A →+* B) hIJ :
          RingHom.{u_2, u_4} (Localization.AtPrime I) (Localization.AtPrime J)) :
        (a : Localization.AtPrime I) → Localization.AtPrime J)
      (mk { deg := i, num := x, den := s, den_mem := hs : NumDenSameDeg 𝒜 I.primeCompl }).val)

Tactic:
simp [localRingHom, map_mk]

Premises used: HomogeneousLocalization.map_mk, HomogeneousLocalization.localRingHom
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
f : 𝒜 →+*ᵍ ℬ
I : Ideal A
inst_14 : I.IsPrime
J : Ideal B
inst_15 : J.IsPrime
hIJ : I = Ideal.comap f J
x : AtPrime 𝒜 I
hx : IsUnit (M := AtPrime ℬ J) ((localRingHom f I J hIJ : (a : AtPrime 𝒜 I) → AtPrime ℬ J) x : AtPrime ℬ J)
rw :
  ∀
    (hx :
      IsUnit (M := Localization (M := B) J.primeCompl)
        (val.{u_1, u_4, u_5} (ι := ι) (σ := τ) (𝒜 := ℬ)
          ((localRingHom f I J hIJ : (a : AtPrime 𝒜 I) → AtPrime ℬ J) x))),
    IsUnit (val x)
⊢ IsUnit x

Tactic:
rw [← isUnit_iff_isUnit_val] at hx ⊢

Premises used: HomogeneousLocalization.isUnit_iff_isUnit_val
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
f : 𝒜 →+*ᵍ ℬ
I : Ideal A
inst_14 : I.IsPrime
J : Ideal B
inst_15 : J.IsPrime
hIJ : I = Ideal.comap f J
x : AtPrime 𝒜 I
hx :
  IsUnit (M := Localization (M := B) J.primeCompl)
    (val.{u_1, u_4, u_5} (ι := ι) (σ := τ) (𝒜 := ℬ) ((localRingHom f I J hIJ : (a : AtPrime 𝒜 I) → AtPrime ℬ J) x))
⊢ IsUnit.{u_4} (M := Localization (M := B) J.primeCompl)
    (((Localization.localRingHom I J (↑f : A →+* B) hIJ :
            RingHom.{u_2, u_4} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        (val x) :
      Localization.AtPrime J)

Tactic:
rw [val_localRingHom] at hx

Premises used: HomogeneousLocalization.val_localRingHom
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
f : 𝒜 →+*ᵍ ℬ
I : Ideal A
inst_14 : I.IsPrime
J : Ideal B
inst_15 : J.IsPrime
hIJ : I = Ideal.comap f J
x : AtPrime 𝒜 I
hx :
  IsUnit.{u_4} (M := Localization (M := B) J.primeCompl)
    (((Localization.localRingHom I J (↑f : A →+* B) hIJ :
            RingHom.{u_2, u_4} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        (val x) :
      Localization.AtPrime J)
⊢ IsUnit (val x)

Tactic:
IsLocalHom.map_nonunit _ hx

Premises used: IsLocalHom.map_nonunit
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
f : 𝒜 →+*ᵍ ℬ
I : Ideal A
inst_14 : I.IsPrime
J : Ideal B
inst_15 : J.IsPrime
hIJ : I = Ideal.comap f J
x : AtPrime 𝒜 I
hx :
  IsUnit.{u_4} (M := Localization (M := B) J.primeCompl)
    (((Localization.localRingHom I J (↑f : A →+* B) hIJ :
            RingHom.{u_2, u_4} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        (val x) :
      Localization.AtPrime J)
⊢ IsUnit (val x)

Tactic:
exact IsLocalHom.map_nonunit _ hx

Premises used: IsLocalHom.map_nonunit
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ HPow.hPow (β := ℕ) x 1 = f * g

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
rw :
  Eq (α := Localization.Away x)
    (Localization.mk (f • g)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (f * g) ⋯))
    1
⊢ HMul.hMul (α := Localization.Away x) (β := at Submonoid.powers x)
      ((algebraMap A (Localization.Away x) : (a : A) → Localization.Away x) f : Localization.Away x)
      (Localization.mk g
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (f * g) ⋯)) =
    1

Tactic:
rw [← Algebra.smul_def, Localization.smul_mk]

Premises used: Localization.smul_mk, Algebra.smul_def
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ Eq (α := Localization.Away x)
    (Localization.mk (f • g)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (f * g) ⋯))
    1

Tactic:
Localization.mk_self ⟨f*g, _⟩

Premises used: HMul.hMul, Subtype.mk, Localization.mk_self
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ Eq (α := Localization.Away x)
    (Localization.mk (f • g)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (f * g) ⋯))
    1

Tactic:
exact Localization.mk_self ⟨f*g, _⟩

Premises used: HMul.hMul, Subtype.mk, Localization.mk_self
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ HMul.hMul (α := Localization.Away x) (β := at Submonoid.powers x)
      ((algebraMap A (Localization.Away x) : (a : A) → Localization.Away x) f : Localization.Away x)
      (Localization.mk g
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (f * g) ⋯)) =
    1

Tactic:
have : algebraMap A (Localization.Away x) f *
    (Localization.mk g ⟨f * g, (Submonoid.mem_powers_iff _ _).mpr ⟨1, by simp [hx]⟩⟩) = 1 := by
    rw [← Algebra.smul_def, Localization.smul_mk]
    exact Localization.mk_self ⟨f*g, _⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this :
  HMul.hMul (α := Localization.Away x) (β := at Submonoid.powers x)
      ((algebraMap A (Localization.Away x) : (a : A) → Localization.Away x) f : Localization.Away x)
      (Localization.mk g
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (f * g) ⋯)) =
    1
simp :
  Eq (α := Localization.Away x)
    ((Localization.awayLift (algebraMap A (Localization.Away x)) f ⋯ : (a : Localization.Away f) → Localization.Away x)
        (Localization.mk (↑a : A)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯)) :
      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.{u_2 + 1} (α := Localization.Away 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)

Tactic:
simp only [awayMapAux, RingHom.coe_comp, Function.comp_apply, algebraMap_apply, val_mk]

Premises used: HomogeneousLocalization.val_mk, RingHom.coe_comp, Function.comp_apply, _private.0.HomogeneousLocalization.awayMapAux, HomogeneousLocalization.algebraMap_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this :
  HMul.hMul (α := Localization.Away x) (β := at Submonoid.powers x)
      ((algebraMap A (Localization.Away x) : (a : A) → Localization.Away x) f : Localization.Away x)
      (Localization.mk g
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (f * g) ⋯)) =
    1
rw :
  Eq (α := Localization.Away x)
    (Localization.mk ((↑a : A) • g ^ i)
      (HPow.hPow (α := ↥(Submonoid.powers x))
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (f * g) ⋯) i))
    (Localization.mk ((↑a : A) * g ^ i)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) ⋯))
⊢ Eq (α := Localization.Away x)
    ((Localization.awayLift (algebraMap A (Localization.Away x)) f ⋯ : (a : Localization.Away f) → Localization.Away x)
        (Localization.mk (↑a : A)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯)) :
      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)

Tactic:
rw [Localization.awayLift_mk (hv := this), ← Algebra.smul_def,
    Localization.mk_pow, Localization.smul_mk]

Premises used: Iff.mpr, Localization.mk, HMul.hMul, Algebra.algebraMap, congrArg, Localization.Away, Subtype.mk, HPow.hPow, pow_one, Localization.smul_mk, Localization.mk_pow, eq_self, Exists.intro, Submonoid.mem_powers_iff, of_eq_true, Algebra.smul_def, congrFun', OfNat.ofNat, Eq, Localization.awayLift_mk, Eq.trans
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this :
  HMul.hMul (α := Localization.Away x) (β := at Submonoid.powers x)
      ((algebraMap A (Localization.Away x) : (a : A) → Localization.Away x) f : Localization.Away x)
      (Localization.mk g
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (f * g) ⋯)) =
    1
subst :
  ∀
    (this :
      HMul.hMul (α := Localization.Away (f * g)) (β := at Submonoid.powers (f * g))
          ((algebraMap A (Localization.Away (f * g)) : (a : A) → Localization.Away (f * g)) f :
            Localization.Away (f * g))
          (Localization.mk g
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x) (f * g)
              ⋯)) =
        1),
    Eq (α := Localization.Away (f * g))
      (Localization.mk ((↑a : A) • g ^ i)
        (HPow.hPow (α := ↥(Submonoid.powers (f * g)))
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x) (f * g) ⋯) i))
      (Localization.mk ((↑a : A) * g ^ i)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x) ((f * g) ^ i)
          ⋯))
⊢ Eq (α := Localization.Away x)
    (Localization.mk ((↑a : A) • g ^ i)
      (HPow.hPow (α := ↥(Submonoid.powers x))
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (f * g) ⋯) i))
    (Localization.mk ((↑a : A) * g ^ i)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) ⋯))

Tactic:
subst hx
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f g : A
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this :
  HMul.hMul (α := Localization.Away (f * g)) (β := at Submonoid.powers (f * g))
      ((algebraMap A (Localization.Away (f * g)) : (a : A) → Localization.Away (f * g)) f : Localization.Away (f * g))
      (Localization.mk g
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x) (f * g) ⋯)) =
    1
⊢ Eq (α := Localization.Away (f * g))
    (Localization.mk ((↑a : A) • g ^ i)
      (HPow.hPow (α := ↥(Submonoid.powers (f * g)))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x) (f * g) ⋯) i))
    (Localization.mk ((↑a : A) * g ^ i)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x) ((f * g) ^ i) ⋯))

Tactic:
rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
z : Away 𝒜 f
obtain :
  ∀ (n : ι) (a : A) (ha : a ∈ 𝒜 n) (j : ℕ) (hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n),
    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)
⊢ Membership.mem (α := Localization.Away x) (γ := Set (Localization.Away x))
    (Set.range (ι := HomogeneousLocalization 𝒜 (Submonoid.powers x)) val)
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) z : Localization.Away x)

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

Premises used: HomogeneousLocalization.mk_surjective, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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)
w₁ : x ^ 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)

Tactic:
use mk ⟨n+j•e,⟨a*g^j, ?_⟩, ⟨x^j, ?_⟩, j, rfl⟩
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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
⊢ 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 := ⋯ }))

Tactic:
simp [awayMapAux_mk 𝒜 (hx := hx)]

Premises used: HomogeneousLocalization.awayMapAux_mk
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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
w : g ^ j ∈ 𝒜 (j • e)
⊢ a * g ^ j ∈ 𝒜 (n + j • e)

Tactic:
apply SetLike.mul_mem_graded ha

Premises used: SetLike.mul_mem_graded
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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
⊢ g ^ j ∈ 𝒜 (j • e)

Tactic:
SetLike.pow_mem_graded _ hg

Premises used: SetLike.pow_mem_graded
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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
⊢ g ^ j ∈ 𝒜 (j • e)

Tactic:
exact SetLike.pow_mem_graded _ hg

Premises used: SetLike.pow_mem_graded