Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case refine_1
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ pullback (pullback.snd f g) (u ≫ pullback.snd i g) ⟶ pullback f (S.affineOpenCover.f (S.affineOpenCover.idx (g t)))

pp: case refine_2
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ Spec R ⟶ Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t)))

pp: case refine_3
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ IsPullback ?refine_1 (pullback.snd (pullback.snd f g) (u ≫ pullback.snd i g))
    (pullback.snd f (S.affineOpenCover.f (S.affineOpenCover.idx (g t)))) ?refine_2

pp: case refine_4
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ ?refine_2 z = Exists.choose ⋯

Tactic:
· exact pullback.map _ _ _ _ (pullback.fst f g) (u ≫ pullback.fst _ _) g
        pullback.condition.symm (by simp [← pullback.condition]; rfl)

Goal state after:
case refine_2
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ Spec R ⟶ Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t)))

case refine_3
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ IsPullback
    (pullback.map (pullback.snd f g) (u ≫ pullback.snd i g) f (S.affineOpenCover.f (S.affineOpenCover.idx (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 (S.affineOpenCover.idx (g t)))) ?refine_2

case refine_4
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst✝² : IsAffine T
t : ↥T
inst✝¹ : Flat f
inst✝ : IsFinite f
i : Spec (S.affineOpenCover.X (S.affineOpenCover.idx (g t))) ⟶ S := S.affineOpenCover.f (S.affineOpenCover.idx (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl : (pullback.fst (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = Exists.choose ⋯
hyr : (pullback.snd (S.affineOpenCover.f (S.affineOpenCover.idx (g t))) g) (u z) = t
⊢ ?refine_2 z = Exists.choose ⋯