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
𝒜 : ι → σ
x : Submonoid A
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1) : A) ∈ x
i2 : ι
n2 : A
hn2 : n2 ∈ 𝒜 i2
d2 : A
hd2 : d2 ∈ 𝒜 i2
h2 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) d2 hd2) : A) ∈ x
hdeg : i1 = i2
hnum : n1 = n2
hden : d1 = d2
subst :
  ∀ (hn2 : n1 ∈ 𝒜 i1) (hd2 : d1 ∈ 𝒜 i1) (h2 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd2) : A) ∈ x),
    { deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x } =
      { deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn2,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd2, den_mem := h2 }
⊢ { deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x } =
    { deg := i2, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) n2 hn2,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i2) d2 hd2, den_mem := h2 }

Tactic:
subst hdeg hnum hden
-- 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
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1) : A) ∈ x
hn2 : n1 ∈ 𝒜 i1
hd2 : d1 ∈ 𝒜 i1
h2 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd2) : A) ∈ x
⊢ { deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn1,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1, den_mem := h1 : NumDenSameDeg 𝒜 x } =
    { deg := i1, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) n1 hn2,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd2, den_mem := h2 }

Tactic:
congr
-- 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 : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
c : NumDenSameDeg 𝒜 x
⊢ (-c).deg = c.deg

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 : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
c : NumDenSameDeg 𝒜 x
⊢ (↑(-c).num : A) = -(↑c.num : A)

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 : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
c : NumDenSameDeg 𝒜 x
⊢ (↑(-c).den : A) = (↑c.den : A)

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
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst_2 : SMul α A
inst_3 : SMulMemClass σ α A
c : NumDenSameDeg 𝒜 x
m : α
⊢ (m • c).deg = c.deg

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
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst_2 : SMul α A
inst_3 : SMulMemClass σ α A
c : NumDenSameDeg 𝒜 x
m : α
⊢ (↑(m • c).num : A) = m • (↑c.num : A)

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
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst_2 : SMul α A
inst_3 : SMulMemClass σ α A
c : NumDenSameDeg 𝒜 x
m : α
⊢ (↑(m • c).den : A) = (↑c.den : A)

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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
⊢ Eq.{u_1 + 1} (α := ι) (deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := x) 1) 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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
⊢ (↑(num 1) : A) = 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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
⊢ (↑(den 1) : A) = 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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
⊢ Eq.{u_1 + 1} (α := ι) (deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := x) 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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
⊢ Eq (α := ↥(𝒜 (deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := x) 0))) (num 0) 0

Tactic:
rfl

Premises used: Set.Mem, 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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
⊢ (↑(den 0) : A) = 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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c1 c2 : NumDenSameDeg 𝒜 x
⊢ (c1 * c2).deg = c1.deg + c2.deg

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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c1 c2 : NumDenSameDeg 𝒜 x
⊢ (↑(c1 * c2).num : A) = (↑c1.num : A) * (↑c2.num : A)

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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c1 c2 : NumDenSameDeg 𝒜 x
⊢ (↑(c1 * c2).den : A) = (↑c1.den : A) * (↑c2.den : A)

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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c1 c2 : NumDenSameDeg 𝒜 x
⊢ (c1 + c2).deg = c1.deg + c2.deg

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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c1 c2 : NumDenSameDeg 𝒜 x
⊢ (↑(c1 + c2).num : A) = (↑c1.den : A) * (↑c2.num : A) + (↑c2.den : A) * (↑c1.num : A)

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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c1 c2 : NumDenSameDeg 𝒜 x
⊢ (↑(c1 + c2).den : A) = (↑c1.den : A) * (↑c2.den : A)

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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
⊢ (↑(@GradedMonoid.GMonoid.gnpow _ (fun (i : ι) ↦ ↥(𝒜 i)) AddCommMonoid.toAddMonoid _ 0 _ c.den :
          ↥(𝒜 (HSMul.hSMul (α := ℕ) 0 c.deg))) :
      A) ∈
    x

Tactic:
simp only [coe_gnpow, pow_zero, one_mem]

Premises used: pow_zero, SetLike.coe_gnpow, OneMemClass.one_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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
n : ℕ
ih :
  (↑(@GradedMonoid.GMonoid.gnpow _ (fun (i : ι) ↦ ↥(𝒜 i)) AddCommMonoid.toAddMonoid _ n _ c.den : ↥(𝒜 (n • c.deg))) :
      A) ∈
    x
⊢ (↑(@GradedMonoid.GMonoid.gnpow _ (fun (i : ι) ↦ ↥(𝒜 i)) AddCommMonoid.toAddMonoid _ (n + 1) _ c.den :
          ↥(𝒜 ((n + 1) • c.deg))) :
      A) ∈
    x

Tactic:
simpa only [pow_succ, coe_gnpow] using x.mul_mem ih c.den_mem

Premises used: Submonoid.mul_mem, pow_succ, HomogeneousLocalization.NumDenSameDeg.den_mem, SetLike.coe_gnpow
-- 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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
n : ℕ
zero :
  (↑(@GradedMonoid.GMonoid.gnpow _ (fun (i : ι) ↦ ↥(𝒜 i)) AddCommMonoid.toAddMonoid _ 0 _ c.den :
          ↥(𝒜 (HSMul.hSMul (α := ℕ) 0 c.deg))) :
      A) ∈
    x
succ :
  ∀ (n : ℕ)
    (ih :
      (↑(@GradedMonoid.GMonoid.gnpow _ (fun (i : ι) ↦ ↥(𝒜 i)) AddCommMonoid.toAddMonoid _ n _ c.den :
              ↥(𝒜 (n • c.deg))) :
          A) ∈
        x),
    (↑(@GradedMonoid.GMonoid.gnpow _ (fun (i : ι) ↦ ↥(𝒜 i)) AddCommMonoid.toAddMonoid _ (n + 1) _ c.den :
            ↥(𝒜 ((n + 1) • c.deg))) :
        A) ∈
      x
⊢ (↑(@GradedMonoid.GMonoid.gnpow _ (fun (i : ι) ↦ ↥(𝒜 i)) AddCommMonoid.toAddMonoid _ n _ c.den : ↥(𝒜 (n • c.deg))) :
      A) ∈
    x

Tactic:
induction n with
        | zero => simp only [coe_gnpow, pow_zero, one_mem]
        | succ n ih => simpa only [pow_succ, coe_gnpow] using x.mul_mem ih c.den_mem

Premises used: pow_succ, pow_zero, SetLike.coe_gnpow, Submodule.zero, OneMemClass.one_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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
n : ℕ
⊢ (c ^ n).deg = n • c.deg

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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
n : ℕ
⊢ (↑(c ^ n).num : A) = (↑c.num : A) ^ n

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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
n : ℕ
⊢ (↑(c ^ n).den : A) = (↑c.den : A) ^ n

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
𝒜 : ι → σ
x : Submonoid A
⊢ Function.Surjective (α := NumDenSameDeg 𝒜 x) mk

Tactic:
Quotient.mk''_surjective

Premises used: HomogeneousLocalization, Quotient.mk''_surjective
-- 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
i : NumDenSameDeg 𝒜 x
⊢ (mk i).val = Localization.mk (↑i.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑i.den : A) ⋯)

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
𝒜 : ι → σ
x : Submonoid A
⊢ Function.Injective (α := HomogeneousLocalization 𝒜 x) val

Tactic:
fun a b => Quotient.recOnSubsingleton₂' a b fun _ _ h => Quotient.sound' h

Premises used: Quotient.recOnSubsingleton₂', Function.Injective
-- 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
hx : 0 ∈ x
⊢ Subsingleton (HomogeneousLocalization 𝒜 x)

Tactic:
have := IsLocalization.subsingleton (S := at x) hx
  (HomogeneousLocalization.val_injective (𝒜 := 𝒜) (x := x)).subsingleton

Premises used: Function.Injective.subsingleton, HomogeneousLocalization.val_injective, IsLocalization.subsingleton
-- 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
α : Type u_4
inst_2 : SMul α A
inst_3 : IsScalarTower α A A
inst_4 : SMulMemClass σ α A
m : α
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) ⋯))
simp :
  Eq (α := Localization (M := A) x)
    (Localization.mk (m • (↑c1.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
    (Localization.mk (m • (↑c2.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
⊢ Eq (α := Localization (M := A) x)
    (Localization.mk (↑(num ((fun (x_1 : NumDenSameDeg 𝒜 x) ↦ m • x_1) c1)) : A)
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑(den ((fun (x_1 : NumDenSameDeg 𝒜 x) ↦ m • x_1) c1)) : A) ⋯))
    (Localization.mk (↑(num ((fun (x_1 : NumDenSameDeg 𝒜 x) ↦ m • x_1) c2)) : A)
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑(den ((fun (x_1 : NumDenSameDeg 𝒜 x) ↦ m • x_1) c2)) : A) ⋯))

Tactic:
simp only [num_smul, den_smul]

Premises used: HomogeneousLocalization.NumDenSameDeg.den_smul, HomogeneousLocalization.NumDenSameDeg.num_smul
-- 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
α : Type u_4
inst_2 : SMul α A
inst_3 : IsScalarTower α A A
inst_4 : SMulMemClass σ α A
m : α
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) ⋯))
⊢ Eq.{u_2 + 1} (α := Localization (M := A) x)
    ((fun (z : Localization (M := A) x) ↦ m • z)
      (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯)))
    ((fun (z : Localization (M := A) x) ↦ m • z)
      (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯)))

Tactic:
congr_arg (fun z : at x => m • z) h

Premises used: congr_arg, HSMul.hSMul
-- 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
α : Type u_4
inst_2 : SMul α A
inst_3 : IsScalarTower α A A
inst_4 : SMulMemClass σ α A
m : α
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) ⋯))
h₁ :
  Localization.mk (m • (↑c1.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯) =
    HSMul.hSMul (β := Localization (M := A) x) m
      (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
h₂ :
  Localization.mk (m • (↑c2.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯) =
    HSMul.hSMul (β := Localization (M := A) x) m
      (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
⊢ Eq (α := Localization (M := A) x)
    (Localization.mk (m • (↑c1.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
    (Localization.mk (m • (↑c2.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))

Tactic:
convert! congr_arg (fun z : at x => m • z) h

Premises used: congr_arg, HSMul.hSMul
-- 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
α : Type u_4
inst_2 : SMul α A
inst_3 : IsScalarTower α A A
inst_4 : SMulMemClass σ α A
m : α
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) ⋯))
h₁ h₂ :
  Eq (α := Localization (M := A) x)
    (Localization.mk (m • (↑c1.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
    (Localization.mk (m • (↑c1.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
⊢ Localization.mk (m • (↑c1.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯) =
    HSMul.hSMul (β := Localization (M := A) x) m
      (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))

Tactic:
rw [Localization.smul_mk]

Premises used: Localization.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
α : Type u_4
inst_2 : SMul α A
inst_3 : IsScalarTower α A A
inst_4 : SMulMemClass σ α A
m : α
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) ⋯))
h₁ h₂ :
  Eq (α := Localization (M := A) x)
    (Localization.mk (m • (↑c2.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
    (Localization.mk (m • (↑c2.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
⊢ Localization.mk (m • (↑c2.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯) =
    HSMul.hSMul (β := Localization (M := A) x) m
      (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))

Tactic:
rw [Localization.smul_mk]

Premises used: Localization.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
α : Type u_4
inst_2 : SMul α A
inst_3 : IsScalarTower α A A
inst_4 : SMulMemClass σ α A
i : NumDenSameDeg 𝒜 x
m : α
⊢ mk (m • i) = m • mk i

Tactic:
rfl

Premises used: Quot.map, 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
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst_2 : SMul α A
inst_3 : IsScalarTower α A A
inst_4 : SMulMemClass σ α A
n : α
x_1 : NumDenSameDeg 𝒜 x
rw :
  Eq (α := Localization (M := A) x)
    (Localization.mk (n • (↑x_1.num : A)) (Subtype.mk (p := fun (x_2 : A) ↦ x_2 ∈ x) (↑(n • x_1).den : A) ⋯))
    (Localization.mk (n • (↑x_1.num : A)) (Subtype.mk (p := fun (x_2 : A) ↦ x_2 ∈ x) (↑x_1.den : A) ⋯))
⊢ (HSMul.hSMul (β := HomogeneousLocalization 𝒜 x) n (Quotient.mk'' x_1)).val = n • val (Quotient.mk'' x_1)

Tactic:
rw [← mk_smul, val_mk, val_mk, Localization.smul_mk, num_smul]

Premises used: HomogeneousLocalization.mk_smul, HomogeneousLocalization.val_mk, Localization.smul_mk, HomogeneousLocalization.NumDenSameDeg.num_smul
-- 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
α : Type u_4
inst_2 : SMul α A
inst_3 : IsScalarTower α A A
inst_4 : SMulMemClass σ α A
n : α
x_1 : NumDenSameDeg 𝒜 x
⊢ Eq (α := Localization (M := A) x)
    (Localization.mk (n • (↑x_1.num : A)) (Subtype.mk (p := fun (x_2 : A) ↦ x_2 ∈ x) (↑(n • x_1).den : A) ⋯))
    (Localization.mk (n • (↑x_1.num : A)) (Subtype.mk (p := fun (x_2 : A) ↦ x_2 ∈ x) (↑x_1.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 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
n : ℕ
y : HomogeneousLocalization 𝒜 x
rw : n • y.val = n • y.val
rw₁ rw₂ : n • y.val = n • y.val
⊢ (n • y).val = n • y.val

Tactic:
rw [val_smul, OreLocalization.nsmul_eq_nsmul]

Premises used: OreLocalization.nsmul_eq_nsmul, HomogeneousLocalization.val_smul
-- 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
n : ℤ
y : HomogeneousLocalization 𝒜 x
rw : n • y.val = n • y.val
rw₁ rw₂ : n • y.val = n • y.val
⊢ (n • y).val = n • y.val

Tactic:
rw [val_smul, OreLocalization.zsmul_eq_zsmul]

Premises used: HomogeneousLocalization.val_smul, OreLocalization.zsmul_eq_zsmul
-- 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 : NegMemClass σ A
𝒜 : ι → σ
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) ⋯))
simp :
  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) ⋯))
⊢ 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) ⋯))

Tactic:
simp only [num_neg, den_neg, ← Localization.neg_mk]

Premises used: HomogeneousLocalization.NumDenSameDeg.num_neg, HomogeneousLocalization.NumDenSameDeg.den_neg, Localization.neg_mk
-- 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 : NegMemClass σ A
𝒜 : ι → σ
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) ⋯))
⊢ 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) ⋯))

Tactic:
congr_arg Neg.neg h

Premises used: congr_arg, Neg.neg