Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case h
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) :=
  fun f hf ↦
    Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f)) ≪≫
      Functor.mapIso M.presheaf (eqToIso ⋯).op
f : ↑R
hf : basicOpen f ≤ basicOpen g
s : ↑Γ(M, basicOpen f)
n : ℕ
t : ↑Γ(M', ⊤)
ht :
  (ConcreteCategory.hom (M'.presheaf.map (homOfLE ⋯).op)) t =
    (ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom (e f hf).inv) s
this :
  (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯)))
      ((AddCommGrpCat.Hom.hom (M.presheaf.map (homOfLE ⋯).op))
        ((AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).hom) t)) =
    (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯)))
      (f ^ n •
        (ConcreteCategory.hom
            (Scheme.Modules.restrictAppIso (Spec.map a) M (basicOpen ((ConcreteCategory.hom a) f))).hom)
          ((AddCommGrpCat.Hom.hom
              (Scheme.Modules.restrictAppIso (Spec.map a) M (basicOpen ((ConcreteCategory.hom a) f))).inv)
            ((AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯))) s)))
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op))
      ((ConcreteCategory.hom ((Scheme.Modules.restrictAppIso ψ M ⊤).hom ≫ M.presheaf.map (eqToHom ⋯))) t) =
    f ^ n • s

Tactic:
simpa using

Goal state after:
case h
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
e : (f : ↑R) → basicOpen f ≤ basicOpen g → (Γ(M', basicOpen ((ConcreteCategory.hom a) f)) ≅ Γ(M, basicOpen f)) :=
  fun f hf ↦
    Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f)) ≪≫
      Functor.mapIso M.presheaf (eqToIso ⋯).op
f : ↑R
hf : basicOpen f ≤ basicOpen g
s : ↑Γ(M, basicOpen f)
n : ℕ
t : ↑Γ(M', ⊤)
ht :
  (ConcreteCategory.hom (M'.presheaf.map (homOfLE ⋯).op)) t =
    (ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom (e f hf).inv) s
this :
  (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯)))
      ((AddCommGrpCat.Hom.hom (M.presheaf.map (homOfLE ⋯).op))
        ((AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso (Spec.map a) M ⊤).hom) t)) =
    (AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯)))
      (f ^ n •
        (ConcreteCategory.hom
            (Scheme.Modules.restrictAppIso (Spec.map a) M (basicOpen ((ConcreteCategory.hom a) f))).hom)
          ((AddCommGrpCat.Hom.hom
              (Scheme.Modules.restrictAppIso (Spec.map a) M (basicOpen ((ConcreteCategory.hom a) f))).inv)
            ((AddCommGrpCat.Hom.hom (M.presheaf.map (eqToHom ⋯))) s)))
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op))
      ((AddCommGrpCat.Hom.hom (Scheme.Modules.restrictAppIso ψ M ⊤).hom) t) =
    f ^ n • s