-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
/-- If `P` is local at the source, local at the target and is stable under post-composition with
open immersions, then `P` can be checked locally around points. -/
lemma iff_exists_resLE [IsLocalAtTarget P] [P.RespectsRight @IsOpenImmersion] :
    P f ↔ ∀ x : X, ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.1) (e : V ≤ f ⁻¹ᵁ U),
      P (f.resLE U V e)

Proof state:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ ∀ (i : ↑↑X.toPresheafedSpace), P ((V i).ι ≫ f)

Tactic:
intro x

Result:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↑↑X.toPresheafedSpace
⊢ P ((V x).ι ≫ f)

Proof state:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(⨆ x, V x)

Tactic:
simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe]

Result:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↑↑X.toPresheafedSpace
⊢ ∃ i, x ∈ V i

Proof state:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ P f

Tactic:
rw [IsLocalAtSource.iff_of_iSup_eq_top (fun x : X ↦ V x) (P := P)]

Result:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ ∀ (i : ↑↑X.toPresheafedSpace), P ((V i).ι ≫ f)

P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ ⨆ x, V x = ⊤

Proof state:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
hf : P f
x : ↑↑X.toPresheafedSpace
⊢ ⊤ ≤ f ⁻¹ᵁ ⊤

Tactic:
simp

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↑↑X.toPresheafedSpace
⊢ P (Scheme.Hom.resLE f (U x) (V x) ⋯ ≫ (U x).ι)

Tactic:
exact MorphismProperty.RespectsRight.postcomp (Q := @IsOpenImmersion) _ inferInstance _ (hf x)

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↑↑X.toPresheafedSpace
⊢ ∃ i, x ∈ V i

Tactic:
use x, hxU x

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↑↑X.toPresheafedSpace
⊢ P ((V x).ι ≫ f)

Tactic:
rw [← Scheme.Hom.resLE_comp_ι _ (e x)]

Result:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↑↑X.toPresheafedSpace
⊢ P (Scheme.Hom.resLE f (U x) (V x) ⋯ ≫ (U x).ι)

Proof state:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
⊢ P f ↔ ∀ (x : ↑↑X.toPresheafedSpace), ∃ U V, ∃ (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)

Tactic:
refine ⟨fun hf x ↦ ⟨⊤, ⊤, trivial, by simp, resLE _ hf⟩, fun hf ↦ ?_⟩

Result:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
hf : ∀ (x : ↑↑X.toPresheafedSpace), ∃ U V, ∃ (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)
⊢ P f

Proof state:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
hf : ∀ (x : ↑↑X.toPresheafedSpace), ∃ U V, ∃ (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)
⊢ P f

Tactic:
choose U V hxU e hf using hf

Result:
P : MorphismProperty Scheme
inst✝² : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocalAtTarget P
inst✝ : P.RespectsRight @IsOpenImmersion
U : ↑↑X.toPresheafedSpace → Y.Opens
V : ↑↑X.toPresheafedSpace → X.Opens
hxU : ∀ (x : ↑↑X.toPresheafedSpace), x ∈ (V x).carrier
e : ∀ (x : ↑↑X.toPresheafedSpace), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ P f