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 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
    (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
c3 c4 : NumDenSameDeg 𝒜 x
h' :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c3.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯))
    (Localization.mk (↑c4.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) ⋯))
h₁ :
  Localization.mk ((↑c1.num : A) * (↑c3.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) ⋯) =
    HMul.hMul (α := Localization (M := A) x)
      (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
      (Localization.mk (↑c3.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯))
⊢ Eq (α := Localization (M := A) x)
    (Localization.mk ((↑c1.num : A) * (↑c3.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) ⋯))
    (Localization.mk ((↑c2.num : A) * (↑c4.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) * (↑c4.den : A)) ⋯))
have h₂ : Localization.mk ((↑c2.num : A) * (↑c4.num : A))
    (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) * (↑c4.den : A)) sorry) =
  HMul.hMul (α := Localization (M := A) x)
    (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) sorry))
    (Localization.mk (↑c4.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) sorry))
Tactic: convert! congr_arg₂ (· * ·) h h'
-- 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 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
    (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
c3 c4 : NumDenSameDeg 𝒜 x
h' :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c3.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯))
    (Localization.mk (↑c4.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) ⋯))
⊢ Localization.mk ((↑c1.num : A) * (↑c3.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) ⋯) =
    HMul.hMul (α := Localization (M := A) x)
      (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
      (Localization.mk (↑c3.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯))
have h₁ : Eq (α := Localization (M := A) x)
  (Localization.mk ((↑c1.num : A) * (↑c3.num : A))
    (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) sorry))
  (Localization.mk ((↑c1.num : A) * (↑c3.num : A))
    (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) sorry *
      Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) sorry))
Tactic: rw [Localization.mk_mul]
-- 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 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
    (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
c3 c4 : NumDenSameDeg 𝒜 x
h' :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c3.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯))
    (Localization.mk (↑c4.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) ⋯))
⊢ Localization.mk ((↑c2.num : A) * (↑c4.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) * (↑c4.den : A)) ⋯) =
    HMul.hMul (α := Localization (M := A) x)
      (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
      (Localization.mk (↑c4.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) ⋯))
have h₁ : Eq (α := Localization (M := A) x)
  (Localization.mk ((↑c2.num : A) * (↑c4.num : A))
    (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) * (↑c4.den : A)) sorry))
  (Localization.mk ((↑c2.num : A) * (↑c4.num : A))
    (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) sorry *
      Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) sorry))
Tactic: rw [Localization.mk_mul]
-- 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 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ (HAdd.hAdd (α := HomogeneousLocalization 𝒜 x) (Quotient.mk'' y1) (Quotient.mk'' y2)).val =
    val (Quotient.mk'' y1) + val (Quotient.mk'' y2)
have rw : Eq (α := Localization (M := A) x)
  (Localization.mk (↑(y1 + y2).num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑(y1 + y2).den : A) sorry))
  (Localization.mk
    ((↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y1.den : A) sorry) : A) * (↑y2.num : A) +
      (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y2.den : A) sorry) : A) * (↑y1.num : A))
    (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y1.den : A) sorry *
      Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y2.den : A) sorry))
Tactic: rw [← mk_add, val_mk, val_mk, val_mk, Localization.add_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 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
⊢ (HMul.hMul (α := HomogeneousLocalization 𝒜 x) (Quotient.mk'' y1) (Quotient.mk'' y2)).val =
    val (Quotient.mk'' y1) * val (Quotient.mk'' y2)
have rw : Eq (α := Localization (M := A) x)
  (Localization.mk (↑(y1 * y2).num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑(y1 * y2).den : A) sorry))
  (Localization.mk ((↑y1.num : A) * (↑y2.num : A))
    (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y1.den : A) sorry *
      Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y2.den : A) sorry))
Tactic: rw [← mk_mul, val_mk, val_mk, val_mk, Localization.mk_mul]
-- 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 𝒜
x : Submonoid A
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ (y1 - y2).val = y1.val - y2.val
have rw : (y1 - y2).val = (y1 + -y2).val
Tactic: rw [sub_eq_add_neg, ← val_neg, ← val_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 𝒜
x : Submonoid A
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ (HPow.hPow (α := HomogeneousLocalization 𝒜 x) (Quotient.mk'' y) n).val = val (Quotient.mk'' y) ^ n
have rw : Eq (α := Localization (M := A) x)
  (Localization.mk (↑(y ^ n).num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑(y ^ n).den : A) sorry))
  (Localization.mk ((↑y.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y.den : A) sorry ^ n))
Tactic: rw [← mk_pow, val_mk, val_mk, Localization.mk_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 𝒜
x : Submonoid A
n : ℕ
⊢ Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) n.unaryCast) (↑n : at x)
have zero : Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (Nat.unaryCast 0)) (↑0 : at x)
Tactic: induction n
Cleared hypotheses: n
-- 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 𝒜
x : Submonoid A
n : ℕ
zero : Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (Nat.unaryCast 0)) (↑0 : at x)
⊢ Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) n.unaryCast) (↑n : at x)
have succ : ∀ (n : ℕ),
  Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) n.unaryCast) (↑n : at x) →
    Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (n + 1).unaryCast)
      (↑(n + 1) : at x)
Tactic: induction n
Cleared hypotheses: n
-- 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 𝒜
x : Submonoid A
n : ℤ
⊢ Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) n.castDef) (↑n : at x)
have ofNat : ∀ (a : ℕ),
  Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (Int.ofNat a).castDef)
    (↑(Int.ofNat a) : at x)
Tactic: cases n
Cleared hypotheses: n
-- 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 𝒜
x : Submonoid A
n : ℤ
ofNat :
  ∀ (a : ℕ),
    Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (Int.ofNat a).castDef)
      (↑(Int.ofNat a) : at x)
⊢ Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) n.castDef) (↑n : at x)
have negSucc : ∀ (a : ℕ),
  Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (Int.negSucc a).castDef)
    (↑(Int.negSucc a) : at x)
Tactic: cases n
Cleared hypotheses: n
-- 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 𝒜
x : Submonoid A
f : NumDenSameDeg 𝒜 x
h : f.num = 0
⊢ mk f = 0
have a : (mk f).val = val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) 0
Tactic: apply val_injective
-- 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 𝒜
x : Submonoid A
f : NumDenSameDeg 𝒜 x
h : f.den = 0
⊢ mk f = 0
have this : Subsingleton (HomogeneousLocalization 𝒜 x)
Tactic: have := subsingleton 𝒜 (h ▸ f.den_mem)
-- 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 𝒜
x : Submonoid A
f g : ↥(𝒜 0)
⊢ mk { deg := 0, num := f * g, den := 1, den_mem := ⋯ } =
    HMul.hMul (α := HomogeneousLocalization 𝒜 x) (mk { deg := 0, num := f, den := 1, den_mem := ⋯ : NumDenSameDeg 𝒜 x })
      (mk { deg := 0, num := g, den := 1, den_mem := ⋯ : NumDenSameDeg 𝒜 x })
have a : val (mk { deg := 0, num := f * g, den := 1, den_mem := sorry : NumDenSameDeg 𝒜 x }) =
  (HMul.hMul (α := HomogeneousLocalization 𝒜 x) (mk { deg := 0, num := f, den := 1, den_mem := sorry : NumDenSameDeg 𝒜 x })
      (mk { deg := 0, num := g, den := 1, den_mem := sorry : NumDenSameDeg 𝒜 x })).val
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 𝒜
x : Submonoid A
f g : ↥(𝒜 0)
⊢ mk { deg := 0, num := f + g, den := 1, den_mem := ⋯ } =
    HAdd.hAdd (α := HomogeneousLocalization 𝒜 x) (mk { deg := 0, num := f, den := 1, den_mem := ⋯ : NumDenSameDeg 𝒜 x })
      (mk { deg := 0, num := g, den := 1, den_mem := ⋯ : NumDenSameDeg 𝒜 x })
have a : val (mk { deg := 0, num := f + g, den := 1, den_mem := sorry : NumDenSameDeg 𝒜 x }) =
  (HAdd.hAdd (α := HomogeneousLocalization 𝒜 x) (mk { deg := 0, num := f, den := 1, den_mem := sorry : NumDenSameDeg 𝒜 x })
      (mk { deg := 0, num := g, den := 1, den_mem := sorry : NumDenSameDeg 𝒜 x })).val
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
𝒜 : ι → σ
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ f.den • f.val = (algebraMap A (Localization (M := A) x) : (a : A) → at x) f.num
have rw : Eq (α := Localization (M := A) x)
  (IsLocalization.mk' (Localization (M := A) x) (f.den * f.num) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) f.den sorry) :
    Localization (M := A) x)
  ((algebraMap A (Localization (M := A) x) : (a : A) → at x) f.num : Localization (M := A) x)
Tactic: rw [eq_num_div_den, Localization.mk_eq_mk', IsLocalization.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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : AtPrime 𝒜 𝔭
⊢ IsUnit (val f) ↔ IsUnit f
have refine : ∀ (h1 : IsUnit (val f)), IsUnit f
Tactic: refine ⟨fun h1 ↦ ?_, IsUnit.map (algebraMap _ _)⟩
-- 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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : AtPrime 𝒜 𝔭
h1 : IsUnit (val f)
⊢ IsUnit f
have rcases : ∀ (b : Localization (M := A) 𝔭.primeCompl) (eq0 : val f * b = 1) (eq1 : b * val f = 1), IsUnit f
Tactic: rcases h1 with ⟨⟨a, b, eq0, eq1⟩, rfl : a = f.val⟩
Cleared hypotheses: h1
-- 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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : AtPrime 𝒜 𝔭
b : Localization (M := A) 𝔭.primeCompl
eq0 : val f * b = 1
eq1 : b * val f = 1
⊢ IsUnit f
have obtain : ∀ (f : NumDenSameDeg 𝒜 𝔭.primeCompl) (eq0 : (mk f).val * b = 1) (eq1 : b * (mk f).val = 1), IsUnit (mk f)
Tactic: obtain ⟨f, rfl⟩ := mk_surjective f
Cleared hypotheses: f, eq0, eq1
-- 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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
b : Localization (M := A) 𝔭.primeCompl
f : NumDenSameDeg 𝒜 𝔭.primeCompl
eq0 : (mk f).val * b = 1
eq1 : b * (mk f).val = 1
⊢ IsUnit (mk f)
have obtain : ∀ (b : A) (s : ↥𝔭.primeCompl) (eq0 : (mk f).val * IsLocalization.mk' (Localization (M := A) 𝔭.primeCompl) b s = 1)
  (eq1 : IsLocalization.mk' (Localization (M := A) 𝔭.primeCompl) b s * (mk f).val = 1), IsUnit (mk f)
Tactic: obtain ⟨b, s, rfl⟩ := IsLocalization.exists_mk'_eq 𝔭.primeCompl b
Cleared hypotheses: b, eq0, eq1
-- 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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 : (mk f).val * IsLocalization.mk' (Localization (M := A) 𝔭.primeCompl) b s = 1
eq1 : IsLocalization.mk' (Localization (M := A) 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)
have eq0₁ : ∃ (c : ↥𝔭.primeCompl),
  (↑c : A) * ((↑f.num : A) * b) =
    (↑c : A) * (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝔭.primeCompl) (↑f.den : A) sorry * s) : A)
Tactic: rw [val_mk, Localization.mk_eq_mk', ← IsLocalization.mk'_mul, IsLocalization.mk'_eq_iff_eq_mul,
    one_mul, IsLocalization.eq_iff_exists (M := 𝔭.primeCompl)] at eq0
Cleared hypotheses: eq0, eq1
-- 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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq0 :
  ∃ (c : ↥𝔭.primeCompl),
    (↑c : A) * ((↑f.num : A) * b) =
      (↑c : A) * (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝔭.primeCompl) (↑f.den : A) ⋯ * s) : A)
eq1 : IsLocalization.mk' (Localization (M := A) 𝔭.primeCompl) b s * (mk f).val = 1
⊢ IsUnit (mk f)
have obtain : ∀ (c : ↥𝔭.primeCompl) (hc : (↑c : A) * ((↑f.num : A) * b) = (↑c : A) * ((↑f.den : A) * (↑s : A))), IsUnit (mk f)
Tactic: obtain ⟨c, hc : _ = c.1 * (f.den.1 * s.1)⟩ := eq0
Cleared hypotheses: eq0
-- 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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq1 : IsLocalization.mk' (Localization (M := A) 𝔭.primeCompl) b s * (mk f).val = 1
c : ↥𝔭.primeCompl
hc : (↑c : A) * ((↑f.num : A) * b) = (↑c : A) * ((↑f.den : A) * (↑s : A))
⊢ IsUnit (mk f)
have this : (↑f.num : A) ∉ 𝔭
Tactic: have : f.num.1 ∉ 𝔭 := by
    exact fun h ↦ mul_mem c.2 (mul_mem f.den_mem s.2)
      (hc ▸ Ideal.mul_mem_left _ c.1 (Ideal.mul_mem_right b _ h))
-- 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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq1 : IsLocalization.mk' (Localization (M := A) 𝔭.primeCompl) b s * (mk f).val = 1
c : ↥𝔭.primeCompl
hc : (↑c : A) * ((↑f.num : A) * b) = (↑c : A) * ((↑f.den : A) * (↑s : A))
this : (↑f.num : A) ∉ 𝔭
⊢ IsUnit (mk f)
have refine : mk f * Quotient.mk'' { deg := f.deg, num := f.den, den := f.num, den_mem := this : NumDenSameDeg 𝒜 𝔭.primeCompl } = 1
Tactic: refine .of_mul_eq_one (Quotient.mk'' ⟨f.1, f.3, f.2, 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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : NumDenSameDeg 𝒜 𝔭.primeCompl
b : A
s : ↥𝔭.primeCompl
eq1 : IsLocalization.mk' (Localization (M := A) 𝔭.primeCompl) b s * (mk f).val = 1
c : ↥𝔭.primeCompl
hc : (↑c : A) * ((↑f.num : A) * b) = (↑c : A) * ((↑f.den : A) * (↑s : A))
this : (↑f.num : A) ∉ 𝔭
⊢ mk f * Quotient.mk'' { deg := f.deg, num := f.den, den := f.num, den_mem := this : NumDenSameDeg 𝒜 𝔭.primeCompl } = 1
have rw : Eq (α := Localization (M := A) 𝔭.primeCompl)
  (Localization.mk
    (↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this : NumDenSameDeg 𝒜 𝔭.primeCompl }).num : A)
    (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝔭.primeCompl)
      (↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this : NumDenSameDeg 𝒜 𝔭.primeCompl }).den : A) sorry))
  (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) 1)
Tactic: rw [← mk_mul, ext_iff_val, 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 : A
d : ι
n : ℕ
hf : f ∈ 𝒜 d
x : A
hx : x ∈ 𝒜 (n • d)
w : ℕ
⊢ Membership.mem (γ := Submonoid A) (Submonoid.powers f) (f ^ n)
have h : (fun (x : ℕ) ↦ f ^ x) n = f ^ n
Tactic: use n
-- 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
x : Away 𝒜 f
⊢ ∃ (n : ℕ) (a : A) (ha : a ∈ 𝒜 (n • d)), Away.mk 𝒜 hf n a ha = x
have obtain : ∀ (N : ι) (s : A) (hs : s ∈ 𝒜 N) (n : ℕ) (hn : (fun (x : ℕ) ↦ f ^ x) n ∈ 𝒜 N),
  ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := sorry })
Tactic: obtain ⟨⟨N, ⟨s, hs⟩, ⟨b, hn⟩, ⟨n, (rfl : _ = b)⟩⟩, rfl⟩ := mk_surjective x
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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun (x : ℕ) ↦ f ^ x) n ∈ 𝒜 N
⊢ ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })
have pos : ∀ (hfn : f ^ n = 0),
  ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := sorry })
Tactic: by_cases hfn : f ^ n = 0