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
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) ⋯))
⊢ Eq.{u_2 + 1} (α := Localization (M := A) x)
    ((fun (x1 x2 : Localization (M := A) x) ↦ x1 * x2)
      (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) ⋯)))
    ((fun (x1 x2 : Localization (M := A) x) ↦ x1 * x2)
      (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) ⋯)))

Tactic:
congr_arg₂ (· * ·) h h'

Premises used: HMul.hMul, congr_arg₂
-- 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
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) ⋯))
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)) ⋯) =
    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) ⋯))
⊢ 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)) ⋯))

Tactic:
convert! congr_arg₂ (· * ·) h h'

Premises used: HMul.hMul, congr_arg₂
-- 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
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₁ :
  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 ((↑c1.num : A) * (↑c3.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.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) ⋯))

Tactic:
rw [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
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₁ :
  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)) ⋯))
    (Localization.mk ((↑c2.num : A) * (↑c4.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : 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) ⋯))

Tactic:
rw [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
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) ⋯))
⊢ 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 ((↑c1.num : A) * (↑c3.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯))

Tactic:
rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
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) ⋯))
⊢ 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)) ⋯))
    (Localization.mk ((↑c2.num : A) * (↑c4.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) ⋯))

Tactic:
rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
i j : NumDenSameDeg 𝒜 x
⊢ mk (i * j) = mk i * mk j

Tactic:
rfl

Premises used: Quotient.map₂, 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
⊢ Eq (α := HomogeneousLocalization 𝒜 x) (mk 1) 1

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
⊢ Eq (α := HomogeneousLocalization 𝒜 x) (mk 0) 0

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
⊢ Eq (α := HomogeneousLocalization 𝒜 x) 0 (Quotient.mk'' 0)

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
⊢ Eq (α := HomogeneousLocalization 𝒜 x) 1 (Quotient.mk'' 1)

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
⊢ Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) 0) 0

Tactic:
Localization.mk_zero _

Premises used: Localization.mk, Quotient.liftOn', Set.Mem, Quotient.mk', OreLocalization.oreDiv, Localization.mk_zero, 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 𝒜
x : Submonoid A
⊢ Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) 1) 1

Tactic:
Localization.mk_one

Premises used: Localization.mk, Quotient.liftOn', Quotient.mk', Localization.mk_one, 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
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
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) ⋯))
    (Localization.mk
      ((↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y1.den : A) ⋯) : A) * (↑y2.num : A) +
        (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y2.den : A) ⋯) : A) * (↑y1.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y1.den : A) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y2.den : A) ⋯))
⊢ (HAdd.hAdd (α := HomogeneousLocalization 𝒜 x) (Quotient.mk'' y1) (Quotient.mk'' y2)).val =
    val (Quotient.mk'' y1) + val (Quotient.mk'' y2)

Tactic:
rw [← mk_add, val_mk, val_mk, val_mk, Localization.add_mk]

Premises used: HomogeneousLocalization.val_mk, Localization.add_mk, HomogeneousLocalization.mk_add
-- 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
y1 y2 : NumDenSameDeg 𝒜 x
⊢ 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) ⋯))
    (Localization.mk
      ((↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y1.den : A) ⋯) : A) * (↑y2.num : A) +
        (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y2.den : A) ⋯) : A) * (↑y1.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y1.den : A) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y2.den : A) ⋯))

Tactic:
rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
y1 y2 : NumDenSameDeg 𝒜 x
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) ⋯))
    (Localization.mk ((↑y1.num : A) * (↑y2.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y1.den : A) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y2.den : A) ⋯))
⊢ (HMul.hMul (α := HomogeneousLocalization 𝒜 x) (Quotient.mk'' y1) (Quotient.mk'' y2)).val =
    val (Quotient.mk'' y1) * val (Quotient.mk'' y2)

Tactic:
rw [← mk_mul, val_mk, val_mk, val_mk, Localization.mk_mul]

Premises used: HomogeneousLocalization.val_mk, HomogeneousLocalization.mk_mul, 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
y1 y2 : NumDenSameDeg 𝒜 x
⊢ 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) ⋯))
    (Localization.mk ((↑y1.num : A) * (↑y2.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y1.den : A) ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y2.den : A) ⋯))

Tactic:
rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
y1 y2 : HomogeneousLocalization 𝒜 x
rw : (y1 - y2).val = (y1 + -y2).val
⊢ (y1 - y2).val = y1.val - y2.val

Tactic:
rw [sub_eq_add_neg, ← val_neg, ← val_add]

Premises used: sub_eq_add_neg, HomogeneousLocalization.val_add, HomogeneousLocalization.val_neg
-- 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
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ (y1 - y2).val = (y1 + -y2).val

Tactic:
rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
y : NumDenSameDeg 𝒜 x
n : ℕ
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) ⋯))
    (Localization.mk ((↑y.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y.den : A) ⋯ ^ n))
⊢ (HPow.hPow (α := HomogeneousLocalization 𝒜 x) (Quotient.mk'' y) n).val = val (Quotient.mk'' y) ^ n

Tactic:
rw [← mk_pow, val_mk, val_mk, Localization.mk_pow]

Premises used: HomogeneousLocalization.mk_pow, HomogeneousLocalization.val_mk, Localization.mk_pow
-- 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
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ 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) ⋯))
    (Localization.mk ((↑y.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y.den : A) ⋯ ^ n))

Tactic:
rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
n : ℕ
zero : Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (Nat.unaryCast 0)) (↑0 : at x)
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)
⊢ Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) n.unaryCast) (↑n : at x)

Tactic:
induction 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 𝒜
x : Submonoid A
⊢ Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (Nat.unaryCast 0)) (↑0 : at x)

Tactic:
simp [Nat.unaryCast, *]

Premises used: Nat.unaryCast
-- 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
n : ℕ
h : 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:
simp [Nat.unaryCast, *]

Premises used: Nat.unaryCast
-- 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
n : ℤ
ofNat :
  ∀ (a : ℕ),
    Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (Int.ofNat a).castDef)
      (↑(Int.ofNat a) : at x)
negSucc :
  ∀ (a : ℕ),
    Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (Int.negSucc a).castDef)
      (↑(Int.negSucc a) : at x)
⊢ Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) n.castDef) (↑n : at x)

Tactic:
cases 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 𝒜
x : Submonoid A
a : ℕ
⊢ Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (Int.ofNat a).castDef)
    (↑(Int.ofNat a) : at x)

Tactic:
simp [Int.castDef, *]

Premises used: Int.castDef
-- 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
a : ℕ
⊢ Eq (α := Localization (M := A) x) (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) (Int.negSucc a).castDef)
    (↑(Int.negSucc a) : at x)

Tactic:
simp [Int.castDef, *]

Premises used: Int.castDef
-- 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
y : HomogeneousLocalization 𝒜 x
⊢ (algebraMap (HomogeneousLocalization 𝒜 x) (Localization (M := A) x) : (a : HomogeneousLocalization 𝒜 x) → at x) y =
    y.val

Tactic:
rfl

Premises used: Quotient.liftOn', 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 𝒜
x : Submonoid A
f : NumDenSameDeg 𝒜 x
h : f.num = 0
a : (mk f).val = val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) 0
⊢ mk f = 0

Tactic:
apply val_injective

Premises used: HomogeneousLocalization.val_injective
-- 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 : NumDenSameDeg 𝒜 x
h : f.num = 0
⊢ (mk f).val = val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) 0

Tactic:
simp only [val_mk, val_zero, h, ZeroMemClass.coe_zero, Localization.mk_zero]

Premises used: HomogeneousLocalization.val_zero, HomogeneousLocalization.val_mk, ZeroMemClass.coe_zero, Localization.mk_zero
-- 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 : NumDenSameDeg 𝒜 x
h : f.den = 0
⊢ Subsingleton (HomogeneousLocalization 𝒜 x)

Tactic:
have := subsingleton 𝒜 (h ▸ f.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
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
f : NumDenSameDeg 𝒜 x
h : f.den = 0
this : Subsingleton (HomogeneousLocalization 𝒜 x)
⊢ mk f = 0

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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 : NumDenSameDeg 𝒜 x
h : f.den = 0
this : Subsingleton (HomogeneousLocalization 𝒜 x)
⊢ mk f = 0

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim