-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem lift_range (H' : Set.range g.base ⊆ Set.range f.base) :
    Set.range (lift f g H').base = f.base ⁻¹' Set.range g.base

Proof state:
case h
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈
      {x |
        ∃ y,
          (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x =
            (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y} ↔
    x✝ ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
constructor

Result:
case h.mp
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈
      {x |
        ∃ y,
          (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x =
            (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y} →
    x✝ ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

case h.mpr
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base) →
    x✝ ∈
      {x |
        ∃ y,
          (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x =
            (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y}

Proof state:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ {x |
      ∃ y,
        (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x =
          (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y} =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
ext

Result:
case h
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈
      {x |
        ∃ y,
          (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x =
            (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y} ↔
    x✝ ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Proof state:
case h.mpr.intro
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
x✝ : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
eq : (ConcreteCategory.hom g.base) y = (ConcreteCategory.hom f.base) x✝
⊢ x✝ ∈
    {x |
      ∃ y,
        (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x =
          (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y}

Tactic:
exact ⟨y, eq.symm⟩

Result:
no goals

Proof state:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ Function.Surjective
    ⇑(ConcreteCategory.hom
        ((inv (pullback.snd f g)).base ≫
          (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom))

Tactic:
rw [← TopCat.epi_iff_surjective, show (inv (pullback.snd f g)).base = _ from
    (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _).map_inv _]

Result:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ Epi
    (inv ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map (pullback.snd f g)) ≫
      (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom)