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 : 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:
exact congr_arg Neg.neg h

Premises used: congr_arg, Neg.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 : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
i : NumDenSameDeg 𝒜 x
⊢ mk (-i) = -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
inst_2 : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
y : NumDenSameDeg 𝒜 x
rw :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑(-y).num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑(-y).den : A) ⋯))
    (Localization.mk (-(↑y.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y.den : A) ⋯))
⊢ val (-Quotient.mk'' y) = -val (Quotient.mk'' y)

Tactic:
rw [← mk_neg, val_mk, val_mk, Localization.neg_mk]

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

Tactic:
simp only [num_pow, den_pow]

Premises used: HomogeneousLocalization.NumDenSameDeg.num_pow, HomogeneousLocalization.NumDenSameDeg.den_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
z : HomogeneousLocalization 𝒜 x
n : ℕ
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) ↦ z ^ n)
      (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯)))
    ((fun (z : Localization (M := A) x) ↦ z ^ n)
      (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 => z ^ n) h

Premises used: congr_arg, HPow.hPow
-- 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
z : HomogeneousLocalization 𝒜 x
n : ℕ
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 ((↑c1.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) ^ n) ⋯) =
    HPow.hPow (α := Localization (M := A) x)
      (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯)) n
h₂ :
  Localization.mk ((↑c2.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) ^ n) ⋯) =
    HPow.hPow (α := Localization (M := A) x)
      (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯)) n
⊢ Eq (α := Localization (M := A) x)
    (Localization.mk ((↑c1.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) ^ n) ⋯))
    (Localization.mk ((↑c2.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) ^ n) ⋯))

Tactic:
convert! congr_arg (fun z : at x => z ^ n) h

Premises used: congr_arg, HPow.hPow
-- 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
z : HomogeneousLocalization 𝒜 x
n : ℕ
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₁ :
  Eq (α := Localization (M := A) x)
    (Localization.mk ((↑c1.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) ^ n) ⋯))
    (Localization.mk ((↑c1.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯ ^ n))
⊢ Localization.mk ((↑c1.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) ^ n) ⋯) =
    HPow.hPow (α := Localization (M := A) x)
      (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯)) n

Tactic:
rw [Localization.mk_pow]

Premises used: 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
z : HomogeneousLocalization 𝒜 x
n : ℕ
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₁ :
  Eq (α := Localization (M := A) x)
    (Localization.mk ((↑c2.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) ^ n) ⋯))
    (Localization.mk ((↑c2.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯ ^ n))
⊢ Localization.mk ((↑c2.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) ^ n) ⋯) =
    HPow.hPow (α := Localization (M := A) x)
      (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯)) n

Tactic:
rw [Localization.mk_pow]

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

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
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) ⋯))
simp :
  Eq (α := Localization (M := A) x)
    (Localization.mk ((↑c1.den : A) * (↑c3.num : A) + (↑c3.den : A) * (↑c1.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) ⋯))
    (Localization.mk ((↑c2.den : A) * (↑c4.num : A) + (↑c4.den : A) * (↑c2.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) * (↑c4.den : A)) ⋯))
⊢ Eq (α := Localization (M := A) x)
    (Localization.mk (↑(num ((fun (x1 x2 : NumDenSameDeg 𝒜 x) ↦ x1 + x2) c1 c3)) : A)
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑(den ((fun (x1 x2 : NumDenSameDeg 𝒜 x) ↦ x1 + x2) c1 c3)) : A) ⋯))
    (Localization.mk (↑(num ((fun (x1 x2 : NumDenSameDeg 𝒜 x) ↦ x1 + x2) c2 c4)) : A)
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑(den ((fun (x1 x2 : NumDenSameDeg 𝒜 x) ↦ x1 + x2) c2 c4)) : A) ⋯))

Tactic:
simp only [num_add, den_add]

Premises used: HomogeneousLocalization.NumDenSameDeg.den_add, HomogeneousLocalization.NumDenSameDeg.num_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
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: HAdd.hAdd, 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.den : A) * (↑c3.num : A) + (↑c3.den : A) * (↑c1.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) ⋯) =
    HAdd.hAdd (α := 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.den : A) * (↑c4.num : A) + (↑c4.den : A) * (↑c2.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) * (↑c4.den : A)) ⋯) =
    HAdd.hAdd (α := 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.den : A) * (↑c3.num : A) + (↑c3.den : A) * (↑c1.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) ⋯))
    (Localization.mk ((↑c2.den : A) * (↑c4.num : A) + (↑c4.den : A) * (↑c2.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: HAdd.hAdd, 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.den : A) * (↑c3.num : A) + (↑c3.den : A) * (↑c1.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) ⋯))
    (Localization.mk
      ((↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯) : A) * (↑c3.num : A) +
        (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯) : A) * (↑c1.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.den : A) * (↑c3.num : A) + (↑c3.den : A) * (↑c1.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) ⋯) =
    HAdd.hAdd (α := 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.add_mk]

Premises used: Localization.add_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 : 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.den : A) * (↑c4.num : A) + (↑c4.den : A) * (↑c2.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) * (↑c4.den : A)) ⋯))
    (Localization.mk
      ((↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯) : A) * (↑c4.num : A) +
        (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) ⋯) : A) * (↑c2.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.den : A) * (↑c4.num : A) + (↑c4.den : A) * (↑c2.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) * (↑c4.den : A)) ⋯) =
    HAdd.hAdd (α := 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.add_mk]

Premises used: Localization.add_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 : 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.den : A) * (↑c3.num : A) + (↑c3.den : A) * (↑c1.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) ⋯))
    (Localization.mk
      ((↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯) : A) * (↑c3.num : A) +
        (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯) : A) * (↑c1.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.den : A) * (↑c4.num : A) + (↑c4.den : A) * (↑c2.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) * (↑c4.den : A)) ⋯))
    (Localization.mk
      ((↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯) : A) * (↑c4.num : A) +
        (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) ⋯) : A) * (↑c2.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
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) ⋯))
simp :
  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)) ⋯))
⊢ Eq (α := Localization (M := A) x)
    (Localization.mk (↑(num ((fun (x1 x2 : NumDenSameDeg 𝒜 x) ↦ x1 * x2) c1 c3)) : A)
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑(den ((fun (x1 x2 : NumDenSameDeg 𝒜 x) ↦ x1 * x2) c1 c3)) : A) ⋯))
    (Localization.mk (↑(num ((fun (x1 x2 : NumDenSameDeg 𝒜 x) ↦ x1 * x2) c2 c4)) : A)
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑(den ((fun (x1 x2 : NumDenSameDeg 𝒜 x) ↦ x1 * x2) c2 c4)) : A) ⋯))

Tactic:
simp only [num_mul, den_mul]

Premises used: HomogeneousLocalization.NumDenSameDeg.num_mul, HomogeneousLocalization.NumDenSameDeg.den_mul