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 𝒜
x : Submonoid A
f g : ↥(𝒜 0)
a :
  val (mk { deg := 0, num := f * g, den := 1, den_mem := ⋯ : NumDenSameDeg 𝒜 x }) =
    (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 })).val
⊢ 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 })

Tactic:
ext
-- 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 𝒜
x : Submonoid A
f g : ↥(𝒜 0)
⊢ val (mk { deg := 0, num := f * g, den := 1, den_mem := ⋯ : NumDenSameDeg 𝒜 x }) =
    (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 })).val

Tactic:
simp [Localization.mk_mul]

Premises used: Localization.mk_mul
-- 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 𝒜
x : Submonoid A
f g : ↥(𝒜 0)
a :
  val (mk { deg := 0, num := f + g, den := 1, den_mem := ⋯ : NumDenSameDeg 𝒜 x }) =
    (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 })).val
⊢ 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 })

Tactic:
ext
-- 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 𝒜
x : Submonoid A
f g : ↥(𝒜 0)
⊢ val (mk { deg := 0, num := f + g, den := 1, den_mem := ⋯ : NumDenSameDeg 𝒜 x }) =
    (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 })).val

Tactic:
simp [Localization.add_mk, add_comm f.1 g.1]

Premises used: add_comm, Localization.add_mk, Subtype.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 𝒜
x : Submonoid A
⊢ Eq (α := ↥(𝒜 0) →+* HomogeneousLocalization 𝒜 x) (algebraMap (↥(𝒜 0)) (HomogeneousLocalization 𝒜 x))
    (fromZeroRingHom 𝒜 x)

Tactic:
rfl

Premises used: 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 𝒜
x : Submonoid A
⊢ IsScalarTower (↥(𝒜 0)) (HomogeneousLocalization 𝒜 x) (Localization (M := A) x)

Tactic:
.of_algebraMap_eq' rfl

Premises used: IsScalarTower.of_algebraMap_eq', rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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 ∈ x

Tactic:
(Quotient.out f).den_mem

Premises used: HomogeneousLocalization.den, Set.Mem, Quotient.out, HomogeneousLocalization.NumDenSameDeg.den_mem
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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.num ∈ 𝒜 f.deg

Tactic:
(Quotient.out f).num.2

Premises used: HomogeneousLocalization.NumDenSameDeg.num, Set.Mem, HomogeneousLocalization.deg, Quotient.out, HomogeneousLocalization.num, Subtype.property
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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.deg

Tactic:
(Quotient.out f).den.2

Premises used: HomogeneousLocalization.den, Set.Mem, HomogeneousLocalization.deg, Quotient.out, HomogeneousLocalization.NumDenSameDeg.den, Subtype.property
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
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.val = Localization.mk f.num (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) f.den ⋯)

Tactic:
congr_arg HomogeneousLocalization.val (Quotient.out_eq' f).symm

Premises used: Quotient.out_eq', Localization.mk, HomogeneousLocalization.den, congr_arg, Quotient.mk', HomogeneousLocalization.num, Eq.symm, OreLocalization.oreDiv, HomogeneousLocalization.NumDenSameDeg.embedding, HomogeneousLocalization.val
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
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 ⋯) :
      Localization (M := A) x)
    ((algebraMap A (Localization (M := A) x) : (a : A) → at x) f.num : Localization (M := A) x)
⊢ f.den • f.val = (algebraMap A (Localization (M := A) x) : (a : A) → at x) f.num

Tactic:
rw [eq_num_div_den, Localization.mk_eq_mk', IsLocalization.smul_mk']

Premises used: Localization.mk_eq_mk', HomogeneousLocalization.eq_num_div_den, IsLocalization.smul_mk'
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ 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 ⋯) :
      Localization (M := A) x)
    ((algebraMap A (Localization (M := A) x) : (a : A) → at x) f.num : Localization (M := A) x)

Tactic:
IsLocalization.mk'_mul_cancel_left _ ⟨_, _⟩

Premises used: HomogeneousLocalization.den, IsLocalization.mk'_mul_cancel_left, Set.Mem, Subtype.mk
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ 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 ⋯) :
      Localization (M := A) x)
    ((algebraMap A (Localization (M := A) x) : (a : A) → at x) f.num : Localization (M := A) x)

Tactic:
exact IsLocalization.mk'_mul_cancel_left _ ⟨_, _⟩

Premises used: IsLocalization.mk'_mul_cancel_left, Subtype.mk
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
f g : HomogeneousLocalization 𝒜 x
⊢ f = g ↔ f.val = g.val

Tactic:
⟨congr_arg val, fun e ↦ val_injective x e⟩

Premises used: HomogeneousLocalization.val_injective, congr_arg, Iff.intro, HomogeneousLocalization.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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : AtPrime 𝒜 𝔭
⊢ IsUnit (val f) ↔ IsUnit f

Tactic:
⟨fun h1 ↦ ?_, IsUnit.map (algebraMap _ _)⟩

Premises used: Algebra.algebraMap, Iff.intro, IsUnit.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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : AtPrime 𝒜 𝔭
refine : ∀ (h1 : IsUnit (val f)), IsUnit f
⊢ IsUnit (val f) ↔ IsUnit f

Tactic:
refine ⟨fun h1 ↦ ?_, IsUnit.map (algebraMap _ _)⟩
-- 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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : AtPrime 𝒜 𝔭
h1 : IsUnit (val f)
rcases : ∀ (b : Localization (M := A) 𝔭.primeCompl) (eq0 : val f * b = 1) (eq1 : b * val f = 1), IsUnit f
⊢ IsUnit f

Tactic:
rcases h1 with ⟨⟨a, b, eq0, eq1⟩, rfl : a = f.val⟩

Premises used: rfl, HomogeneousLocalization.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 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
f : AtPrime 𝒜 𝔭
b : Localization (M := A) 𝔭.primeCompl
eq0 : val f * b = 1
eq1 : b * val f = 1
obtain : ∀ (f : NumDenSameDeg 𝒜 𝔭.primeCompl) (eq0 : (mk f).val * b = 1) (eq1 : b * (mk f).val = 1), IsUnit (mk f)
⊢ IsUnit f

Tactic:
obtain ⟨f, rfl⟩ := mk_surjective f

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 𝒜
𝔭 : 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
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)
⊢ IsUnit (mk f)

Tactic:
obtain ⟨b, s, rfl⟩ := IsLocalization.exists_mk'_eq 𝔭.primeCompl b

Premises used: Ideal.primeCompl, rfl, IsLocalization.exists_mk'_eq
-- 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 𝒜
𝔭 : 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
⊢ ∃ (c : ↥𝔭.primeCompl),
    (↑c : A) * ((↑f.num : A) * b) =
      (↑c : A) * (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝔭.primeCompl) (↑f.den : A) ⋯ * 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

Premises used: Localization.mk_eq_mk', HomogeneousLocalization.val_mk, IsLocalization.mk'_eq_iff_eq_mul, Ideal.primeCompl, one_mul, IsLocalization.eq_iff_exists, IsLocalization.mk'_mul
-- 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 𝒜
𝔭 : 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
eq0₁ :
  ∃ (c : ↥𝔭.primeCompl),
    (↑c : A) * ((↑f.num : A) * b) =
      (↑c : A) * (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝔭.primeCompl) (↑f.den : A) ⋯ * s) : A)
⊢ IsLocalization.mk' (Localization (M := A) 𝔭.primeCompl) b s * (mk f).val = 1

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

Premises used: Localization.mk_eq_mk', HomogeneousLocalization.val_mk, IsLocalization.mk'_eq_iff_eq_mul, Ideal.primeCompl, one_mul, IsLocalization.eq_iff_exists, IsLocalization.mk'_mul
-- 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 𝒜
𝔭 : 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
obtain :
  ∀ (c : ↥𝔭.primeCompl) (hc : (↑c : A) * ((↑f.num : A) * b) = (↑c : A) * ((↑f.den : A) * (↑s : A))), IsUnit (mk f)
⊢ IsUnit (mk f)

Tactic:
obtain ⟨c, hc : _ = c.1 * (f.den.1 * s.1)⟩ := eq0

Premises used: HMul.hMul, HomogeneousLocalization.NumDenSameDeg.den, Subtype.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 𝒜
𝔭 : 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))
⊢ (↑f.num : A) ∉ 𝔭

Tactic:
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))

Premises used: Eq.rec, HomogeneousLocalization.NumDenSameDeg.den_mem, Ideal.mul_mem_right, Ideal.mul_mem_left, Subtype.val, Not, Subtype.property, MulMemClass.mul_mem
-- 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 𝒜
𝔭 : 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))
⊢ (↑f.num : A) ∉ 𝔭

Tactic:
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))

Premises used: HomogeneousLocalization.NumDenSameDeg.den_mem, Subtype.property, MulMemClass.mul_mem
-- 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 𝒜
𝔭 : 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))
⊢ (↑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))
-- 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 𝒜
𝔭 : 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)

Tactic:
.of_mul_eq_one (Quotient.mk'' ⟨f.1, f.3, f.2, this⟩) ?_

Premises used: HomogeneousLocalization.NumDenSameDeg.num, IsUnit.of_mul_eq_one, Quotient.mk'', HomogeneousLocalization.NumDenSameDeg.mk, HomogeneousLocalization.NumDenSameDeg.den, HomogeneousLocalization.NumDenSameDeg.deg
-- 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 𝒜
𝔭 : 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) ∉ 𝔭
refine :
  mk f * Quotient.mk'' { deg := f.deg, num := f.den, den := f.num, den_mem := this : NumDenSameDeg 𝒜 𝔭.primeCompl } = 1
⊢ IsUnit (mk f)

Tactic:
refine .of_mul_eq_one (Quotient.mk'' ⟨f.1, f.3, f.2, this⟩) ?_
-- 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 𝒜
𝔭 : 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) ∉ 𝔭
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)
        ⋯))
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) 1)
⊢ mk f * Quotient.mk'' { deg := f.deg, num := f.den, den := f.num, den_mem := this : NumDenSameDeg 𝒜 𝔭.primeCompl } = 1

Tactic:
rw [← mk_mul, ext_iff_val, val_mk]

Premises used: HomogeneousLocalization.val_mk, HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.mk_mul
-- 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 𝒜
𝔭 : 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) ∉ 𝔭
⊢ 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)
        ⋯))
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) 1)

Tactic:
simp [mul_comm f.den.1]

Premises used: mul_comm, HomogeneousLocalization.NumDenSameDeg.den, Subtype.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
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
r : Eq (α := AtPrime 𝒜 𝔭) 0 1
⊢ False

Tactic:
simp [ext_iff_val, val_zero, val_one, zero_ne_one] at r

Premises used: HomogeneousLocalization.val_zero, HomogeneousLocalization.val_one, zero_ne_one, HomogeneousLocalization.ext_iff_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
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
𝔭 : Ideal A
inst_6 : 𝔭.IsPrime
a : AtPrime 𝒜 𝔭
⊢ IsUnit a ∨ IsUnit (1 - a)

Tactic:
simpa only [← isUnit_iff_isUnit_val, val_sub, val_one]
      using IsLocalRing.isUnit_or_isUnit_one_sub_self _

Premises used: IsLocalRing.isUnit_or_isUnit_one_sub_self, HomogeneousLocalization.val_one, HomogeneousLocalization.val_sub, 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 𝒜
f : A
d : ι
n : ℕ
hf : f ∈ 𝒜 d
x : A
hx : x ∈ 𝒜 (n • d)
w : ℕ
h : (fun (x : ℕ) ↦ f ^ x) n = f ^ n
⊢ Membership.mem (γ := Submonoid A) (Submonoid.powers f) (f ^ n)

Tactic:
use n
-- 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 : A
d : ι
n : ℕ
hf : f ∈ 𝒜 d
x : A
hx : x ∈ 𝒜 (n • d)
⊢ Eq (α := at Submonoid.powers f) (val (Away.mk 𝒜 hf n x hx))
    (Localization.mk x
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯))

Tactic:
rfl

Premises used: Localization.mk, Quotient.mk', OreLocalization.oreDiv, rfl, HomogeneousLocalization.NumDenSameDeg.embedding, HomogeneousLocalization.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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
x : Away 𝒜 f
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 := ⋯ })
⊢ ∃ (n : ℕ) (a : A) (ha : a ∈ 𝒜 (n • d)), Away.mk 𝒜 hf n a ha = x

Tactic:
obtain ⟨⟨N, ⟨s, hs⟩, ⟨b, hn⟩, ⟨n, (rfl : _ = b)⟩⟩, rfl⟩ := mk_surjective x

Premises used: HomogeneousLocalization.mk_surjective, rfl