-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
theorem preimage_basicOpen {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) {U : Opens Y}
    (s : Y.presheaf.obj (op U)) :
    (Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) =
      @RingedSpace.basicOpen X.toRingedSpace ((Opens.map f.base).obj U) (f.c.app _ s)

Proof state:
case h.h.mpr.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s))

Tactic:
simp only [Opens.map_coe, Set.mem_preimage, SetLike.mem_coe, toRingedSpace] at hx ⊢

Result:
case h.h.mpr.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
⊢ (ConcreteCategory.hom f.base) x ∈ RingedSpace.basicOpen Y.toSheafedSpace s

Proof state:
case h.h.mpr.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
⊢ (ConcreteCategory.hom f.base) x ∈ RingedSpace.basicOpen Y.toSheafedSpace s

Tactic:
rw [RingedSpace.mem_basicOpen _ s (f.base x) hxU]

Result:
case h.h.mpr.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
⊢ IsUnit ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)

Proof state:
case h.h.mpr
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)) →
    x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s))

Tactic:
rintro ⟨hxU, hx⟩

Result:
case h.h.mpr.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s))

Proof state:
case h.h.mp.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))

Tactic:
rw [SetLike.mem_coe, X.toRingedSpace.mem_basicOpen _ _ hxU]

Result:
case h.h.mp.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
⊢ (Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) =
    X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)

Tactic:
ext x

Result:
case h.h
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) ↔
    x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))

Proof state:
case h.h
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) ↔
    x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))

Tactic:
constructor

Result:
case h.h.mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) →
    x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))

case h.h.mpr
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)) →
    x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s))

Proof state:
case h.h.mp.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (Hom.stalkMap f x))
      ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s))

Tactic:
exact (f.stalkMap _).hom.isUnit_map hx

Result:
no goals

Proof state:
case h.h.mp.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))

Tactic:
rw [← stalkMap_germ_apply]

Result:
case h.h.mp.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (Hom.stalkMap f x))
      ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s))

Proof state:
case h.h.mpr.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (Hom.stalkMap f x))
      ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s))
⊢ IsUnit ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)

Tactic:
exact (isUnit_map_iff (f.toShHom.stalkMap _).hom _).mp hx

Result:
no goals

Proof state:
case h.h.mp.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))

Tactic:
delta toRingedSpace

Result:
case h.h.mp.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))