awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
𝒜 : ι → σ
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) ⋯))
⊢ 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) ⋯))
have 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) sorry))
  (Localization.mk (m • (↑c2.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) sorry))
Tactic: rw [Localization.smul_mk]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
𝒜 : ι → σ
x : Submonoid A
α : Type u_4
inst_2 : SMul α A
inst_3 : IsScalarTower α A A
inst_4 : SMulMemClass σ α A
n : α
x_1 : NumDenSameDeg 𝒜 x
⊢ (HSMul.hSMul (β := HomogeneousLocalization 𝒜 x) n (Quotient.mk'' x_1)).val = n • val (Quotient.mk'' x_1)
have 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) sorry))
  (Localization.mk (n • (↑x_1.num : A)) (Subtype.mk (p := fun (x_2 : A) ↦ x_2 ∈ x) (↑x_1.den : A) sorry))
Tactic: rw [← mk_smul, val_mk, val_mk, Localization.smul_mk, num_smul]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
n : ℕ
y : HomogeneousLocalization 𝒜 x
⊢ (n • y).val = n • y.val
have rw : n • y.val = n • y.val
Tactic: rw [val_smul, OreLocalization.nsmul_eq_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
n : ℕ
y : HomogeneousLocalization 𝒜 x
rw : n • y.val = n • y.val
⊢ (n • y).val = n • y.val
have rw₁ : n • y.val = n • y.val
Tactic: rw [val_smul, OreLocalization.nsmul_eq_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ι → σ
x : Submonoid A
n : ℤ
y : HomogeneousLocalization 𝒜 x
⊢ (n • y).val = n • y.val
have rw : n • y.val = n • y.val
Tactic: rw [val_smul, OreLocalization.zsmul_eq_zsmul]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ι → σ
x : Submonoid A
n : ℤ
y : HomogeneousLocalization 𝒜 x
rw : n • y.val = n • y.val
⊢ (n • y).val = n • y.val
have rw₁ : n • y.val = n • y.val
Tactic: rw [val_smul, OreLocalization.zsmul_eq_zsmul]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : 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) ⋯))
have simp : Eq (α := Localization (M := A) x)
  (-Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) sorry))
  (-Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) sorry))
Tactic: simp only [num_neg, den_neg, ← Localization.neg_mk]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ val (-Quotient.mk'' y) = -val (Quotient.mk'' y)
have rw : Eq (α := Localization (M := A) x)
  (Localization.mk (↑(-y).num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑(-y).den : A) sorry))
  (Localization.mk (-(↑y.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑y.den : A) sorry))
Tactic: rw [← mk_neg, val_mk, val_mk, Localization.neg_mk]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
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 (↑(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) ⋯))
have 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) sorry))
  (Localization.mk ((↑c2.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) ^ n) sorry))
Tactic: simp only [num_pow, den_pow]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
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 ((↑c2.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) ^ n) ⋯))
have h₁ : Localization.mk ((↑c1.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) ^ n) sorry) =
  HPow.hPow (α := Localization (M := A) x)
    (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) sorry)) n
Tactic: convert! congr_arg (fun z : at x => z ^ n) h
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
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
⊢ 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) ⋯))
have h₂ : Localization.mk ((↑c2.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) ^ n) sorry) =
  HPow.hPow (α := Localization (M := A) x)
    (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) sorry)) n
Tactic: convert! congr_arg (fun z : at x => z ^ n) h
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
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) ⋯))
⊢ 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
have 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) sorry))
  (Localization.mk ((↑c1.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) sorry ^ n))
Tactic: rw [Localization.mk_pow]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
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) ⋯))
⊢ 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
have 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) sorry))
  (Localization.mk ((↑c2.num : A) ^ n) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) sorry ^ n))
Tactic: rw [Localization.mk_pow]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
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 (↑(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) ⋯))
have 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)) sorry))
  (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)) sorry))
Tactic: simp only [num_add, den_add]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
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 ((↑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)) ⋯))
have 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)) sorry) =
  HAdd.hAdd (α := Localization (M := A) x)
    (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) sorry))
    (Localization.mk (↑c3.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) sorry))
Tactic: convert! congr_arg₂ (· + ·) h h'
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
    (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
c3 c4 : NumDenSameDeg 𝒜 x
h' :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c3.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯))
    (Localization.mk (↑c4.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) ⋯))
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) ⋯))
⊢ 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)) ⋯))
have 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)) sorry) =
  HAdd.hAdd (α := Localization (M := A) x)
    (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) sorry))
    (Localization.mk (↑c4.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) sorry))
Tactic: convert! congr_arg₂ (· + ·) h h'
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
    (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
c3 c4 : NumDenSameDeg 𝒜 x
h' :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c3.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯))
    (Localization.mk (↑c4.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) ⋯))
⊢ Localization.mk ((↑c1.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) ⋯))
have 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)) sorry))
  (Localization.mk
    ((↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) sorry) : A) * (↑c3.num : A) +
      (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) sorry) : A) * (↑c1.num : A))
    (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) sorry *
      Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) sorry))
Tactic: rw [Localization.add_mk]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
    (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
c3 c4 : NumDenSameDeg 𝒜 x
h' :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c3.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯))
    (Localization.mk (↑c4.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) ⋯))
⊢ Localization.mk ((↑c2.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) ⋯))
have 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)) sorry))
  (Localization.mk
    ((↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) sorry) : A) * (↑c4.num : A) +
      (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) sorry) : A) * (↑c2.num : A))
    (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) sorry *
      Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) sorry))
Tactic: rw [Localization.add_mk]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
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 (↑(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) ⋯))
have 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)) sorry))
  (Localization.mk ((↑c2.num : A) * (↑c4.num : A))
    (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) * (↑c4.den : A)) sorry))
Tactic: simp only [num_mul, den_mul]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (goal)
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) ⋯))
    (Localization.mk (↑c2.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) ⋯))
c3 c4 : NumDenSameDeg 𝒜 x
h' :
  Eq (α := Localization (M := A) x)
    (Localization.mk (↑c3.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) ⋯))
    (Localization.mk (↑c4.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c4.den : A) ⋯))
⊢ Eq (α := Localization (M := A) x)
    (Localization.mk ((↑c1.num : A) * (↑c3.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) ⋯))
    (Localization.mk ((↑c2.num : A) * (↑c4.num : A))
      (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c2.den : A) * (↑c4.den : A)) ⋯))
have h₁ : Localization.mk ((↑c1.num : A) * (↑c3.num : A))
    (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) ((↑c1.den : A) * (↑c3.den : A)) sorry) =
  HMul.hMul (α := Localization (M := A) x)
    (Localization.mk (↑c1.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) sorry))
    (Localization.mk (↑c3.num : A) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c3.den : A) sorry))
Tactic: convert! congr_arg₂ (· * ·) h h'