-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem range_pullback_fst_of_right :
    Set.range (pullback.fst g f).base =
      ((Opens.map g.base).obj ⟨Set.range f.base, H.base_open.isOpen_range⟩).1

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom (pullback.fst g f).base) =
    ((Opens.map g.base).obj { carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }).carrier

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)]

Result:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) ''
      (⇑(ConcreteCategory.hom (pullback.snd g.base f.base)) ⁻¹' Set.univ) =
    ((Opens.map g.base).obj { carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }).carrier

X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop g f).hom)

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹'
      (⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) '' Set.univ) =
    ((Opens.map g.base).obj { carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }).carrier

Tactic:
rw [Set.image_univ]

Result:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) =
    ((Opens.map g.base).obj { carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }).carrier

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) ''
      (⇑(ConcreteCategory.hom (pullback.snd g.base f.base)) ⁻¹' Set.univ) =
    ((Opens.map g.base).obj { carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }).carrier

Tactic:
erw [TopCat.pullback_fst_image_snd_preimage]

Result:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹'
      (⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) '' Set.univ) =
    ((Opens.map g.base).obj { carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }).carrier

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) =
    ((Opens.map g.base).obj { carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }).carrier

Tactic:
rfl

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop g f).hom

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso Scheme.forgetToTop g f).hom)

Tactic:
rw [← TopCat.epi_iff_surjective]

Result:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Epi (PreservesPullback.iso Scheme.forgetToTop g f).hom