awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 𝒜
e_1 d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
e :
  Eq (α := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha) : Away 𝒜 x)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf m b hb) : Away 𝒜 x)
⊢ ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * Away.mk 𝒜 hf m b hb
have e₁ : Eq (α := at Submonoid.powers x)
  (val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha)))
  (val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf m b hb)))
Tactic: replace e := congr_arg val e
Cleared hypotheses: e
-- 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 𝒜
e_1 d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
e :
  Eq (α := at Submonoid.powers x)
    (val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha)))
    (val.{0, u_2, u_3} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf m b hb)))
⊢ ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * Away.mk 𝒜 hf m b hb
have e₁ : ∃ (c : ↥(Submonoid.powers x)), (↑c : A) * (x ^ m * (a * g ^ n)) = (↑c : A) * (x ^ n * (b * g ^ m))
Tactic: simp only [RingHom.algebraMap_toAlgebra, awayMap_mk, val_mk,
      Localization.mk_eq_mk_iff, Localization.r_iff_exists] at e
Cleared hypotheses: e
-- 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_1 d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
e : ∃ (c : ↥(Submonoid.powers x)), (↑c : A) * (x ^ m * (a * g ^ n)) = (↑c : A) * (x ^ n * (b * g ^ m))
⊢ ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * Away.mk 𝒜 hf m b hb
have toIsLocalizationMap : ∀ (k : ℕ)
  (hc :
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
              ((fun (x_1 : ℕ) ↦ x ^ x_1) k) sorry) :
          A) *
        (x ^ m * (a * g ^ n)) =
      (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
              ((fun (x_1 : ℕ) ↦ x ^ x_1) k) sorry) :
          A) *
        (x ^ n * (b * g ^ m))),
  ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * Away.mk 𝒜 hf m b hb
Tactic: obtain ⟨⟨_, k, rfl⟩, hc⟩ := e
Cleared hypotheses: e
-- 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
⊢ ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    (↑c : Away 𝒜 f) * Away.mk 𝒜 hf n a ha = (↑c : Away 𝒜 f) * Away.mk 𝒜 hf m b hb
have toIsLocalizationMap : (↑(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) (k + m + n)) sorry) :
      Away 𝒜 f) *
    Away.mk 𝒜 hf n a ha =
  (↑(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) (k + m + n)) sorry) :
      Away 𝒜 f) *
    Away.mk 𝒜 hf m b hb
Tactic: refine ⟨⟨_, k + m + n, rfl⟩, ?_⟩
-- 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
⊢ (↑(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) (k + m + n)) ⋯) :
        Away 𝒜 f) *
      Away.mk 𝒜 hf n a ha =
    (↑(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) (k + m + n)) ⋯) :
        Away 𝒜 f) *
      Away.mk 𝒜 hf m b hb
have toIsLocalizationMap : val
    ((↑(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) (k + m + n)) sorry) :
        Away 𝒜 f) *
      Away.mk 𝒜 hf n a ha) =
  val
    ((↑(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) (k + m + n)) sorry) :
        Away 𝒜 f) *
      Away.mk 𝒜 hf m b hb)
Tactic: ext
-- 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
⊢ val
      ((↑(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) (k + m + n)) ⋯) :
          Away 𝒜 f) *
        Away.mk 𝒜 hf n a ha) =
    val
      ((↑(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) (k + m + n)) ⋯) :
          Away 𝒜 f) *
        Away.mk 𝒜 hf m b hb)
have toIsLocalizationMap : ∃ (a_1 : A),
  Membership.mem (γ := Submonoid A) (Submonoid.powers f) a_1 ∧
    a_1 * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
      a_1 * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))
Tactic: simp only [val_mul, val_pow, val_mk, Localization.mk_pow,
      Localization.mk_eq_mk_iff, Localization.r_iff_exists, Submonoid.coe_mul, Localization.mk_mul,
      SubmonoidClass.coe_pow, Subtype.exists, exists_prop]
-- 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
⊢ ∃ (a_1 : A),
    Membership.mem (γ := Submonoid A) (Submonoid.powers f) a_1 ∧
      a_1 * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
        a_1 * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))
have toIsLocalizationMap : (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
  (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))
Tactic: refine ⟨_, ⟨k, rfl⟩, ?_⟩
-- 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
⊢ (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))
have toIsLocalizationMap : ∀ (hf : f ∈ 𝒜 0) (hd : Ne (α := ℕ) 0 0) (ha : a ∈ 𝒜 (HSMul.hSMul (β := ℕ) n 0)) (hb : b ∈ 𝒜 (HSMul.hSMul (β := ℕ) m 0)),
  (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * (HPow.hPow (β := ℕ) g 0 ^ (k + m + n) * a)) =
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * (HPow.hPow (β := ℕ) g 0 ^ (k + m + n) * b))
Tactic: rcases d with - | d
Cleared hypotheses: d, hf, hd, ha, hb
-- 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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
toIsLocalizationMap :
  ∀ (hf : f ∈ 𝒜 0) (hd : Ne (α := ℕ) 0 0) (ha : a ∈ 𝒜 (HSMul.hSMul (β := ℕ) n 0))
    (hb : b ∈ 𝒜 (HSMul.hSMul (β := ℕ) m 0)),
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * (HPow.hPow (β := ℕ) g 0 ^ (k + m + n) * a)) =
      (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * (HPow.hPow (β := ℕ) g 0 ^ (k + m + n) * b))
⊢ (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ d) ^ (k + m + n) * a)) =
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ d) ^ (k + m + n) * b))
have toIsLocalizationMap₁ : ∀ (d : ℕ) (hf : f ∈ 𝒜 (d + 1)) (hd : d + 1 ≠ 0) (ha : a ∈ 𝒜 (n • (d + 1))) (hb : b ∈ 𝒜 (m • (d + 1))),
  (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))
Tactic: rcases d with - | d
Cleared hypotheses: d, hf, hd, ha, hb
-- 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 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
a : A
m : ℕ
b : A
k : ℕ
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
            ((fun (x_1 : ℕ) ↦ x ^ x_1) k) ⋯) :
        A) *
      (x ^ n * (b * g ^ m))
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
⊢ (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))
have hc₁ : (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
          ((fun (x : ℕ) ↦ (f * g) ^ x) k) sorry) :
      A) *
    ((f * g) ^ m * (a * g ^ n)) =
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
          ((fun (x : ℕ) ↦ (f * g) ^ x) k) sorry) :
      A) *
    ((f * g) ^ n * (b * g ^ m))
Tactic: subst hx
Cleared hypotheses: x, hx, this, hc
-- 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 : ℕ
f g : A
hg : g ∈ 𝒜 e
n : ℕ
a : A
m : ℕ
b : A
k d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := RingHom.toAlgebra (awayMap 𝒜 hg ⋯)
hc :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ n * (b * g ^ m))
⊢ (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))
have h : (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
  f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) *
    ((↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) sorry) :
        A) *
      ((f * g) ^ m * (a * g ^ n)))
Tactic: convert! congr(f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) * $hc) using 1
-- 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 : ℕ
f g : A
hg : g ∈ 𝒜 e
n : ℕ
a : A
m : ℕ
b : A
k d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := RingHom.toAlgebra (awayMap 𝒜 hg ⋯)
hc :
  (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ m * (a * g ^ n)) =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
        A) *
      ((f * g) ^ n * (b * g ^ m))
h :
  (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) *
      ((↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
              ((fun (x : ℕ) ↦ (f * g) ^ x) k) ⋯) :
          A) *
        ((f * g) ^ m * (a * g ^ n)))
⊢ (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))
have h₁ : (fun (x : ℕ) ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b)) =
  f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) *
    ((↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers (f * g)) x)
            ((fun (x : ℕ) ↦ (f * g) ^ x) k) sorry) :
        A) *
      ((f * g) ^ n * (b * g ^ m)))
Tactic: convert! congr(f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) * $hc) using 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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
⊢ Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    ⊤
have pos : ∀ (HH : Subsingleton (Away 𝒜 f)),
  Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x})
    ⊤
Tactic: by_cases HH : Subsingleton (HomogeneousLocalization.Away 𝒜 f)
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
pos :
  ∀ (HH : Subsingleton (Away 𝒜 f)),
    Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
      (Submodule.span ↥(𝒜 0)
        {x : Away 𝒜 f |
          ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
      ⊤
⊢ Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    ⊤
have neg : ∀ (HH : ¬Subsingleton (Away 𝒜 f)),
  Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x})
    ⊤
Tactic: by_cases HH : Subsingleton (HomogeneousLocalization.Away 𝒜 f)
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
⊢ Eq (α := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    ⊤
have neg : LE.le (α := Submodule (↥(𝒜 0)) (Away 𝒜 f)) ⊤
  (Submodule.span ↥(𝒜 0)
    {x : Away 𝒜 f |
      ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x})
Tactic: rw [← top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst_6 : Fintype ι'
v : ι' → A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range v)) ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
x : Away 𝒜 f
⊢ Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) ⋯ = x})
    x
have neg : ∀ (n : ι) (a : A) (ha : a ∈ 𝒜 n) (j : ℕ) (hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n),
  Membership.mem (γ := Submodule (↥(𝒜 0)) (Away 𝒜 f))
    (Submodule.span ↥(𝒜 0)
      {x : Away 𝒜 f |
        ∃ (a : ℕ) (ai : ι' → ℕ) (hai : ∑ i : ι', ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i : ι', v i ^ ai i) sorry = x})
    (mk
      { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x : ℕ) ↦ f ^ x) j) hb', den_mem := sorry })
Tactic: obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, ⟨j, (rfl : _ = b)⟩⟩, rfl⟩ := mk_surjective x
Cleared hypotheses: x