-- Mathlib/Geometry/RingedSpace/Basic.lean
theorem basicOpen_res {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) (f : X.presheaf.obj U) :
    @basicOpen X (unop V) (X.presheaf.map i f) = unop V ⊓ @basicOpen X (unop U) f

Proof state:
case h.h.mp.intro
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ unop V
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x ⋯)) f)
⊢ x ∈ ↑(unop V ⊓ X.basicOpen f)

Tactic:
exact ⟨hxV, i.unop.le hxV, hx⟩

Result:
no goals

Proof state:
case h.h.mpr.intro.intro
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑(unop V)
w✝ : x ∈ unop U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x w✝)) f)
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f))

Tactic:
refine ⟨hxV, ?_⟩

Result:
case h.h.mpr.intro.intro
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑(unop V)
w✝ : x ∈ unop U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x w✝)) f)
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop V) x hxV)) ((ConcreteCategory.hom (X.presheaf.map i)) f))

Proof state:
case h.h
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)) ↔ x ∈ ↑(unop V ⊓ X.basicOpen f)

Tactic:
constructor

Result:
case h.h.mp
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)) → x ∈ ↑(unop V ⊓ X.basicOpen f)

case h.h.mpr
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(unop V ⊓ X.basicOpen f) → x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f))

Proof state:
case h.h.mpr
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(unop V ⊓ X.basicOpen f) → x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f))

Tactic:
rintro ⟨hxV, _, hx⟩

Result:
case h.h.mpr.intro.intro
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑(unop V)
w✝ : x ∈ unop U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x w✝)) f)
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f))

Proof state:
case h.h.mp.intro
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ unop V
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop V) x hxV)) ((ConcreteCategory.hom (X.presheaf.map i)) f))
⊢ x ∈ ↑(unop V ⊓ X.basicOpen f)

Tactic:
rw [germ_res_apply' X.presheaf] at hx

Result:
case h.h.mp.intro
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ unop V
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x ⋯)) f)
⊢ x ∈ ↑(unop V ⊓ X.basicOpen f)

Proof state:
case h.h.mpr.intro.intro
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑(unop V)
w✝ : x ∈ unop U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x w✝)) f)
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop V) x hxV)) ((ConcreteCategory.hom (X.presheaf.map i)) f))

Tactic:
rw [germ_res_apply' X.presheaf]

Result:
case h.h.mpr.intro.intro
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑(unop V)
w✝ : x ∈ unop U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x w✝)) f)
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x ⋯)) f)

Proof state:
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f) = unop V ⊓ X.basicOpen f

Tactic:
ext x

Result:
case h.h
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)) ↔ x ∈ ↑(unop V ⊓ X.basicOpen f)

Proof state:
case h.h.mp
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)) → x ∈ ↑(unop V ⊓ X.basicOpen f)

Tactic:
rintro ⟨hxV, hx⟩

Result:
case h.h.mp.intro
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ unop V
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop V) x hxV)) ((ConcreteCategory.hom (X.presheaf.map i)) f))
⊢ x ∈ ↑(unop V ⊓ X.basicOpen f)

Proof state:
case h.h.mpr.intro.intro
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑(unop V)
w✝ : x ∈ unop U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x w✝)) f)
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop U) x ⋯)) f)

Tactic:
exact hx

Result:
no goals