Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x ↦ f ^ x) i ∈ 𝒜 n
⊢ ∃ c,
    ↑c *
        (↑(↑((fun x_1 ↦
                        { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                          den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
                ⟨↑((fun x_1 ↦
                          { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                            den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                        { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
                  ⋯⟩).2 *
          ((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).1) =
      ↑c *
        (↑((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).2 *
          (↑((fun x_1 ↦
                      { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                        den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                    { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
              ⟨↑((fun x_1 ↦
                        { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                          den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
                ⋯⟩).1)

Tactic:
use 1

Goal state after:
case h
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x ↦ f ^ x) i ∈ 𝒜 n
⊢ ↑1 *
      (↑(↑((fun x_1 ↦
                      { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                        den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                    { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
              ⟨↑((fun x_1 ↦
                        { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                          den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
                ⋯⟩).2 *
        ((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).1) =
    ↑1 *
      (↑((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).2 *
        (↑((fun x_1 ↦
                    { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                      den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                  { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
            ⟨↑((fun x_1 ↦
                      { deg := x_1.deg, num := ⟨(GradedRingHom.id 𝒜) ↑x_1.num, ⋯⟩,
                        den := ⟨(GradedRingHom.id 𝒜) ↑x_1.den, ⋯⟩, den_mem := ⋯ })
                    { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
              ⋯⟩).1)