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
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun (x : ℕ) ↦ f ^ x) n ∈ 𝒜 N
pos :
  ∀ (hfn : f ^ n = 0),
    ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
      Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
        (mk
          { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })
⊢ ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })
have neg : ∀ (hfn : ¬f ^ n = 0),
  ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := sorry })
Tactic: by_cases hfn : f ^ n = 0
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (hypothesis)
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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun (x : ℕ) ↦ f ^ x) n ∈ 𝒜 N
hfn : f ^ n = 0
⊢ ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })
have this : Subsingleton (HomogeneousLocalization 𝒜 (Submonoid.powers f))
Tactic: have := HomogeneousLocalization.subsingleton 𝒜 (x := .powers f) ⟨n, hfn⟩
-- 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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun (x : ℕ) ↦ f ^ x) n ∈ 𝒜 N
hfn : ¬f ^ n = 0
⊢ ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := N, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 N) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })
have neg : ∀ (hs : s ∈ 𝒜 (n • d)) (hn : (fun (x : ℕ) ↦ f ^ x) n ∈ 𝒜 (n • d)),
  ∃ (n_1 : ℕ) (a : A) (ha : a ∈ 𝒜 (n_1 • d)),
    Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n_1 a ha)
      (mk
        { deg := n • d, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) s hs,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := sorry })
Tactic: obtain rfl := DirectSum.degree_eq_of_mem_mem 𝒜 hn (SetLike.pow_mem_graded n hf) hfn
Cleared hypotheses: N, hs, hn
-- 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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
s : A
n : ℕ
hfn : ¬f ^ n = 0
hs : s ∈ 𝒜 (n • d)
hn : (fun (x : ℕ) ↦ f ^ x) n ∈ 𝒜 (n • d)
⊢ Eq (α := Away 𝒜 f) (Away.mk 𝒜 hf n s hs)
    (mk
      { deg := n • d, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) s hs,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := ⋯ })
have a : Eq (α := at Submonoid.powers f) (val (Away.mk 𝒜 hf n s hs))
  (val
    (mk
      { deg := n • d, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) s hs,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • d)) ((fun (x : ℕ) ↦ f ^ x) n) hn, den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) }))
Tactic: ext
-- 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 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
⊢ ∀ᶠ (n : ℕ) in Filter.atTop,
    Membership.mem (γ := Set (at Submonoid.powers f))
      ((⇑(algebraMap A (at Submonoid.powers f)) : (a : A) → at Submonoid.powers f) '' (↑(𝒜 (n • m)) : Set A))
      (f ^ n • val z)
have obtain : ∀ (k : ℕ) (hk : f ^ k = den z),
  ∀ᶠ (n : ℕ) in Filter.atTop,
    Membership.mem (γ := Set (at Submonoid.powers f))
      ((⇑(algebraMap A (at Submonoid.powers f)) : (a : A) → at Submonoid.powers f) '' (↑(𝒜 (n • m)) : Set A))
      (f ^ n • val z)
Tactic: obtain ⟨k, hk : f ^ k = _⟩ := z.den_mem
-- 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 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
⊢ ∀ᶠ (n : ℕ) in Filter.atTop,
    Membership.mem (γ := Set (at Submonoid.powers f))
      ((⇑(algebraMap A (at Submonoid.powers f)) : (a : A) → at Submonoid.powers f) '' (↑(𝒜 (n • m)) : Set A))
      (f ^ n • val z)
have apply : Set.Ici k ⊆
  {x : ℕ |
    (fun (n : ℕ) ↦
        Membership.mem (γ := Set (at Submonoid.powers f))
          ((⇑(algebraMap A (at Submonoid.powers f)) : (a : A) → at Submonoid.powers f) '' (↑(𝒜 (n • m)) : Set A))
          (f ^ n • val z))
      x}
Tactic: apply Filter.mem_of_superset (Filter.Ici_mem_atTop k)
-- 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 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z
have pos : ∀ (hfk : f ^ k = 0),
  ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z
Tactic: by_cases hfk : f ^ k = 0
-- 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 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
pos :
  ∀ (hfk : f ^ k = 0),
    ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z
have neg : ∀ (hfk : ¬f ^ k = 0),
  ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z
Tactic: by_cases hfk : f ^ k = 0
-- 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 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z
have pos : (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ k' • val z
Tactic: refine ⟨0, zero_mem _, ?_⟩
-- 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 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
⊢ (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ k' • val z
have pos : (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ (k' - k + k) • val z
Tactic: rw [← tsub_add_cancel_of_le hk', map_zero, pow_add, hfk, mul_zero, zero_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 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
pos : (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ (k' - k + k) • val z
⊢ (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ k' • val z
have pos₁ : 0 = f ^ (k' - k + k) • val z
Tactic: rw [← tsub_add_cancel_of_le hk', map_zero, pow_add, hfk, mul_zero, zero_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 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
pos : (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ (k' - k + k) • val z
pos₁ : 0 = f ^ (k' - k + k) • val z
⊢ (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ k' • val z
have pos₂ : 0 = (f ^ (k' - k) * f ^ k) • val z
Tactic: rw [← tsub_add_cancel_of_le hk', map_zero, pow_add, hfk, mul_zero, zero_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 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
pos : (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ (k' - k + k) • val z
pos₁ : 0 = f ^ (k' - k + k) • val z
pos₂ : 0 = (f ^ (k' - k) * f ^ k) • val z
⊢ (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ k' • val z
have pos₃ : 0 = (f ^ (k' - k) * 0) • val z
Tactic: rw [← tsub_add_cancel_of_le hk', map_zero, pow_add, hfk, mul_zero, zero_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 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
pos : (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ (k' - k + k) • val z
pos₁ : 0 = f ^ (k' - k + k) • val z
pos₂ : 0 = (f ^ (k' - k) * f ^ k) • val z
pos₃ : 0 = (f ^ (k' - k) * 0) • val z
⊢ (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ k' • val z
have pos₄ : 0 = HSMul.hSMul (α := A) 0 (val z)
Tactic: rw [← tsub_add_cancel_of_le hk', map_zero, pow_add, hfk, mul_zero, zero_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 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : f ^ k = 0
pos : (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ (k' - k + k) • val z
pos₁ : 0 = f ^ (k' - k + k) • val z
pos₂ : 0 = (f ^ (k' - k) * f ^ k) • val z
pos₃ : 0 = (f ^ (k' - k) * 0) • val z
pos₄ : 0 = HSMul.hSMul (α := A) 0 (val z)
⊢ (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) 0 = f ^ k' • val z
have pos₅ : Eq.{u_2 + 1} (α := at Submonoid.powers f) 0 0
Tactic: rw [← tsub_add_cancel_of_le hk', map_zero, pow_add, hfk, mul_zero, zero_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 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x = f ^ k' • val z
have neg : ∃ x ∈ 𝒜 ((k' - k + k) • m),
  Eq (α := at Submonoid.powers f)
    ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x : at Submonoid.powers f)
    ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) (f ^ (k' - k) * num z) :
      at Submonoid.powers f)
Tactic: rw [← tsub_add_cancel_of_le hk', pow_add, mul_smul, hk, den_smul_val,
    Algebra.smul_def, ← map_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 𝒜
f : A
m : ι
hf : f ∈ 𝒜 m
z : Away 𝒜 f
k : ℕ
hk : f ^ k = den z
k' : ℕ
hk' : k ≤ k'
hfk : ¬f ^ k = 0
⊢ ∃ x ∈ 𝒜 ((k' - k + k) • m),
    Eq (α := at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x : at Submonoid.powers f)
      ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) (f ^ (k' - k) * num z) :
        at Submonoid.powers f)
have neg : ∃ x ∈ 𝒜 ((k' - k) • m + deg z),
  Eq (α := at Submonoid.powers f)
    ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) x : at Submonoid.powers f)
    ((algebraMap A (at Submonoid.powers f) : (a : A) → at Submonoid.powers f) (f ^ (k' - k) • num z) :
      at Submonoid.powers f)
Tactic: rw [← smul_eq_mul, add_smul,
    DirectSum.degree_eq_of_mem_mem 𝒜 (SetLike.pow_mem_graded _ hf) (hk.symm ▸ z.den_mem_deg) hfk]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (hypothesis)
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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
e : embedding 𝒜 P x = embedding 𝒜 P y
⊢ (Setoid.ker (embedding ℬ Q) : NumDenSameDeg ℬ Q → NumDenSameDeg ℬ Q → Prop)
    ((fun (x : NumDenSameDeg 𝒜 P) ↦
        ({ deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ } :
          NumDenSameDeg ℬ Q))
      x)
    ((fun (x : NumDenSameDeg 𝒜 P) ↦
        ({ deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ } :
          NumDenSameDeg ℬ Q))
      y)
have e₁ : Eq.{u_4 + 1} (α := Localization (M := B) Q)
  (((IsLocalization.map (Localization (M := B) Q) (↑g : A →+* B) comap_le :
          RingHom.{u_2, u_4} (Localization (M := A) P) (Localization (M := B) Q)) :
        (a : at P) → at Q)
      (embedding 𝒜 P x) :
    Localization (M := B) Q)
  (((IsLocalization.map (Localization (M := B) Q) (↑g : A →+* B) comap_le :
          RingHom.{u_2, u_4} (Localization (M := A) P) (Localization (M := B) Q)) :
        (a : at P) → at Q)
      (embedding 𝒜 P y) :
    Localization (M := B) Q)
Tactic: apply_fun IsLocalization.map (Localization Q) g.toRingHom comap_le at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization (hypothesis)
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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
e :
  Eq.{u_4 + 1} (α := Localization (M := B) Q)
    (((IsLocalization.map (Localization (M := B) Q) (↑g : A →+* B) comap_le :
            RingHom.{u_2, u_4} (Localization (M := A) P) (Localization (M := B) Q)) :
          (a : at P) → at Q)
        (embedding 𝒜 P x) :
      Localization (M := B) Q)
    (((IsLocalization.map (Localization (M := B) Q) (↑g : A →+* B) comap_le :
            RingHom.{u_2, u_4} (Localization (M := A) P) (Localization (M := B) Q)) :
          (a : at P) → at Q)
        (embedding 𝒜 P y) :
      Localization (M := B) Q)
⊢ (Setoid.ker (embedding ℬ Q) : NumDenSameDeg ℬ Q → NumDenSameDeg ℬ Q → Prop)
    ((fun (x : NumDenSameDeg 𝒜 P) ↦
        ({ deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ } :
          NumDenSameDeg ℬ Q))
      x)
    ((fun (x : NumDenSameDeg 𝒜 P) ↦
        ({ deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ } :
          NumDenSameDeg ℬ Q))
      y)
have e₁ : Eq.{u_4 + 1} (α := Localization (M := B) Q)
  (Localization.mk (((↑g : A →+* B) : (a : A) → B) (↑x.num : A))
      (Subtype.mk (p := fun (x : B) ↦ x ∈ Q) (((↑g : A →+* B) : (a : A) → B) (↑x.den : A)) sorry) :
    Localization (M := B) Q)
  (Localization.mk (((↑g : A →+* B) : (a : A) → B) (↑y.num : A))
      (Subtype.mk (p := fun (x : B) ↦ x ∈ Q) (((↑g : A →+* B) : (a : A) → B) (↑y.den : A)) sorry) :
    Localization (M := B) Q)
Tactic: simp_rw [HomogeneousLocalization.NumDenSameDeg.embedding, Localization.mk_eq_mk',
        IsLocalization.map_mk', ← Localization.mk_eq_mk'] at e
Cleared hypotheses: e
-- 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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
⊢ Eq (α := HomogeneousLocalization ℬ Q)
    (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
      (fun (x : NumDenSameDeg 𝒜 P) ↦
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ })
      ⋯ 1)
    1
have simp : Eq (α := HomogeneousLocalization ℬ Q)
  (Quotient.mk''
    { deg := NumDenSameDeg.deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := P) 1,
      num := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ (NumDenSameDeg.deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := P) 1)) 1 sorry,
      den := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ (NumDenSameDeg.deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := P) 1)) 1 sorry,
      den_mem := sorry })
  1
Tactic: simp only [← mk_one (𝒜 := 𝒜), Quotient.map'_mk'',
    num_one, den_one, map_one]
-- 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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
⊢ Quotient.map'
      (fun (x : NumDenSameDeg 𝒜 P) ↦
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ })
      ⋯ (HMul.hMul (α := HomogeneousLocalization 𝒜 P) (Quotient.mk'' x) (Quotient.mk'' y)) =
    HMul.hMul (α := HomogeneousLocalization ℬ Q)
      (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
        (fun (x : NumDenSameDeg 𝒜 P) ↦
          { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
            NumDenSameDeg ℬ Q })
        ⋯ (Quotient.mk'' x))
      (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
        (fun (x : NumDenSameDeg 𝒜 P) ↦
          { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
            NumDenSameDeg ℬ Q })
        ⋯ (Quotient.mk'' y))
have simp : Quotient.mk''
    { deg := (x * y).deg,
      num :=
        Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x * y).deg)
          (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.num : A) : B) ((g : (a : A) → B) (↑y.num : A) : B)) sorry,
      den :=
        Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x * y).deg)
          (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.den : A) : B) ((g : (a : A) → B) (↑y.den : A) : B)) sorry,
      den_mem := sorry } =
  mk
    (HMul.hMul (α := NumDenSameDeg ℬ Q)
      { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) sorry,
        den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) sorry, den_mem := sorry :
        NumDenSameDeg ℬ Q }
      { deg := y.deg, num := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.num : A)) sorry,
        den := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.den : A)) sorry, den_mem := sorry :
        NumDenSameDeg ℬ Q })
Tactic: simp only [← mk_mul, Quotient.map'_mk'', num_mul, map_mul, den_mul]