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 :
  (ConcreteCategory.hom ((M.restrict ψ).presheaf.map (homOfLE ⋯).op ≫ (e f hf).hom)) t =
    (ConcreteCategory.hom (e f hf).hom) ((ConcreteCategory.hom a) f ^ n • (ConcreteCategory.hom (e f hf).inv) s)
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) ((ConcreteCategory.hom iso.hom) t) = f ^ n • s

Tactic:
simp only [homOfLE_leOfHom, Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, eqToIso.hom,
      eqToHom_op, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, eqToIso.inv, e, iso] at this ⊢

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 :
  (ConcreteCategory.hom
        ((M.restrict ψ).presheaf.map (homOfLE ⋯).op ≫
          (Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f))).hom ≫
            M.presheaf.map (eqToHom ⋯)))
      t =
    (ConcreteCategory.hom
        ((Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f))).hom ≫ M.presheaf.map (eqToHom ⋯)))
      ((ConcreteCategory.hom a) f ^ n •
        (ConcreteCategory.hom
            (M.presheaf.map (eqToHom ⋯) ≫
              (Scheme.Modules.restrictAppIso ψ M (basicOpen ((ConcreteCategory.hom a) f))).inv))
          s)
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op))
      ((ConcreteCategory.hom ((Scheme.Modules.restrictAppIso ψ M ⊤).hom ≫ M.presheaf.map (eqToHom ⋯))) t) =
    f ^ n • s