awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
i : ι
x : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
mem :
  ∀ (x : A) (hx : x ∈ s) (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have zero : ∀ (i : ι),
  Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) i) : A)
Tactic: induction hx using Subsemiring.closure_induction generalizing i with
  | mem _ hx => exact Subsemiring.subset_closure <| h i hx
  | zero => simp
  | one =>
    rw [decompose_one, one_def]
    obtain rfl | h := eq_or_ne i 0 <;> simp [of_eq_of_ne, *]
  | add _ _ _ _ h₁ h₂ => simpa using add_mem (h₁ i) (h₂ i)
  | mul x y _ _ h₁ h₂ =>
    classical
    rw [decompose_mul, DirectSum.mul_eq_dfinsuppSum]
    rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
    refine sum_mem fun j _ ↦ ?_
    rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
    refine sum_mem fun k _ ↦ ?_
    obtain rfl | h := eq_or_ne i (j + k) <;> simp [of_eq_of_ne, mul_mem, *]
Cleared hypotheses: i, hx
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
i : ι
x : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
mem :
  ∀ (x : A) (hx : x ∈ s) (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
zero :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) i) : A)
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have one : ∀ (i : ι),
  Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 1 : (a : ι) → ↥(𝒜 a)) i) : A)
Tactic: induction hx using Subsemiring.closure_induction generalizing i with
  | mem _ hx => exact Subsemiring.subset_closure <| h i hx
  | zero => simp
  | one =>
    rw [decompose_one, one_def]
    obtain rfl | h := eq_or_ne i 0 <;> simp [of_eq_of_ne, *]
  | add _ _ _ _ h₁ h₂ => simpa using add_mem (h₁ i) (h₂ i)
  | mul x y _ _ h₁ h₂ =>
    classical
    rw [decompose_mul, DirectSum.mul_eq_dfinsuppSum]
    rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
    refine sum_mem fun j _ ↦ ?_
    rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
    refine sum_mem fun k _ ↦ ?_
    obtain rfl | h := eq_or_ne i (j + k) <;> simp [of_eq_of_ne, mul_mem, *]
Cleared hypotheses: i, hx
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h :
  ∀ (i : ι) ⦃x : A⦄,
    x ∈ s → (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ s
i : ι
x : A
hx : Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x
mem :
  ∀ (x : A) (hx : x ∈ s) (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
zero :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) i) : A)
one :
  ∀ (i : ι),
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
      (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 1 : (a : ι) → ↥(𝒜 a)) i) : A)
⊢ Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
have add : ∀ (x y : A),
  Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) x →
    Membership.mem (γ := Subsemiring A) (Subsemiring.closure s) y →
      ∀
        (h₁ :
          ∀ (i : ι),
            Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
              (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))
        (h₂ :
          ∀ (i : ι),
            Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
              (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) y : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A))
        (i : ι),
        Membership.mem (γ := Subsemiring A) (Subsemiring.closure s)
          (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (x + y) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A)
Tactic: induction hx using Subsemiring.closure_induction generalizing i with
  | mem _ hx => exact Subsemiring.subset_closure <| h i hx
  | zero => simp
  | one =>
    rw [decompose_one, one_def]
    obtain rfl | h := eq_or_ne i 0 <;> simp [of_eq_of_ne, *]
  | add _ _ _ _ h₁ h₂ => simpa using add_mem (h₁ i) (h₂ i)
  | mul x y _ _ h₁ h₂ =>
    classical
    rw [decompose_mul, DirectSum.mul_eq_dfinsuppSum]
    rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
    refine sum_mem fun j _ ↦ ?_
    rw [DFinsupp.sum_apply, DFinsupp.sum, AddSubmonoidClass.coe_finsetSum]
    refine sum_mem fun k _ ↦ ?_
    obtain rfl | h := eq_or_ne i (j + k) <;> simp [of_eq_of_ne, mul_mem, *]
Cleared hypotheses: i, hx
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
⊢ IsHomogeneous 𝒜 (P := Subsemiring A) (Subsemiring.closure s)
have rw : IsHomogeneous 𝒜 (P := Subsemiring A) (Subsemiring.closure (insert 0 s))
Tactic: rw [← Subsemiring.closure_insert_zero s]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
⊢ IsHomogeneous 𝒜 (P := Subsemiring A) (Subsemiring.closure (insert 0 s))
have refine : ∀ (i : ι) (x : A) (hx : x ∈ insert 0 s),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
Tactic: refine IsHomogeneous.subsemiringClosure fun i x hx ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx : x ∈ insert 0 s
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
have inl : ∀ (hx : 0 ∈ insert 0 s), (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
Tactic: obtain rfl | hx := mem_insert_iff.mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx : x ∈ insert 0 s
inl :
  ∀ (hx : 0 ∈ insert 0 s), (↑(((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) 0 : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
have inr : ∀ (hx : x ∈ s),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
Tactic: obtain rfl | hx := mem_insert_iff.mp hx
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx_1 : x ∈ insert 0 s
hx : x ∈ s
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
have inr : ∀ (j : ι) (hj : x ∈ 𝒜 j),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
Tactic: obtain ⟨j, hj⟩ := h x hx
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx_1 : x ∈ insert 0 s
hx : x ∈ s
j : ι
hj : x ∈ 𝒜 j
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
have inr : ∀ (hj : x ∈ 𝒜 i),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
Tactic: obtain rfl | h := eq_or_ne i j
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring (goal)
Goal:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst : AddMonoid ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx_1 : x ∈ insert 0 s
hx : x ∈ s
j : ι
hj : x ∈ 𝒜 j
inr :
  ∀ (hj : x ∈ 𝒜 i),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
have inr₁ : ∀ (h : i ≠ j),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) x : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) ∈ insert 0 s
Tactic: obtain rfl | h := eq_or_ne i j
-- 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
c1 c2 : NumDenSameDeg 𝒜 x
hdeg : c1.deg = c2.deg
hnum : (↑c1.num : A) = (↑c2.num : A)
hden : (↑c1.den : A) = (↑c2.den : A)
⊢ c1 = c2
have rcases : ∀ (i1 : ι) (n1 : A) (hn1 : n1 ∈ 𝒜 i1) (d1 : A) (hd1 : d1 ∈ 𝒜 i1)
  (h1 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1) : A) ∈ x)
  (hdeg :
    { 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 =
      c2.deg)
  (hnum :
    (↑{ 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 }.num :
        A) =
      (↑c2.num : A))
  (hden :
    (↑{ 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 }.den :
        A) =
      (↑c2.den : A)),
  { 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 } =
    c2
Tactic: rcases c1 with ⟨i1, ⟨n1, hn1⟩, ⟨d1, hd1⟩, h1⟩
Cleared hypotheses: c1, hdeg, hnum, hden
-- 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
c2 : NumDenSameDeg 𝒜 x
i1 : ι
n1 : A
hn1 : n1 ∈ 𝒜 i1
d1 : A
hd1 : d1 ∈ 𝒜 i1
h1 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i1) d1 hd1) : A) ∈ x
hdeg :
  { 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 =
    c2.deg
hnum :
  (↑{ 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 }.num :
      A) =
    (↑c2.num : A)
hden :
  (↑{ 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 }.den :
      A) =
    (↑c2.den : A)
⊢ { 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 } =
    c2
have rcases : ∀ (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 :
    { 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 =
      { 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 : NumDenSameDeg 𝒜 x }.deg)
  (hnum :
    (↑{ 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 }.num :
        A) =
      (↑{ 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 : NumDenSameDeg 𝒜 x }.num :
        A))
  (hden :
    (↑{ 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 }.den :
        A) =
      (↑{ 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 : NumDenSameDeg 𝒜 x }.den :
        A)),
  { 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: rcases c2 with ⟨i2, ⟨n2, hn2⟩, ⟨d2, hd2⟩, h2⟩
Cleared hypotheses: c2, hdeg, hnum, hden
-- 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
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
⊢ { 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 }
have 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 }
Tactic: subst hdeg hnum hden
Cleared hypotheses: i2, n2, hn2, d2, hd2, h2, hdeg, hnum, hden
-- 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
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
inst_5 : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
n : ℕ
⊢ (↑(@GradedMonoid.GMonoid.gnpow _ (fun (i : ι) ↦ ↥(𝒜 i)) AddCommMonoid.toAddMonoid _ n _ c.den : ↥(𝒜 (n • c.deg))) :
      A) ∈
    x
have zero : (↑(@GradedMonoid.GMonoid.gnpow _ (fun (i : ι) ↦ ↥(𝒜 i)) AddCommMonoid.toAddMonoid _ 0 _ c.den :
        ↥(𝒜 (HSMul.hSMul (α := ℕ) 0 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
Cleared hypotheses: n
-- 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
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
⊢ (↑(@GradedMonoid.GMonoid.gnpow _ (fun (i : ι) ↦ ↥(𝒜 i)) AddCommMonoid.toAddMonoid _ n _ c.den : ↥(𝒜 (n • c.deg))) :
      A) ∈
    x
have 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
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
Cleared hypotheses: n
-- 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) ⋯))
⊢ 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) ⋯))
have 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) sorry))
  (Localization.mk (m • (↑c2.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) sorry))
Tactic: simp only [num_smul, den_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
𝒜 : ι → σ
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 (α := 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) ⋯))
have h₁ : Localization.mk (m • (↑c1.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) sorry) =
  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) sorry))
Tactic: convert! congr_arg (fun z : at x => m • z) 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
𝒜 : ι → σ
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) ⋯))
⊢ 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) ⋯))
have h₂ : Localization.mk (m • (↑c2.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c2.den : A) sorry) =
  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) sorry))
Tactic: convert! congr_arg (fun z : at x => m • z) 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
𝒜 : ι → σ
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 • (↑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) ⋯))
have 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) sorry))
  (Localization.mk (m • (↑c1.num : A)) (Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ x) (↑c1.den : A) sorry))
Tactic: rw [Localization.smul_mk]