awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsIso f ↔ IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
have rw : ((Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f) ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)) ↔
  IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
Tactic: rw [isIso_iff_isOpenImmersion_and_epi_base,
    IsOpenImmersion.iff_isIso_stalkMap, and_comm, ← and_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ ((Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f) ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)) ↔
    IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
have refine_1 : Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f → IsIso f.base
Tactic: refine and_congr ⟨?_, ?_⟩ Iff.rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
refine_1 : Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f → IsIso f.base
⊢ ((Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f) ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)) ↔
    IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
have refine_2 : IsIso f.base → Epi f.base ∧ IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f
Tactic: refine and_congr ⟨?_, ?_⟩ Iff.rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h₁ : Epi f.base
h₂ : IsOpenEmbedding (X := ↥X) (Y := ↥Y) ⇑f
⊢ IsIso f.base
have refine_1 : IsIso (TopCat.isoOfHomeo ((Equiv.ofBijective ⇑f sorry).toHomeomorphOfContinuousOpen sorry sorry)).hom
Tactic: convert_to
      IsIso
        (TopCat.isoOfHomeo
          (Equiv.toHomeomorphOfContinuousOpen
            (.ofBijective _ ⟨h₂.injective, (TopCat.epi_iff_surjective _).mp h₁⟩) h₂.continuous
            h₂.isOpenMap)).hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan f g ⋙ forget)
have rw : HasLimit (cospan ((cospan f g ⋙ forget).map WalkingCospan.Hom.inl) ((cospan f g ⋙ forget).map WalkingCospan.Hom.inr))
Tactic: rw [hasLimit_iff_of_iso (diagramIsoCospan _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan g f ⋙ forget)
have rw : HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))
Tactic: rw [hasLimit_iff_of_iso (diagramIsoCospan _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (X := pullback f g) (pullback.snd f g)
have this : Eq (α := forget.obj (pullback f g) ⟶ forget.obj Y)
  (CategoryStruct.comp (Y := pullback (forget.map f) (forget.map g)) (Iso.hom (PreservesPullback.iso forget f g))
    (pullback.snd (forget.map f) (forget.map g)))
  (forget.map (pullback.snd f g))
Tactic: have := PreservesPullback.iso_hom_snd forget f g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  Eq (α := (pullback f g).toLocallyRingedSpace ⟶ Y.toLocallyRingedSpace)
    (CategoryStruct.comp (Y := pullback (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))
      (Iso.hom
        (PreservesPullback.iso
          { obj := Scheme.toLocallyRingedSpace, map := fun {X Y : Scheme.{u}} ↦ Scheme.Hom.toLRSHom,
            map_id := Scheme.forgetToLocallyRingedSpace._proof_1,
            map_comp := @Scheme.forgetToLocallyRingedSpace._proof_2 }
          f g))
      (pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g)))
    (Scheme.Hom.toLRSHom (pullback.snd f g))
⊢ LocallyRingedSpace.IsOpenImmersion (X := (pullback f g).toLocallyRingedSpace) (Scheme.Hom.toLRSHom (pullback.snd f g))
have rw : LocallyRingedSpace.IsOpenImmersion (X := (pullback f g).toLocallyRingedSpace)
  (CategoryStruct.comp (Y := pullback (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))
    (Iso.hom
      (PreservesPullback.iso
        { obj := Scheme.toLocallyRingedSpace, map := fun {X Y : Scheme.{u}} ↦ Scheme.Hom.toLRSHom,
          map_id := Scheme.forgetToLocallyRingedSpace._proof_1,
          map_comp := @Scheme.forgetToLocallyRingedSpace._proof_2 }
        f g))
    (pullback.snd (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g)))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (X := pullback g f) (pullback.fst g f)
have rw : IsOpenImmersion (X := pullback g f) (Iso.hom (pullbackSymmetry g f) ≫ pullback.snd f g)
Tactic: rw [← pullbackSymmetry_hom_comp_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) one)
have rw : IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) left ≫ (cospan f g).map Hom.inl)
Tactic: rw [← limit.w (cospan f g) WalkingCospan.Hom.inl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) left ≫ (cospan f g).map Hom.inl)
have change : IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) left ≫ f)
Tactic: change IsOpenImmersion (_ ≫ f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g) (forget ⋙ LocallyRingedSpace.forgetToTop)
have refine_1 : PreservesLimit (cospan f g) forget
Tactic: refine @Limits.comp_preservesLimit _ _ _ _ _ _ (K := cospan f g) _ _ (F := forget)
    (G := LocallyRingedSpace.forgetToTop) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
refine_1 : PreservesLimit (cospan f g) forget
⊢ PreservesLimit (cospan f g) (forget ⋙ LocallyRingedSpace.forgetToTop)
have refine_2 : PreservesLimit (cospan f g ⋙ forget) LocallyRingedSpace.forgetToTop
Tactic: refine @Limits.comp_preservesLimit _ _ _ _ _ _ (K := cospan f g) _ _ (F := forget)
    (G := LocallyRingedSpace.forgetToTop) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g ⋙ forget) LocallyRingedSpace.forgetToTop
have refine_2 : PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
  LocallyRingedSpace.forgetToTop
Tactic: refine @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoCospan.{u} _).symm ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
    LocallyRingedSpace.forgetToTop
have refine_2 : PreservesLimit (cospan (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))
  (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat)
Tactic: dsimp [LocallyRingedSpace.forgetToTop]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g) = (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
have rw : Set.image (α := (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
          (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) :
      (a : (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u)) → ↥Y)
    (Set.preimage (β := ↥X)
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := pullback f.base g.base) (pullback.fst f.base g.base)) :
        (a : (↑(pullback f.base g.base) : Type u)) → ↥X)
      Set.univ) =
  (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
Tactic: rw [← show _ = (pullback.snd f g).base from
    PreservesPullback.iso_hom_snd Scheme.forgetToTop f g, TopCat.coe_comp, Set.range_comp,
    Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.fst f.base g.base)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Set.image (α := (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
            (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) :
        (a : (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u)) → ↥Y)
      (Set.preimage (β := ↥X)
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := pullback f.base g.base) (pullback.fst f.base g.base)) :
          (a : (↑(pullback f.base g.base) : Type u)) → ↥X)
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
⊢ Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g) = (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
have rw₁ : Function.Surjective (α := ↥(pullback f g)) (β :=
  (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
        (↑(pullback f g).toPresheafedSpace : TopCat)) (Y :=
        pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
        (Iso.hom (PreservesPullback.iso Scheme.forgetToTop f g))) :
    (a : ↥(pullback f g)) → (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
Tactic: rw [← show _ = (pullback.snd f g).base from
    PreservesPullback.iso_hom_snd Scheme.forgetToTop f g, TopCat.coe_comp, Set.range_comp,
    Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.fst f.base g.base)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.image (α := (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
            (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) :
        (a : (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u)) → ↥Y)
      (Set.preimage (β := ↥X)
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := pullback f.base g.base) (pullback.fst f.base g.base)) :
          (a : (↑(pullback f.base g.base) : Type u)) → ↥X)
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
have erw : Set.preimage (β := (↑(Scheme.forgetToTop.obj Z) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (Scheme.forgetToTop.map g)) :
      (a : ↥Y) → (↑(Scheme.forgetToTop.obj Z) : Type u))
    (Set.image (α := (↑(Scheme.forgetToTop.obj X) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (Scheme.forgetToTop.map f)) :
        (a : (↑(Scheme.forgetToTop.obj X) : Type u)) → (↑(Scheme.forgetToTop.obj Z) : Type u))
      Set.univ) =
  (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
Tactic: erw [TopCat.pullback_snd_image_fst_preimage]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.preimage (β := (↑(Scheme.forgetToTop.obj Z) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (Scheme.forgetToTop.map g)) :
        (a : ↥Y) → (↑(Scheme.forgetToTop.obj Z) : Type u))
      (Set.image (α := (↑(Scheme.forgetToTop.obj X) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Scheme.forgetToTop.map f)) :
          (a : (↑(Scheme.forgetToTop.obj X) : Type u)) → (↑(Scheme.forgetToTop.obj Z) : Type u))
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
have rw : Set.preimage (β := (↑(Scheme.forgetToTop.obj Z) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (Scheme.forgetToTop.map g)) :
      (a : ↥Y) → (↑(Scheme.forgetToTop.obj Z) : Type u))
    (Set.range (ι := (↑(Scheme.forgetToTop.obj X) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (Scheme.forgetToTop.map f)) :
        (a : (↑(Scheme.forgetToTop.obj X) : Type u)) → (↑(Scheme.forgetToTop.obj Z) : Type u))) =
  (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
Tactic: rw [Set.image_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective (α := ↥(pullback f g)) (β :=
    (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(pullback f g).toPresheafedSpace : TopCat)) (Y :=
          pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
          (Iso.hom (PreservesPullback.iso Scheme.forgetToTop f g))) :
      (a : ↥(pullback f g)) → (↑(pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) : Type u))
have rw : Epi (X := (↑(pullback f g).toPresheafedSpace : TopCat)) (Y :=
  pullback (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))
  (Iso.hom (PreservesPullback.iso Scheme.forgetToTop f g))
Tactic: rw [← TopCat.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f) = (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
have rw : Set.image (α := (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
          (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) :
      (a : (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u)) → ↥Y)
    (Set.preimage (β := ↥X)
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := pullback g.base f.base) (pullback.snd g.base f.base)) :
        (a : (↑(pullback g.base f.base) : Type u)) → ↥X)
      Set.univ) =
  (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
Tactic: rw [← show _ = (pullback.fst g f).base from
    PreservesPullback.iso_hom_fst Scheme.forgetToTop g f, TopCat.coe_comp, Set.range_comp,
    Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.snd g.base f.base)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Set.image (α := (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
            (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) :
        (a : (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u)) → ↥Y)
      (Set.preimage (β := ↥X)
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := pullback g.base f.base) (pullback.snd g.base f.base)) :
          (a : (↑(pullback g.base f.base) : Type u)) → ↥X)
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
⊢ Set.range (ι := ↥(pullback g f)) ⇑(pullback.fst g f) = (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
have rw₁ : Function.Surjective (α := ↥(pullback g f)) (β :=
  (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
        (↑(pullback g f).toPresheafedSpace : TopCat)) (Y :=
        pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
        (Iso.hom (PreservesPullback.iso Scheme.forgetToTop g f))) :
    (a : ↥(pullback g f)) → (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
Tactic: rw [← show _ = (pullback.fst g f).base from
    PreservesPullback.iso_hom_fst Scheme.forgetToTop g f, TopCat.coe_comp, Set.range_comp,
    Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.snd g.base f.base)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.image (α := (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
            (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) :
        (a : (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u)) → ↥Y)
      (Set.preimage (β := ↥X)
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := pullback g.base f.base) (pullback.snd g.base f.base)) :
          (a : (↑(pullback g.base f.base) : Type u)) → ↥X)
        Set.univ) =
    (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
have erw : Set.preimage (β := (↑(Scheme.forgetToTop.obj Z) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (Scheme.forgetToTop.map g)) :
      (a : ↥Y) → (↑(Scheme.forgetToTop.obj Z) : Type u))
    (Set.image (α := (↑(Scheme.forgetToTop.obj X) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (Scheme.forgetToTop.map f)) :
        (a : (↑(Scheme.forgetToTop.obj X) : Type u)) → (↑(Scheme.forgetToTop.obj Z) : Type u))
      Set.univ) =
  (↑(g ⁻¹ᵁ Scheme.Hom.opensRange f) : Set ↥Y)
Tactic: erw [TopCat.pullback_fst_image_snd_preimage]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective (α := ↥(pullback g f)) (β :=
    (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(pullback g f).toPresheafedSpace : TopCat)) (Y :=
          pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
          (Iso.hom (PreservesPullback.iso Scheme.forgetToTop g f))) :
      (a : ↥(pullback g f)) → (↑(pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) : Type u))
have rw : Epi (X := (↑(pullback g f).toPresheafedSpace : TopCat)) (Y :=
  pullback (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))
  (Iso.hom (PreservesPullback.iso Scheme.forgetToTop g f))
Tactic: rw [← TopCat.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw : Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g ≫ g))
  (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
Tactic: rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw₁ : Eq (α := Set ↥Z)
  (Set.range (ι := ↥(pullback f g))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(pullback f g).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.snd f g))) ≫
            g.base)) :
      (a : ↥(pullback f g)) → ↥Z))
  (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
Tactic: rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
rw :
  Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.snd f g ≫ g))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
rw₁ :
  Eq (α := Set ↥Z)
    (Set.range (ι := ↥(pullback f g))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(pullback f g).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (pullback.snd f g))) ≫
              g.base)) :
        (a : ↥(pullback f g)) → ↥Z))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) ⇑(pullback.fst f g ≫ f))
    (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
have rw₂ : Eq (α := Set ↥Z) (Set.range (ι := ↥(pullback f g)) (Function.comp (β := ↥Y) ⇑g ⇑(pullback.snd f g)))
  (Set.range (ι := ↥X) ⇑f ∩ Set.range (ι := ↥Y) ⇑g)
Tactic: rw [pullback.condition, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp,
    range_pullbackSnd, Opens.map_obj, Opens.coe_mk,
    Set.image_preimage_eq_inter_range, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]