awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (X := pullback f g) (pullback.fst f g)
⊢ P g
have H₁ : ∀ (V : X.Opens) (hV : IsCompact V.carrier) (e : Eq (α := Set ↥(Spec R)) (⇑f '' (↑V : Set ↥X)) Set.univ), P g
Tactic: obtain ⟨V : X.Opens, hV, e⟩ := f.isOpenMap.exists_opens_image_eq_of_prespectralSpace
    f.continuous (by simp) isOpen_univ isCompact_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (X := pullback f g) (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : Eq (α := Set ↥(Spec R)) (⇑f '' (↑V : Set ↥X)) Set.univ
⊢ P g
have H₁ : Surjective (V.ι ≫ f)
Tactic: refine MorphismProperty.of_isPullback_of_descendsAlong (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact)
    (.paste_vert (.of_hasPullback V.ι _) (.of_hasPullback f g)) ⟨⟨?_, inferInstance⟩,
      (quasiCompact_iff_compactSpace _).mpr (isCompact_iff_compactSpace.mp hV)⟩ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (X := pullback f g) (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : Eq (α := Set ↥(Spec R)) (⇑f '' (↑V : Set ↥X)) Set.univ
H₁ : Surjective (V.ι ≫ f)
⊢ P g
have H₂ : P (X := pullback (Y := pullback f g) V.ι (pullback.fst f g)) (pullback.fst V.ι (pullback.fst f g))
Tactic: refine MorphismProperty.of_isPullback_of_descendsAlong (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact)
    (.paste_vert (.of_hasPullback V.ι _) (.of_hasPullback f g)) ⟨⟨?_, inferInstance⟩,
      (quasiCompact_iff_compactSpace _).mpr (isCompact_iff_compactSpace.mp hV)⟩ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
inst_3 : Mono f
⊢ IsIso f
have hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
Tactic: apply MorphismProperty.of_pullback_fst_of_descendsAlong
    (P := isomorphisms Scheme.{u}) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f) (g := f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
inst_3 : Mono f
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
⊢ IsIso f
have hfst : isomorphisms Scheme (X := pullback f f) (pullback.fst f f)
Tactic: apply MorphismProperty.of_pullback_fst_of_descendsAlong
    (P := isomorphisms Scheme.{u}) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f) (g := f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
⊢ IsOpenImmersion f
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
      IsOpenImmersion f)
  (hf : ¬Surjective f), IsOpenImmersion f
Tactic: wlog hf : Surjective f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
        IsOpenImmersion f)
    (hf : ¬Surjective f), IsOpenImmersion f
⊢ IsOpenImmersion f
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
  IsOpenImmersion f
Tactic: wlog hf : Surjective f
Cleared hypotheses: X, Y, f, inst, inst_1, inst_2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
⊢ IsOpenImmersion f
have hU : IsOpenImmersion U.ι
Tactic: have hU : IsOpenImmersion U.ι := U.instIsOpenImmersionι
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
⊢ IsOpenImmersion f
have heq : f = f' ≫ U.ι
Tactic: have heq : f = f' ≫ U.ι := by simp [f']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
⊢ IsOpenImmersion f
have hflat : Flat f'
Tactic: have hflat : Flat f' :=
      of_postcomp (W := @Flat) f' U.ι hU (by rwa [← heq])
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
⊢ IsOpenImmersion f
have hfinpres : LocallyOfFinitePresentation f'
Tactic: have hfinpres : LocallyOfFinitePresentation f' :=
      of_postcomp (W := @LocallyOfFinitePresentation) f' U.ι hU (by rwa [← heq])
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
⊢ IsOpenImmersion f
have hmono : Mono f'
Tactic: have hmono : Mono f' := mono_of_mono_fac heq.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
⊢ IsOpenImmersion f
have inr : IsOpenImmersion (f' ≫ U.ι)
Tactic: rw [heq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
x_1 : ↥(↑U : Scheme)
x : ↥Y
y : ↥X
hy : f y = x
⊢ Eq (α := ↥(↑U : Scheme)) (f' y : ↥(↑U : Scheme)) (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) x ⋯ : ↥U)
have a : Eq (α := ↥Y) (U.ι (f' y : ↥(↑U : Scheme)) : ↥Y) (U.ι (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) x sorry) : ↥Y)
Tactic: apply U.ι.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
⊢ IsOpenImmersion (f' ≫ U.ι)
have this₁ : IsOpenImmersion f'
Tactic: have := this f' ⟨fun ⟨x, ⟨y, hy⟩⟩ ↦
      ⟨y, by apply U.ι.injective; simp [← Scheme.Hom.comp_apply, f', hy]⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
hf : Surjective f
⊢ IsOpenImmersion f
have hhomeo : IsHomeomorph (X := ↥X) (Y := ↥Y) ⇑f
Tactic: have hhomeo : IsHomeomorph f.base := ⟨f.continuous, f.isOpenMap, f.injective, f.surjective⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
hf : Surjective f
hhomeo : IsHomeomorph (X := ↥X) (Y := ↥Y) ⇑f
⊢ IsOpenImmersion f
have this : QuasiCompact f
Tactic: have : QuasiCompact f := ⟨fun U hU hc ↦ hhomeo.homeomorph.isCompact_preimage.mpr hc⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatMono (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
hf : Surjective f
hhomeo : IsHomeomorph (X := ↥X) (Y := ↥Y) ⇑f
this : QuasiCompact f
⊢ IsOpenImmersion f
have this₁ : IsIso f
Tactic: have := Flat.isIso_of_surjective_of_mono f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
s : ↥S
t : ↥T
hs : g t = s
⊢ finrank f' t = finrank f s
have subst : finrank f' t = finrank f (g t)
Tactic: subst hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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
⊢ finrank f' t = finrank f (g t)
have this : IsAffine X
Tactic: have : IsAffine X := isAffine_of_isAffineHom f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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 : IsAffine X
⊢ finrank f' t = finrank f (g t)
have this₁ : IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop g') (Scheme.Hom.appTop f')
Tactic: have : IsPushout f.appTop g.appTop g'.appTop f'.appTop := isPushout_appTop_of_isPullback h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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 (T.isoSpec.hom t) =
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank (S.isoSpec.hom (g t))
have 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)
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ finrank (f ≫ g) = finrank g
have h : ∀ (z : ↥S), finrank (f ≫ g) z = finrank g z
Tactic: ext z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ finrank (f ≫ g) z = finrank g z
have apply : IsPullback f (f ≫ g) g (𝟙 S)
Tactic: apply finrank_of_isPullback g (f ≫ g) f (𝟙 _) _ _ _ rfl
-- 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))
⊢ finrank f (g t) = IsAffine.finrank (X := pullback f g) (pullback.snd f g) t
have 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))
          sorry :
        ↥(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
Tactic: obtain ⟨y, hyl, hyr⟩ := Scheme.Pullback.exists_preimage_pullback
    (S.affineOpenCover.covers <| g t).choose t (S.affineOpenCover.covers <| g t).choose_spec
-- 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))
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
have 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))
          sorry :
        ↥(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
Tactic: obtain ⟨R, u, hu, z, rfl⟩ := (pullback i g).exists_Spec_apply_eq y
Cleared hypotheses: y, hyl, hyr
-- 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
⊢ finrank f (g t) = IsAffine.finrank (X := pullback f g) (pullback.snd f g) t
have 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
Tactic: trans IsAffine.finrank (pullback.snd (pullback.snd f g) (u ≫ pullback.snd _ _)) z
-- 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
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
⊢ finrank f (g t) = IsAffine.finrank (X := pullback f g) (pullback.snd f g) t
have 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
Tactic: trans IsAffine.finrank (pullback.snd (pullback.snd f g) (u ≫ pullback.snd _ _)) z
-- 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
⊢ 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_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)))
Tactic: refine (IsAffine.finrank_of_isPullback _ _ ?_ ?_ ?_ _ _ ?_).symm