-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem image_morphismRestrict_preimage {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : Opens U) :
    (f ⁻¹ᵁ U).ι ''ᵁ ((f ∣_ U) ⁻¹ᵁ V) = f ⁻¹ᵁ (U.ι ''ᵁ V)

Proof state:
case h.e'_1
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : x ∈ f ⁻¹ᵁ U
hx' : (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ ∈ V
⊢ ↑⟨(ConcreteCategory.hom f.base) x, hx⟩ = ↑((ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩)

Tactic:
exact (morphismRestrict_base_coe f U ⟨x, hx⟩).symm

Result:
no goals

Proof state:
case h.h.mpr.intro.mk.intro
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
hx' : ⟨(ConcreteCategory.hom f.base) x, hx⟩ ∈ V.carrier
⊢ x ∈ ↑((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V)

Tactic:
refine ⟨⟨_, hx⟩, (?_ : (f ∣_ U).base ⟨x, hx⟩ ∈ V.1), rfl⟩

Result:
case h.h.mpr.intro.mk.intro
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
hx' : ⟨(ConcreteCategory.hom f.base) x, hx⟩ ∈ V.carrier
⊢ (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ ∈ V.carrier

Proof state:
case h.h.mp.intro.mk.intro
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : x ∈ f ⁻¹ᵁ U
hx' : (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ ∈ V
⊢ ⟨(ConcreteCategory.hom f.base) x, hx⟩ ∈ ↑V

Tactic:
convert hx'

Result:
case h.e'_1
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : x ∈ f ⁻¹ᵁ U
hx' : (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ ∈ V
⊢ ⟨(ConcreteCategory.hom f.base) x, hx⟩ = (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩

Proof state:
case h.h.mp
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) → x ∈ ↑(f ⁻¹ᵁ U.ι ''ᵁ V)

Tactic:
rintro ⟨⟨x, hx⟩, hx' : (f ∣_ U).base _ ∈ V, rfl⟩

Result:
case h.h.mp.intro.mk.intro
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : x ∈ f ⁻¹ᵁ U
hx' : (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ ∈ V
⊢ (ConcreteCategory.hom (Scheme.Hom.toLRSHom (f ⁻¹ᵁ U).ι).base) ⟨x, hx⟩ ∈ ↑(f ⁻¹ᵁ U.ι ''ᵁ V)

Proof state:
case h.h.mp.intro.mk.intro
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : x ∈ f ⁻¹ᵁ U
hx' : (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ ∈ V
⊢ (ConcreteCategory.hom (Scheme.Hom.toLRSHom (f ⁻¹ᵁ U).ι).base) ⟨x, hx⟩ ∈ ↑(f ⁻¹ᵁ U.ι ''ᵁ V)

Tactic:
refine ⟨⟨_, hx⟩, ?_, rfl⟩

Result:
case h.h.mp.intro.mk.intro
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : x ∈ f ⁻¹ᵁ U
hx' : (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ ∈ V
⊢ ⟨(ConcreteCategory.hom f.base) x, hx⟩ ∈ ↑V

Proof state:
case h.h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ↔ x ∈ ↑(f ⁻¹ᵁ U.ι ''ᵁ V)

Tactic:
constructor

Result:
case h.h.mp
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) → x ∈ ↑(f ⁻¹ᵁ U.ι ''ᵁ V)

case h.h.mpr
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(f ⁻¹ᵁ U.ι ''ᵁ V) → x ∈ ↑((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V)

Proof state:
case h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
⊢ ↑((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) = ↑(f ⁻¹ᵁ U.ι ''ᵁ V)

Tactic:
ext x

Result:
case h.h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) ↔ x ∈ ↑(f ⁻¹ᵁ U.ι ''ᵁ V)

Proof state:
case h.e'_5
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
hx' : ⟨(ConcreteCategory.hom f.base) x, hx⟩ ∈ V.carrier
⊢ ↑((ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩) = ↑⟨(ConcreteCategory.hom f.base) x, hx⟩

Tactic:
exact morphismRestrict_base_coe f U ⟨x, hx⟩

Result:
no goals

Proof state:
case h.e'_1
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : x ∈ f ⁻¹ᵁ U
hx' : (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ ∈ V
⊢ ⟨(ConcreteCategory.hom f.base) x, hx⟩ = (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩

Tactic:
refine Subtype.ext ?_

Result:
case h.e'_1
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : x ∈ f ⁻¹ᵁ U
hx' : (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ ∈ V
⊢ ↑⟨(ConcreteCategory.hom f.base) x, hx⟩ = ↑((ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩)

Proof state:
case h.h.mpr.intro.mk.intro
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
hx' : ⟨(ConcreteCategory.hom f.base) x, hx⟩ ∈ V.carrier
⊢ (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ ∈ V.carrier

Tactic:
convert hx'

Result:
case h.e'_5
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
hx' : ⟨(ConcreteCategory.hom f.base) x, hx⟩ ∈ V.carrier
⊢ (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ = ⟨(ConcreteCategory.hom f.base) x, hx⟩

Proof state:
case h.e'_5
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
hx' : ⟨(ConcreteCategory.hom f.base) x, hx⟩ ∈ V.carrier
⊢ (ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩ = ⟨(ConcreteCategory.hom f.base) x, hx⟩

Tactic:
refine Subtype.ext ?_

Result:
case h.e'_5
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
hx' : ⟨(ConcreteCategory.hom f.base) x, hx⟩ ∈ V.carrier
⊢ ↑((ConcreteCategory.hom (f ∣_ U).base) ⟨x, hx⟩) = ↑⟨(ConcreteCategory.hom f.base) x, hx⟩

Proof state:
case h.h.mpr
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(f ⁻¹ᵁ U.ι ''ᵁ V) → x ∈ ↑((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V)

Tactic:
rintro ⟨⟨x, hx⟩, hx' : _ ∈ V.1, rfl : x = _⟩

Result:
case h.h.mpr.intro.mk.intro
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
hx' : ⟨(ConcreteCategory.hom f.base) x, hx⟩ ∈ V.carrier
⊢ x ∈ ↑((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V)

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
⊢ (f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V = f ⁻¹ᵁ U.ι ''ᵁ V

Tactic:
ext1

Result:
case h
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : Opens ↑↑(↑U).toPresheafedSpace
⊢ ↑((f ⁻¹ᵁ U).ι ''ᵁ (f ∣_ U) ⁻¹ᵁ V) = ↑(f ⁻¹ᵁ U.ι ''ᵁ V)