-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst : IsAffine T
t : ↥T
inst_1 : Flat f
inst_2 : IsFinite f
i : Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) ⟶ S :=
  S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl :
  Eq (α := ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    ((pullback.fst (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
        (u z) :
      ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    (Exists.choose (p :=
        fun
          (y :
            ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))) ↦
        Eq (α := ↥S)
          ((S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) y : ↥S)
          (g t : ↥S))
        ⋯ :
      ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
hyr :
  (pullback.snd (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
      (u z : ↥(pullback i g)) =
    t
refine_1 :
  pullback (X := pullback f g) (pullback.snd f g) (u ≫ pullback.snd i g) ⟶
    pullback (Y :=
      Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))) f
      (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))
refine_2 :
  Spec R ⟶ Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))
refine_3 :
  IsPullback (P := pullback (X := pullback f g) (pullback.snd f g) (u ≫ pullback.snd i g)) (X :=
    pullback (Y :=
      Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))) f
      (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))
    (pullback.map (pullback.snd f g) (u ≫ pullback.snd i g) f
      (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))
      (pullback.fst f g) (u ≫ pullback.fst i g) g ⋯ ⋯)
    (pullback.snd (pullback.snd f g) (u ≫ pullback.snd i g))
    (pullback.snd f (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))
    (u ≫ pullback.fst i g)
⊢ finrank f (g t) =
    IsAffine.finrank (X := pullback (X := pullback f g) (pullback.snd f g) (u ≫ pullback.snd i g))
      (pullback.snd (pullback.snd f g) (u ≫ pullback.snd i g)) z
have refine_4 : Eq (α := ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
  ((u ≫ pullback.fst i g) z :
    ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
  (Exists.choose (p :=
      fun
        (y :
          ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))) ↦
      Eq (α := ↥S)
        ((S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) y : ↥S)
        (g t : ↥S))
      sorry :
    ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
Tactic: refine (IsAffine.finrank_of_isPullback _ _ ?_ ?_ ?_ _ _ ?_).symm