awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S Y T : Scheme
f : X ⟶ S
inst : IsAffine S
inst_1 : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst_2 : Flat f
inst_3 : IsFinite f
t : ↥T
this_1 : IsAffine X
this : IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop g') (Scheme.Hom.appTop f')
rw :
  (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank
      (PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appTop g)) (T.isoSpec.hom t)) =
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank ((T.isoSpec.hom ≫ Spec.map (Scheme.Hom.appTop g)) t)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f')).finrank (T.isoSpec.hom t) =
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank (S.isoSpec.hom (g t))

Tactic:
rw [CommRingCat.finrank_eq_of_isPushout this f.flat_appTop f.finite_appTop (T.isoSpec.hom t),
    ← Scheme.Hom.comp_apply, ← Scheme.isoSpec_hom_naturality]

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.isoSpec_hom_naturality, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.comp_apply, CommRingCat.finrank_eq_of_isPushout, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Hom.flat_appTop, AlgebraicGeometry.Scheme.Hom.finite_appTop, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S Y T : Scheme
f : X ⟶ S
inst : IsAffine S
inst_1 : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst_2 : Flat f
inst_3 : IsFinite f
t : ↥T
this_1 : IsAffine X
this : IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop g') (Scheme.Hom.appTop f')
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank
      (PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appTop g)) (T.isoSpec.hom t)) =
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank ((T.isoSpec.hom ≫ Spec.map (Scheme.Hom.appTop g)) t)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S T : Scheme
f : X ⟶ S
inst : IsAffine S
inst_1 : IsAffine T
g : T ⟶ S
inst_2 : Flat f
inst_3 : IsFinite f
x : ↥T
⊢ finrank (X := pullback f g) (pullback.snd f g) x = finrank f (g x)

Tactic:
finrank_of_isPullback f _ _ _ (.of_hasPullback _ _) _ _ rfl

Premises used: _private.0.AlgebraicGeometry.IsAffine.finrank_of_isPullback, CategoryTheory.IsPullback.of_hasPullback, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S Y : Scheme
inst : IsAffine S
f : X ⟶ Y
g : Y ⟶ S
inst_1 : IsIso f
inst_2 : IsFinite g
inst_3 : Flat g
h : ∀ (z : ↥S), finrank (f ≫ g) z = finrank g z
⊢ finrank (f ≫ g) = finrank g

Tactic:
ext z
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S Y : Scheme
inst : IsAffine S
f : X ⟶ Y
g : Y ⟶ S
inst_1 : IsIso f
inst_2 : IsFinite g
inst_3 : Flat g
z : ↥S
apply : IsPullback f (f ≫ g) g (𝟙 S)
⊢ finrank (f ≫ g) z = finrank g z

Tactic:
apply finrank_of_isPullback g (f ≫ g) f (𝟙 _) _ _ _ rfl

Premises used: CategoryTheory.CategoryStruct.id, _private.0.AlgebraicGeometry.IsAffine.finrank_of_isPullback, CategoryTheory.CategoryStruct.comp, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S Y : Scheme
inst : IsAffine S
f : X ⟶ Y
g : Y ⟶ S
inst_1 : IsIso f
inst_2 : IsFinite g
inst_3 : Flat g
z : ↥S
⊢ CommSq f (f ≫ g) g (𝟙 S)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S Y : Scheme
inst : IsAffine S
f : X ⟶ Y
g : Y ⟶ S
inst_1 : IsIso f
inst_2 : IsFinite g
inst_3 : Flat g
z : ↥S
⊢ IsPullback f (f ≫ g) g (𝟙 S)

Tactic:
exact IsPullback.of_horiz_isIso (by simp)

Premises used: CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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))
obtain :
  ∀
    (y :
      ↥(pullback (X :=
          Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))
          (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g))
    (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)
            y :
          ↥(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)
          y =
        t),
    finrank f (g t) = IsAffine.finrank (X := pullback f g) (pullback.snd f g) t
⊢ finrank f (g t) = IsAffine.finrank (X := pullback f g) (pullback.snd f g) t

Tactic:
obtain ⟨y, hyl, hyr⟩ := Scheme.Pullback.exists_preimage_pullback
    (S.affineOpenCover.covers <| g t).choose t (S.affineOpenCover.covers <| g t).choose_spec

Premises used: Exists.choose_spec, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.AffineCover.covers, AlgebraicGeometry.Scheme.affineOpenCover, AlgebraicGeometry.PresheafedSpace.Hom.base, Exists.choose, DFunLike.coe, AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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))
y :
  ↥(pullback (X :=
      Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))
      (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
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)
        y :
      ↥(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) y =
    t
obtain :
  ∀ (R : CommRingCat.{u}) (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),
    finrank f (g t) = IsAffine.finrank (X := pullback f g) (pullback.snd f g) t
⊢ finrank f (g t) = IsAffine.finrank (X := pullback f g) (pullback.snd f g) t

Tactic:
obtain ⟨R, u, hu, z, rfl⟩ := (pullback i g).exists_Spec_apply_eq y

Premises used: AlgebraicGeometry.Scheme.exists_Spec_apply_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
trans :
  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
trans₁ :
  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 =
    IsAffine.finrank (X := pullback f g) (pullback.snd f g) t
⊢ finrank f (g t) = IsAffine.finrank (X := pullback f g) (pullback.snd f g) t

Tactic:
trans IsAffine.finrank (pullback.snd (pullback.snd f g) (u ≫ pullback.snd _ _)) z

Premises used: CategoryTheory.Limits.pullback.snd, _private.0.AlgebraicGeometry.IsAffine.finrank, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ 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

Tactic:
(IsAffine.finrank_of_isPullback _ _ ?_ ?_ ?_ _ _ ?_).symm

Premises used: AlgebraicGeometry.Scheme.Hom.finrank, _private.0.AlgebraicGeometry.IsAffine.finrank_of_isPullback, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
simp :
  u ≫ pullback.fst i g ≫ i =
    u ≫
      pullback.fst i g ≫
        S.affineCover.f
          (Exists.choose (p := fun (i : S.affineCover.I₀) ↦
            ∃ (y : ↥(S.affineCover.X i)), Eq (α := ↥S) ((S.affineCover.f i) y : ↥S) (g t : ↥S)) ⋯)
⊢ (u ≫ pullback.snd i g) ≫ g =
    (u ≫ pullback.fst i g) ≫
      S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))

Tactic:
simp [← pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ u ≫ pullback.fst i g ≫ i =
    u ≫
      pullback.fst i g ≫
        S.affineCover.f
          (Exists.choose (p := fun (i : S.affineCover.I₀) ↦
            ∃ (y : ↥(S.affineCover.X i)), Eq (α := ↥S) ((S.affineCover.f i) y : ↥S) (g t : ↥S)) ⋯)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ 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)))

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

Premises used: CategoryTheory.Limits.pullback.map, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.pullback.condition, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ Spec R ⟶ Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))

Tactic:
exact u ≫ pullback.fst _ _

Premises used: CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ 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)

Tactic:
apply IsPullback.map_fst_comp_fst_snd_comp_fst

Premises used: CategoryTheory.IsPullback.map_fst_comp_fst_snd_comp_fst