-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst : IsIso f
inst_1 : Flat g
inst_2 : IsFinite g
z : ↥S
e : pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
    (f ≫ g) (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) ≅
  pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z))) g
    (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) :=
  Iso.trans (Y :=
    pullback (Y :=
      pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
        g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
      f (pullback.fst g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z))))
    (Iso.symm
      (pullbackRightPullbackFstIso g
        (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) f))
    (asIso
      (pullback.snd f
        (pullback.fst g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))))
this :
  e.hom ≫ pullback.snd g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) =
    pullback.snd (f ≫ g) (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z))
h :
  IsAffine.finrank (X :=
      pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
        (f ≫ g) (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
      (pullback.snd (f ≫ g)
        (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
      (Exists.choose (p :=
        fun
          (y : ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))) ↦
        (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) y = z) ⋯) =
    finrank g z
h₁ :
  IsAffine.finrank (X :=
      pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
        (f ≫ g) (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
      (pullback.snd (f ≫ g)
        (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
      (Exists.choose (p :=
        fun
          (y : ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))) ↦
        (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) y = z) ⋯) =
    IsAffine.finrank (X :=
      pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
        g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
      (pullback.snd g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
      (Exists.choose (p :=
        fun
          (y : ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))) ↦
        (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) y = z) ⋯)
⊢ finrank (f ≫ g) z = finrank g z
have h₂ : IsAffine.finrank
    (e.hom ≫
      pullback.snd g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
    (Exists.choose (p :=
      fun (y : ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))) ↦
      (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) y = z) sorry) =
  IsAffine.finrank (X :=
    pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z))) g
      (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
    (pullback.snd g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
    (Exists.choose (p :=
      fun (y : ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))) ↦
      (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) y = z) sorry)
Tactic: rw [finrank, finrank, ← this, IsAffine.finrank_comp_left_of_isIso]