-- Mathlib/AlgebraicGeometry/Properties.lean
theorem reduce_to_affine_nbhd (P : ∀ (X : Scheme) (_ : X), Prop)
    (h₁ : ∀ R x, P (Spec R) x)
    (h₂ : ∀ {X Y} (f : X ⟶ Y) [IsOpenImmersion f] (x : X), P X x → P Y (f.base x)) :
    ∀ (X : Scheme) (x : X), P X x

Proof state:
P : (X : Scheme) → ↑↑X.toPresheafedSpace → Prop
h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x
h₂ :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace),
    P X x → P Y ((ConcreteCategory.hom f.base) x)
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ P X x

Tactic:
obtain ⟨y, e⟩ := X.affineCover.covers x

Result:
case intro
P : (X : Scheme) → ↑↑X.toPresheafedSpace → Prop
h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x
h₂ :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace),
    P X x → P Y ((ConcreteCategory.hom f.base) x)
X : Scheme
x : ↑↑X.toPresheafedSpace
y : ↑↑(X.affineCover.obj (X.affineCover.f x)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f x)).base) y = x
⊢ P X x

Proof state:
case intro
P : (X : Scheme) → ↑↑X.toPresheafedSpace → Prop
h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x
h₂ :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace),
    P X x → P Y ((ConcreteCategory.hom f.base) x)
X : Scheme
x : ↑↑X.toPresheafedSpace
y : ↑↑(X.affineCover.obj (X.affineCover.f x)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f x)).base) y = x
⊢ P X x

Tactic:
convert h₂ (X.affineCover.map (X.affineCover.f x)) y _

Result:
case h.e'_2
P : (X : Scheme) → ↑↑X.toPresheafedSpace → Prop
h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x
h₂ :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace),
    P X x → P Y ((ConcreteCategory.hom f.base) x)
X : Scheme
x : ↑↑X.toPresheafedSpace
y : ↑↑(X.affineCover.obj (X.affineCover.f x)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f x)).base) y = x
⊢ x = (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f x)).base) y

case intro
P : (X : Scheme) → ↑↑X.toPresheafedSpace → Prop
h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x
h₂ :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace),
    P X x → P Y ((ConcreteCategory.hom f.base) x)
X : Scheme
x : ↑↑X.toPresheafedSpace
y : ↑↑(X.affineCover.obj (X.affineCover.f x)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f x)).base) y = x
⊢ P (X.affineCover.obj (X.affineCover.f x)) y

Proof state:
P : (X : Scheme) → ↑↑X.toPresheafedSpace → Prop
h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x
h₂ :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace),
    P X x → P Y ((ConcreteCategory.hom f.base) x)
⊢ ∀ (X : Scheme) (x : ↑↑X.toPresheafedSpace), P X x

Tactic:
intro X x

Result:
P : (X : Scheme) → ↑↑X.toPresheafedSpace → Prop
h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x
h₂ :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace),
    P X x → P Y ((ConcreteCategory.hom f.base) x)
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ P X x

Proof state:
case intro
P : (X : Scheme) → ↑↑X.toPresheafedSpace → Prop
h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x
h₂ :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace),
    P X x → P Y ((ConcreteCategory.hom f.base) x)
X : Scheme
x : ↑↑X.toPresheafedSpace
y : ↑↑(X.affineCover.obj (X.affineCover.f x)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f x)).base) y = x
⊢ P (X.affineCover.obj (X.affineCover.f x)) y

Tactic:
apply h₁

Result:
no goals

Proof state:
case h.e'_2
P : (X : Scheme) → ↑↑X.toPresheafedSpace → Prop
h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x
h₂ :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace),
    P X x → P Y ((ConcreteCategory.hom f.base) x)
X : Scheme
x : ↑↑X.toPresheafedSpace
y : ↑↑(X.affineCover.obj (X.affineCover.f x)).toPresheafedSpace
e : (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f x)).base) y = x
⊢ x = (ConcreteCategory.hom (X.affineCover.map (X.affineCover.f x)).base) y

Tactic:
rw [e]

Result:
no goals