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

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.snd (𝒰.affineRefinement.openCover.map i) f =
    pullback.fst (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd) ≫ pullback.snd (𝒰.map i.fst) f

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

Result:
case h.e'_2.h.h.e'_7
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) ⟶ X) =
    (pullback (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd) ⟶ X)
⊢ (pullbackRightPullbackFstIso (𝒰.map i.fst) f ((𝒰.obj i.fst).affineCover.map i.snd)).hom ≫
      pullback.snd (𝒰.affineRefinement.openCover.map i) f =
    pullback.snd ((𝒰.obj i.fst).affineCover.map i.snd) (pullback.fst (𝒰.map i.fst) f) ≫ pullback.snd (𝒰.map i.fst) f

Proof state:
case h.e'_2.h.h.e'_7
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) ⟶ X) =
    (pullback (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd) ⟶ X)
⊢ (pullbackRightPullbackFstIso (𝒰.map i.fst) f ((𝒰.obj i.fst).affineCover.map i.snd)).hom ≫
      pullback.snd (𝒰.affineRefinement.openCover.map i) f =
    pullback.snd ((𝒰.obj i.fst).affineCover.map i.snd) (pullback.fst (𝒰.map i.fst) f) ≫ pullback.snd (𝒰.map i.fst) f

Tactic:
exact pullbackRightPullbackFstIso_hom_snd _ _ _

Result:
no goals

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

Tactic:
simp only [Cover.pullbackCover_obj, AffineCover.cover_obj, AffineCover.cover_map,
  pullbackCoverAffineRefinementObjIso, Iso.trans_inv, asIso_inv, Iso.symm_inv, Category.assoc,
  Cover.pullbackCover_map, pullbackSymmetry_inv_comp_fst, IsIso.inv_comp_eq, limit.lift_π_assoc,
  id_eq, PullbackCone.mk_pt, cospan_left, PullbackCone.mk_π_app, pullbackSymmetry_hom_comp_fst]

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.snd (𝒰.affineRefinement.openCover.map i) f =
    pullback.fst (pullback.fst (𝒰.map i.fst) f) ((𝒰.obj i.fst).affineCover.map i.snd) ≫ pullback.snd (𝒰.map i.fst) f