-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
@[reassoc]
lemma awayMap_awayToSection  :
    CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x =
      awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE (basicOpen_mono _ _ _ ⟨_, hx⟩)).op

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
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 := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                        den_mem := ⋯ })
                    { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
              ⟨↑((fun x_1 =>
                        { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑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 := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                      den_mem := ⋯ })
                  { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
            ⟨↑((fun x_1 =>
                      { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                        den_mem := ⋯ })
                    { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
              ⋯⟩).1)

Tactic:
simp only [OneMemClass.coe_one, RingHom.id_apply, one_mul, hx]

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
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
⊢ f ^ i * (↑a * g ^ i) = (f * g) ^ i * ↑a

Proof state:
case hf.a.a.h.mk.a
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
a : ↑(CommRingCat.of (Away 𝒜 f))
i : ↑(ProjectiveSpectrum.top 𝒜)
hi : i ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
⊢ val (↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x)) a) ⟨i, hi⟩) =
    val (↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op)) a) ⟨i, hi⟩)

Tactic:
obtain ⟨⟨n, a, ⟨b, hb'⟩, i, rfl : _ = b⟩, rfl⟩ := mk_surjective a

Result:
case hf.a.a.h.mk.a.intro.mk.mk.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
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
⊢ val
      (↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x))
            (mk { deg := n, num := a, den := ⟨(fun x => f ^ x) i, hb'⟩, den_mem := ⋯ }))
        ⟨i✝, hi⟩) =
    val
      (↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op))
            (mk { deg := n, num := a, den := ⟨(fun x => f ^ x) i, hb'⟩, den_mem := ⋯ }))
        ⟨i✝, hi⟩)

Proof state:
case hf.a.a.h.mk.a.intro.mk.mk.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
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
⊢ (Localization.r (↑⟨i✝, hi⟩).asHomogeneousIdeal.toIdeal.primeCompl)
    ((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩)
    (↑((fun x_1 =>
              { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                den_mem := ⋯ })
            { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
      ⟨↑((fun x_1 =>
                { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                  den_mem := ⋯ })
              { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
        ⋯⟩)

Tactic:
rw [Localization.r_iff_exists]

Result:
case hf.a.a.h.mk.a.intro.mk.mk.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
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 := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                          den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
                ⟨↑((fun x_1 =>
                          { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑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 := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                        den_mem := ⋯ })
                    { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
              ⟨↑((fun x_1 =>
                        { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                          den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
                ⋯⟩).1)

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
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
⊢ f ^ i * (↑a * g ^ i) = (f * g) ^ i * ↑a

Tactic:
ring

Result:
no goals