-- Mathlib/AlgebraicGeometry/Cover/Open.lean
@[reassoc]
lemma OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom
    (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i) :
    (𝒰.pullbackCoverAffineRefinementObjIso f i).inv ≫
      𝒰.affineRefinement.openCover.pullbackHom f i =
      (𝒰.obj i.1).affineCover.pullbackHom (𝒰.pullbackHom f i.1) i.2

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Cover.pullbackCover 𝒰.affineRefinement.openCover f).J
⊢ (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ≫ Cover.pullbackHom 𝒰.affineRefinement.openCover f i =
    Cover.pullbackHom (𝒰.obj i.fst).affineCover (Cover.pullbackHom 𝒰 f i.fst) i.snd

Tactic:
simp only [Cover.pullbackCover_obj, Cover.pullbackHom, AffineCover.cover_obj,
  AffineOpenCover.openCover_map, pullbackCoverAffineRefinementObjIso, Iso.trans_inv, asIso_inv,
  Iso.symm_inv, Category.assoc, pullbackSymmetry_inv_comp_snd, IsIso.inv_comp_eq, limit.lift_π,
  id_eq, PullbackCone.mk_pt, PullbackCone.mk_π_app, Category.comp_id]

Result:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Cover.pullbackCover 𝒰.affineRefinement.openCover f).J
⊢ (pullbackSymmetry ((𝒰.obj i.fst).affineCover.map i.snd) (pullback.fst (𝒰.map i.fst) f)).inv ≫
      (pullbackRightPullbackFstIso (𝒰.map i.fst) f ((𝒰.obj i.fst).affineCover.map i.snd)).hom ≫
        pullback.fst (𝒰.affineRefinement.map i) f =
    pullback.snd (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd)

Proof state:
case h.e'_2.h.h.e'_7.h
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Cover.pullbackCover 𝒰.affineRefinement.openCover f).J
e_1✝ :
  (pullback (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd) ⟶ 𝒰.affineRefinement.openCover.obj i) =
    (pullback (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd) ⟶
      (𝒰.obj i.fst).affineCover.obj i.snd)
e_5✝ : 𝒰.affineRefinement.openCover.obj i = (𝒰.obj i.fst).affineCover.obj i.snd
⊢ (pullbackRightPullbackFstIso (𝒰.map i.fst) f ((𝒰.obj i.fst).affineCover.map i.snd)).hom ≫
      pullback.fst (𝒰.affineRefinement.map i) f =
    pullback.fst ((𝒰.obj i.fst).affineCover.map i.snd) (pullback.fst (𝒰.map i.fst) f)

Tactic:
exact pullbackRightPullbackFstIso_hom_fst _ _ _

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Cover.pullbackCover 𝒰.affineRefinement.openCover f).J
⊢ (pullbackSymmetry ((𝒰.obj i.fst).affineCover.map i.snd) (pullback.fst (𝒰.map i.fst) f)).inv ≫
      (pullbackRightPullbackFstIso (𝒰.map i.fst) f ((𝒰.obj i.fst).affineCover.map i.snd)).hom ≫
        pullback.fst (𝒰.affineRefinement.map i) f =
    pullback.snd (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd)

Tactic:
convert pullbackSymmetry_inv_comp_fst ((𝒰.obj i.1).affineCover.map i.2) (pullback.fst _ _)

Result:
case h.e'_2.h.h.e'_7.h
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Cover.pullbackCover 𝒰.affineRefinement.openCover f).J
e_1✝ :
  (pullback (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd) ⟶ 𝒰.affineRefinement.openCover.obj i) =
    (pullback (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd) ⟶
      (𝒰.obj i.fst).affineCover.obj i.snd)
e_5✝ : 𝒰.affineRefinement.openCover.obj i = (𝒰.obj i.fst).affineCover.obj i.snd
⊢ (pullbackRightPullbackFstIso (𝒰.map i.fst) f ((𝒰.obj i.fst).affineCover.map i.snd)).hom ≫
      pullback.fst (𝒰.affineRefinement.map i) f =
    pullback.fst ((𝒰.obj i.fst).affineCover.map i.snd) (pullback.fst (𝒰.map i.fst) f)