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 𝒜
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
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
⊢ Eq (α := HomogeneousLocalization ℬ Q)
    (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
      (fun (x : NumDenSameDeg 𝒜 P) ↦
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ })
      ⋯ 0)
    0
have simp : Eq (α := HomogeneousLocalization ℬ Q)
  (Quotient.mk''
    { deg := 0, num := (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ 0) 0 sorry : ↥(ℬ 0)),
      den := (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ 0) 1 sorry : ↥(ℬ 0)), den_mem := sorry })
  0
Tactic: simp only [← mk_zero (𝒜 := 𝒜), Quotient.map'_mk'', deg_zero,
    num_zero, ZeroMemClass.coe_zero, map_zero, den_zero, map_one]
-- 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 𝒜
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
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
⊢ Quotient.map'
      (fun (x : NumDenSameDeg 𝒜 P) ↦
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ })
      ⋯ (HAdd.hAdd (α := HomogeneousLocalization 𝒜 P) (Quotient.mk'' x) (Quotient.mk'' y)) =
    HAdd.hAdd (α := HomogeneousLocalization ℬ Q)
      (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
        (fun (x : NumDenSameDeg 𝒜 P) ↦
          { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
            NumDenSameDeg ℬ Q })
        ⋯ (Quotient.mk'' x))
      (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
        (fun (x : NumDenSameDeg 𝒜 P) ↦
          { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
            NumDenSameDeg ℬ Q })
        ⋯ (Quotient.mk'' y))
have simp : Quotient.mk''
    { deg := (x + y).deg,
      num :=
        Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x + y).deg)
          (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.den : A) : B) ((g : (a : A) → B) (↑y.num : A) : B) +
            HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑y.den : A) : B) ((g : (a : A) → B) (↑x.num : A) : B))
          sorry,
      den :=
        Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x + y).deg)
          (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.den : A) : B) ((g : (a : A) → B) (↑y.den : A) : B)) sorry,
      den_mem := sorry } =
  mk
    (HAdd.hAdd (α := NumDenSameDeg ℬ Q)
      { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) sorry,
        den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) sorry, den_mem := sorry :
        NumDenSameDeg ℬ Q }
      { deg := y.deg, num := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.num : A)) sorry,
        den := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.den : A)) sorry, den_mem := sorry :
        NumDenSameDeg ℬ Q })
Tactic: simp only [← mk_add, Quotient.map'_mk'', num_add, map_add, map_mul, den_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 𝒜
P : Submonoid A
⊢ Eq (α := HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P)
    (map (GradedRingHom.id 𝒜) ⋯ : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P)
    (RingHom.id (HomogeneousLocalization 𝒜 P) : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P)
have a : ∀ (x : HomogeneousLocalization 𝒜 P),
  Eq (α := Localization (M := A) P)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (((map (GradedRingHom.id 𝒜) sorry : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P) :
          (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P)
        x))
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((RingHom.id (HomogeneousLocalization 𝒜 P) : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P) x))
Tactic: ext x
-- 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 𝒜
P : Submonoid A
x : HomogeneousLocalization 𝒜 P
⊢ Eq (α := Localization (M := A) P)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (((map (GradedRingHom.id 𝒜) ⋯ : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P) :
          (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P)
        x))
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((RingHom.id (HomogeneousLocalization 𝒜 P) : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P) x))
have a : ∀ (c : NumDenSameDeg 𝒜 P),
  Eq (α := Localization (M := A) P)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (((map (GradedRingHom.id 𝒜) sorry : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P) :
          (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P)
        (mk c)))
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((RingHom.id (HomogeneousLocalization 𝒜 P) : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P)
        (mk c)))
Tactic: obtain ⟨c, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- 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 𝒜
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 : ℬ →+*ᵍ 𝒞
P : Submonoid A
Q : Submonoid B
R : Submonoid C
hpq : P ≤ Submonoid.comap f Q
hqr : Q ≤ Submonoid.comap g R
⊢ Eq (α := HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒞 R) (map (g.comp f) ⋯)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map g hqr) (map f hpq))
have a : ∀ (x : HomogeneousLocalization 𝒜 P),
  Eq (α := Localization (M := C) R)
    (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
      ((map (g.comp f) sorry : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R) x))
    (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map g hqr) (map f hpq) :
          (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R)
        x))
Tactic: ext x
-- 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 𝒜
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 : ℬ →+*ᵍ 𝒞
P : Submonoid A
Q : Submonoid B
R : Submonoid C
hpq : P ≤ Submonoid.comap f Q
hqr : Q ≤ Submonoid.comap g R
x : HomogeneousLocalization 𝒜 P
⊢ Eq (α := Localization (M := C) R)
    (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
      ((map (g.comp f) ⋯ : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R) x))
    (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map g hqr) (map f hpq) :
          (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R)
        x))
have a : ∀ (c : NumDenSameDeg 𝒜 P),
  Eq (α := Localization (M := C) R)
    (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
      ((map (g.comp f) sorry : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R) (mk c)))
    (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map g hqr) (map f hpq) :
          (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R)
        (mk c)))
Tactic: obtain ⟨c, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- 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 𝒜
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
⊢ 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))
have 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)
Tactic: obtain ⟨⟨i, x, s, hs⟩, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- 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 𝒜
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)
⊢ IsUnit x
have 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)
Tactic: rw [← isUnit_iff_isUnit_val] at hx ⊢
Cleared hypotheses: 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 𝒜
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 (val x)
have 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)
Tactic: rw [val_localRingHom] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f 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
have 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) sorry))
  1
Tactic: rw [← Algebra.smul_def, Localization.smul_mk]
-- 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 g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ 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)
have 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) sorry)) =
  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, _⟩
-- 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 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
⊢ 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)
have simp : Eq (α := Localization.Away x)
  ((Localization.awayLift (algebraMap A (Localization.Away x)) f sorry : (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) 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: simp only [awayMapAux, RingHom.coe_comp, Function.comp_apply, algebraMap_apply, 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 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
⊢ 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)
have 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) sorry) 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) sorry))
Tactic: rw [Localization.awayLift_mk (hv := this), ← Algebra.smul_def,
    Localization.mk_pow, Localization.smul_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 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
⊢ 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) ⋯))
have 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) sorry)) =
      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) sorry) 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) sorry))
Tactic: subst hx
Cleared hypotheses: x, hx, 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 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
z : Away 𝒜 f
⊢ 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)
have 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 𝒜 sorry : (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 := sorry }) :
      Localization.Away x)
Tactic: obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, j, rfl : _ = b⟩, rfl⟩ := mk_surjective z
Cleared hypotheses: z
-- 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
⊢ 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 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) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n + j • e)) (x ^ j) sorry, den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers x) }))
  ((awayMapAux 𝒜 sorry : (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 := sorry }))
Tactic: use mk ⟨n+j•e,⟨a*g^j, ?_⟩, ⟨x^j, ?_⟩, j, rfl⟩