awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Etale (goal)
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑((𝒰.X i).residueField y) : Type u) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst_1 : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑(CommRingCat.of Ω) : Type u) :=
  (CommRingCat.Hom.hom a).toAlgebra
b : (↑((𝒰.X i).residueField y) : Type u) →ₐ[(↑(S.residueField ((𝒰.f i) y)) : Type u)] Ω := IsSepClosed.lift
⊢ Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom = a
have hf : CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom) = CommRingCat.Hom.hom a
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Etale (hypothesis)
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑((𝒰.X i).residueField y) : Type u) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst_1 : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑(CommRingCat.of Ω) : Type u) :=
  (CommRingCat.Hom.hom a).toAlgebra
b : (↑((𝒰.X i).residueField y) : Type u) →ₐ[(↑(S.residueField ((𝒰.f i) y)) : Type u)] Ω := IsSepClosed.lift
⊢ ∃ (y_1 : Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) (𝒰.X i)),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) (𝒰.f i)) :
            (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj (𝒰.X i))) →
              (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
          y_1 :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((Equiv.symm (SpecToEquivOfField Ω S) :
            (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
          (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) ((𝒰.f i) y) a :
            (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) :
        Spec (CommRingCat.of Ω) ⟶ S)
have hfac : Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom = a
Tactic: have hfac : (𝒰.f i).residueFieldMap y ≫ CommRingCat.ofHom b.toRingHom = a := by
      ext1; exact b.comp_algebraMap
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Etale (goal)
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑((𝒰.X i).residueField y) : Type u) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst_1 : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑(CommRingCat.of Ω) : Type u) :=
  (CommRingCat.Hom.hom a).toAlgebra
b : (↑((𝒰.X i).residueField y) : Type u) →ₐ[(↑(S.residueField ((𝒰.f i) y)) : Type u)] Ω := IsSepClosed.lift
hfac : Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom = a
⊢ ∃ (y_1 : Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) (𝒰.X i)),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) (𝒰.f i)) :
            (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj (𝒰.X i))) →
              (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
          y_1 :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((Equiv.symm (SpecToEquivOfField Ω S) :
            (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
          (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) ((𝒰.f i) y) a :
            (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) :
        Spec (CommRingCat.of Ω) ⟶ S)
have h : Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) (𝒰.f i)) :
        (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj (𝒰.X i))) →
          (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
      (Spec.map (CommRingCat.ofHom b.toRingHom) ≫ (𝒰.X i).fromSpecResidueField y) :
    (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
  ((Equiv.symm (SpecToEquivOfField Ω S) :
        (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
      (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) ((𝒰.f i) y) a :
        (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) :
    Spec (CommRingCat.of Ω) ⟶ S)
Tactic: use Spec.map (CommRingCat.ofHom b.toRingHom) ≫ (𝒰.X i).fromSpecResidueField y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Fpqc (goal)
Goal:
⊢ fppfPrecoverage ≤ fpqcPrecoverage
have rw : fppfPrecoverage ≤ qcPrecoverage ∧ fppfPrecoverage ≤ precoverage @Flat
Tactic: rw [fpqcPrecoverage, propQCPrecoverage, le_inf_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Fpqc (goal)
Goal:
⊢ fppfPrecoverage ≤ qcPrecoverage ∧ fppfPrecoverage ≤ precoverage @Flat
have refine : fppfPrecoverage ≤ qcPrecoverage
Tactic: refine ⟨?_, precoverage_mono fun X Y f ⟨hf, _⟩ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Fpqc (goal)
Goal:
⊢ fpqcTopology.Subcanonical
have refine : ∀ (X : Scheme.{u_1}), Presieve.IsSheaf fpqcTopology (Functor.obj yoneda X)
Tactic: refine GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ fun X ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Fpqc (goal)
Goal:
X : Scheme
⊢ Presieve.IsSheaf fpqcTopology (Functor.obj yoneda X)
have rw : Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X) ∧
  ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
    Flat (Spec.map f) →
      Surjective (Spec.map f) → Presieve.IsSheafFor (Functor.obj yoneda X) (Presieve.singleton (Spec.map f))
Tactic: rw [fpqcTopology_eq_propQCTopology, isSheaf_type_propQCTopology_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Fpqc (goal)
Goal:
X : Scheme
⊢ Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X) ∧
    ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (Functor.obj yoneda X) (Presieve.singleton (Spec.map f))
have refine_1 : Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Fpqc (goal)
Goal:
X : Scheme
refine_1 : Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X)
⊢ Presieve.IsSheaf zariskiTopology (Functor.obj yoneda X) ∧
    ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
      Flat (Spec.map f) →
        Surjective (Spec.map f) → Presieve.IsSheafFor (Functor.obj yoneda X) (Presieve.singleton (Spec.map f))
have refine_2 : ∀ {R S : CommRingCat.{u_1}} (f : R ⟶ S),
  Flat (Spec.map f) →
    Surjective (Spec.map f) → Presieve.IsSheafFor (Functor.obj yoneda X) (Presieve.singleton (Spec.map f))
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Fpqc (hypothesis)
Goal:
X : Scheme
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
⊢ Presieve.IsSheafFor (Functor.obj yoneda X) (Presieve.singleton (Spec.map f))
have this : IsRegularEpi (Spec.map f)
Tactic: have : IsRegularEpi (Spec.map f) :=
      isRegularEpi_of_flat_of_surjective_of_isAffine _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Fpqc (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
inst_2 : LocallyOfFinitePresentation f
⊢ Presieve.singleton f ∈ fppfPrecoverage.coverings Y
have rw : (Presieve.ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ f) ∈ fppfPrecoverage.coverings Y
Tactic: rw [← Presieve.ofArrows_pUnit.{_, _, 0}]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Fpqc (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : Surjective f
inst_2 : Flat f
⊢ EffectiveEpi f
have rw : ∀ (Y_1 : Scheme.{u_1}), Presieve.IsSheafFor (Functor.obj yoneda Y_1) (Presieve.singleton f)
Tactic: rw [← Sieve.effectiveEpimorphic_singleton,
    Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Fpqc (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Surjective f
inst_2 : Flat f
⊢ EffectiveEpi f
have rw : ∀ (Y_1 : Scheme.{u_1}), Presieve.IsSheafFor (Functor.obj yoneda Y_1) (Presieve.singleton f)
Tactic: rw [← Sieve.effectiveEpimorphic_singleton,
    Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (hypothesis)
Goal:
P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
⊢ ∃ (a : ↥(pullback f g)), (pullback.snd f g) a = y
have this : HasPullback g f
Tactic: haveI : HasPullback g f := hasPullback_symmetry f g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
⊢ ∃ (a : ↥(pullback f g)), (pullback.snd f g) a = y
have obtain : ∀ (a : ↥(pullback g f)) (ha : (pullback.fst g f) a = y), ∃ (a : ↥(pullback f g)), (pullback.snd f g) a = y
Tactic: obtain ⟨a, ha⟩ := exists_preimage_fst_triplet_of_prop hf y x h.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
⊢ ∃ (a : ↥(pullback f g)), (pullback.snd f g) a = y
have h₁ : (pullback.snd f g) ((Iso.inv (pullbackSymmetry f g)) a : ↥(pullback f g)) = y
Tactic: use (pullbackSymmetry f g).inv a
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P : MorphismProperty Scheme
inst : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
⊢ (pullback.snd f g) ((Iso.inv (pullbackSymmetry f g)) a : ↥(pullback f g)) = y
have h₁ : (CategoryStruct.comp (Y := pullback f g) (Iso.inv (pullbackSymmetry f g)) (pullback.snd f g)) a = y
Tactic: rwa [← Scheme.Hom.comp_apply, pullbackSymmetry_inv_comp_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
⊢ ∃ (a : ↥(pullback f g)), (pullback.fst f g) a = x
have rw : ∃ (a : ↥(pullback f g)),
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := (↑(pullback f g).toPresheafedSpace : TopCat))
          (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
            (Iso.hom (PreservesPullback.iso forgetToTop f g)) (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
        (a : ↥(pullback f g)) → ↥X)
      a =
    x
Tactic: rw [← show _ = (pullback.fst _ _ : pullback f g ⟶ _).base from
        PreservesPullback.iso_hom_fst Scheme.forgetToTop f g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
⊢ Membership.mem (γ := Set ↥X)
    (Set.range (ι := (↑(pullback f.base g.base) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (X := pullback f.base g.base) (pullback.fst f.base g.base)) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X))
    x
have rw : Membership.mem (γ := Set ↥X) {x : ↥X | ∃ (y : ↥Y), Eq (α := ↥S) (f x : ↥S) (g y : ↥S)} x
Tactic: rw [TopCat.pullback_fst_range f.base g.base]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (hypothesis)
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
⊢ ∃ (a : ↥(pullback f g)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
              (Iso.hom (PreservesPullback.iso forgetToTop f g))
              (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
          (a : ↥(pullback f g)) → ↥X)
        a =
      x
have this : Membership.mem (γ := Set ↥X)
  (Set.range (ι := (↑(pullback f.base g.base) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
          TopCat.carrier) (X := pullback f.base g.base) (pullback.fst f.base g.base)) :
      (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X))
  x
Tactic: have : x ∈ Set.range (pullback.fst f.base g.base) := by
      rw [TopCat.pullback_fst_range f.base g.base]
      use y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
this :
  Membership.mem (γ := Set ↥X)
    (Set.range (ι := (↑(pullback f.base g.base) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
            TopCat.carrier) (X := pullback f.base g.base) (pullback.fst f.base g.base)) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X))
    x
⊢ ∃ (a : ↥(pullback f g)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
              (Iso.hom (PreservesPullback.iso forgetToTop f g))
              (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
          (a : ↥(pullback f g)) → ↥X)
        a =
      x
have obtain : ∀ (a : (↑(pullback f.base g.base) : Type u_1))
  (ha :
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (X := pullback f.base g.base) (pullback.fst f.base g.base) :
          (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X)
        a =
      x),
  ∃ (a : ↥(pullback f g)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
              (Iso.hom (PreservesPullback.iso forgetToTop f g))
              (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
          (a : ↥(pullback f g)) → ↥X)
        a =
      x
Tactic: obtain ⟨a, ha⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
a : (↑(pullback f.base g.base) : Type u_1)
ha :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := pullback f.base g.base) (pullback.fst f.base g.base) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X)
      a =
    x
⊢ ∃ (a : ↥(pullback f g)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
              (Iso.hom (PreservesPullback.iso forgetToTop f g))
              (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
          (a : ↥(pullback f g)) → ↥X)
        a =
      x
have h₁ : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
        (X := (↑(pullback f g).toPresheafedSpace : TopCat))
        (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
          (Iso.hom (PreservesPullback.iso forgetToTop f g)) (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
      (a : ↥(pullback f g)) → ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            (X := pullback (forgetToTop.map f) (forgetToTop.map g)) (Y := forgetToTop.obj (pullback f g))
            (Iso.inv (PreservesPullback.iso forgetToTop f g)) :
          (a : (↑(pullback (forgetToTop.map f) (forgetToTop.map g)) : Type u_1)) →
            (↑(forgetToTop.obj (pullback f g)) : Type u_1))
        a :
      (↑(forgetToTop.obj (pullback f g)) : Type u_1)) =
  x
Tactic: use (PreservesPullback.iso Scheme.forgetToTop f g).inv a
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
a : (↑(pullback f.base g.base) : Type u_1)
ha :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := pullback f.base g.base) (pullback.fst f.base g.base) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X)
      a =
    x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := (↑(pullback f g).toPresheafedSpace : TopCat))
          (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
            (Iso.hom (PreservesPullback.iso forgetToTop f g)) (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
        (a : ↥(pullback f g)) → ↥X)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X := pullback (forgetToTop.map f) (forgetToTop.map g)) (Y :=
              forgetToTop.obj (pullback f g)) (Iso.inv (PreservesPullback.iso forgetToTop f g)) :
            (a : (↑(pullback (forgetToTop.map f) (forgetToTop.map g)) : Type u_1)) →
              (↑(forgetToTop.obj (pullback f g)) : Type u_1))
          a :
        (↑(forgetToTop.obj (pullback f g)) : Type u_1)) =
    x
have h₁ : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
        (X := pullback (forgetToTop.map f) (forgetToTop.map g))
        (CategoryStruct.comp (Y := (↑(pullback f g).toPresheafedSpace : TopCat))
          (Iso.inv (PreservesPullback.iso forgetToTop f g))
          (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
            (Iso.hom (PreservesPullback.iso forgetToTop f g)) (pullback.fst (forgetToTop.map f) (forgetToTop.map g)))) :
      (a : (↑(pullback (forgetToTop.map f) (forgetToTop.map g)) : Type u_1)) → ↥X)
    a =
  x
Tactic: rwa [← TopCat.comp_app, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.MorphismProperty (goal)
Goal:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h_1 : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : Eq (α := ↥S) (f x : ↥S) (g y : ↥S)
a : (↑(pullback f.base g.base) : Type u_1)
ha :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := pullback f.base g.base) (pullback.fst f.base g.base) :
        (a : (↑(pullback f.base g.base) : Type u_1)) → ↥X)
      a =
    x
h₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := pullback (forgetToTop.map f) (forgetToTop.map g))
          (CategoryStruct.comp (Y := (↑(pullback f g).toPresheafedSpace : TopCat))
            (Iso.inv (PreservesPullback.iso forgetToTop f g))
            (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
              (Iso.hom (PreservesPullback.iso forgetToTop f g))
              (pullback.fst (forgetToTop.map f) (forgetToTop.map g)))) :
        (a : (↑(pullback (forgetToTop.map f) (forgetToTop.map g)) : Type u_1)) → ↥X)
      a =
    x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
          (X := (↑(pullback f g).toPresheafedSpace : TopCat))
          (CategoryStruct.comp (Y := pullback (forgetToTop.map f) (forgetToTop.map g))
            (Iso.hom (PreservesPullback.iso forgetToTop f g)) (pullback.fst (forgetToTop.map f) (forgetToTop.map g))) :
        (a : ↥(pullback f g)) → ↥X)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
              TopCat.carrier) (X := pullback (forgetToTop.map f) (forgetToTop.map g)) (Y :=
              forgetToTop.obj (pullback f g)) (Iso.inv (PreservesPullback.iso forgetToTop f g)) :
            (a : (↑(pullback (forgetToTop.map f) (forgetToTop.map g)) : Type u_1)) →
              (↑(forgetToTop.obj (pullback f g)) : Type u_1))
          a :
        (↑(forgetToTop.obj (pullback f g)) : Type u_1)) =
    x
have h₂ : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
        (X := pullback (forgetToTop.map f) (forgetToTop.map g)) (pullback.fst (forgetToTop.map f) (forgetToTop.map g)) :
      (a : (↑(pullback (forgetToTop.map f) (forgetToTop.map g)) : Type u_1)) → ↥X)
    a =
  x
Tactic: rwa [← TopCat.comp_app, Iso.inv_hom_id_assoc]