-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
/-- If `P` holds for `f` over affine opens `U₂` of `Y` and `V₂` of `X` and `U₁` (resp. `V₁`) are
open neighborhoods of `x` (resp. `f.base x`), then `P` also holds for `f` over some affine open
`U'` of `Y` (resp. `V'` of `X`) that is contained in `U₁` (resp. `V₁`). -/
lemma exists_affineOpens_le_appLE_of_appLE
    (hPa : StableUnderCompositionWithLocalizationAwayTarget P) (hPl : LocalizationAwayPreserves P)
    (x : X) (U₁ : Y.Opens) (U₂ : Y.affineOpens) (V₁ : X.Opens) (V₂ : X.affineOpens)
    (hx₁ : x ∈ V₁) (hx₂ : x ∈ V₂.1) (e₂ : V₂.1 ≤ f ⁻¹ᵁ U₂.1) (h₂ : P (f.appLE U₂ V₂ e₂).hom)
    (hfx₁ : f.base x ∈ U₁.1) :
    ∃ (U' : Y.affineOpens) (V' : X.affineOpens) (_ : U'.1 ≤ U₁) (_ : V'.1 ≤ V₁) (_ : x ∈ V'.1)
      (e : V'.1 ≤ f⁻¹ᵁ U'.1), P (f.appLE U' V' e).hom

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
x : ↑↑X.toPresheafedSpace
U₁ : Y.Opens
U₂ : ↑Y.affineOpens
V₁ : X.Opens
V₂ : ↑X.affineOpens
hx₁ : x ∈ V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : (ConcreteCategory.hom f.base) x ∈ U₁.carrier
r : ↑Γ(Y, ↑U₂)
hBr : Y.basicOpen r ≤ U₁
hBfx : ↑⟨(ConcreteCategory.hom f.base) x, hfx₁⟩ ∈ Y.basicOpen r
s : ↑Γ(X, ↑V₂)
hBs : X.basicOpen s ≤ V₁
hBx : ↑⟨x, hx₁⟩ ∈ X.basicOpen s
r' : ↑Γ(Y, ↑⟨Y.basicOpen r, ⋯⟩)
s' : ↑Γ(X, ↑⟨X.basicOpen s, ⋯⟩)
hBx' : x ∈ X.basicOpen s'
e' : X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r'
hf' : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') e'))
⊢ ∃ U' V',
    ∃ (_ : ↑U' ≤ U₁) (_ : ↑V' ≤ V₁) (_ : x ∈ ↑V') (e : ↑V' ≤ f ⁻¹ᵁ ↑U'),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U') (↑V') e))

Tactic:
exact ⟨⟨Y.basicOpen r', (U₂.2.basicOpen _).basicOpen _⟩,
  ⟨X.basicOpen s', (V₂.2.basicOpen _).basicOpen _⟩, le_trans (Y.basicOpen_le _) hBr,
  le_trans (X.basicOpen_le _) hBs, hBx', e', hf'⟩

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
x : ↑↑X.toPresheafedSpace
U₁ : Y.Opens
U₂ : ↑Y.affineOpens
V₁ : X.Opens
V₂ : ↑X.affineOpens
hx₁ : x ∈ V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : (ConcreteCategory.hom f.base) x ∈ U₁.carrier
⊢ ∃ U' V',
    ∃ (_ : ↑U' ≤ U₁) (_ : ↑V' ≤ V₁) (_ : x ∈ ↑V') (e : ↑V' ≤ f ⁻¹ᵁ ↑U'),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U') (↑V') e))

Tactic:
obtain ⟨r, hBr, hBfx⟩ := U₂.2.exists_basicOpen_le ⟨f.base x, hfx₁⟩ (e₂ hx₂)

Result:
case intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
x : ↑↑X.toPresheafedSpace
U₁ : Y.Opens
U₂ : ↑Y.affineOpens
V₁ : X.Opens
V₂ : ↑X.affineOpens
hx₁ : x ∈ V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : (ConcreteCategory.hom f.base) x ∈ U₁.carrier
r : ↑Γ(Y, ↑U₂)
hBr : Y.basicOpen r ≤ U₁
hBfx : ↑⟨(ConcreteCategory.hom f.base) x, hfx₁⟩ ∈ Y.basicOpen r
⊢ ∃ U' V',
    ∃ (_ : ↑U' ≤ U₁) (_ : ↑V' ≤ V₁) (_ : x ∈ ↑V') (e : ↑V' ≤ f ⁻¹ᵁ ↑U'),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U') (↑V') e))

Proof state:
case intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
x : ↑↑X.toPresheafedSpace
U₁ : Y.Opens
U₂ : ↑Y.affineOpens
V₁ : X.Opens
V₂ : ↑X.affineOpens
hx₁ : x ∈ V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : (ConcreteCategory.hom f.base) x ∈ U₁.carrier
r : ↑Γ(Y, ↑U₂)
hBr : Y.basicOpen r ≤ U₁
hBfx : ↑⟨(ConcreteCategory.hom f.base) x, hfx₁⟩ ∈ Y.basicOpen r
⊢ ∃ U' V',
    ∃ (_ : ↑U' ≤ U₁) (_ : ↑V' ≤ V₁) (_ : x ∈ ↑V') (e : ↑V' ≤ f ⁻¹ᵁ ↑U'),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U') (↑V') e))

Tactic:
obtain ⟨s, hBs, hBx⟩ := V₂.2.exists_basicOpen_le ⟨x, hx₁⟩ hx₂

Result:
case intro.intro.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
x : ↑↑X.toPresheafedSpace
U₁ : Y.Opens
U₂ : ↑Y.affineOpens
V₁ : X.Opens
V₂ : ↑X.affineOpens
hx₁ : x ∈ V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : (ConcreteCategory.hom f.base) x ∈ U₁.carrier
r : ↑Γ(Y, ↑U₂)
hBr : Y.basicOpen r ≤ U₁
hBfx : ↑⟨(ConcreteCategory.hom f.base) x, hfx₁⟩ ∈ Y.basicOpen r
s : ↑Γ(X, ↑V₂)
hBs : X.basicOpen s ≤ V₁
hBx : ↑⟨x, hx₁⟩ ∈ X.basicOpen s
⊢ ∃ U' V',
    ∃ (_ : ↑U' ≤ U₁) (_ : ↑V' ≤ V₁) (_ : x ∈ ↑V') (e : ↑V' ≤ f ⁻¹ᵁ ↑U'),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U') (↑V') e))

Proof state:
case intro.intro.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
x : ↑↑X.toPresheafedSpace
U₁ : Y.Opens
U₂ : ↑Y.affineOpens
V₁ : X.Opens
V₂ : ↑X.affineOpens
hx₁ : x ∈ V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : (ConcreteCategory.hom f.base) x ∈ U₁.carrier
r : ↑Γ(Y, ↑U₂)
hBr : Y.basicOpen r ≤ U₁
hBfx : ↑⟨(ConcreteCategory.hom f.base) x, hfx₁⟩ ∈ Y.basicOpen r
s : ↑Γ(X, ↑V₂)
hBs : X.basicOpen s ≤ V₁
hBx : ↑⟨x, hx₁⟩ ∈ X.basicOpen s
⊢ ∃ U' V',
    ∃ (_ : ↑U' ≤ U₁) (_ : ↑V' ≤ V₁) (_ : x ∈ ↑V') (e : ↑V' ≤ f ⁻¹ᵁ ↑U'),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U') (↑V') e))

Tactic:
obtain ⟨r', s', hBx', e', hf'⟩ := exists_basicOpen_le_appLE_of_appLE_of_isAffine hPa hPl x
  ⟨Y.basicOpen r, U₂.2.basicOpen _⟩ U₂ ⟨X.basicOpen s, V₂.2.basicOpen _⟩ V₂ hBx hx₂ e₂ h₂ hBfx

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P
x : ↑↑X.toPresheafedSpace
U₁ : Y.Opens
U₂ : ↑Y.affineOpens
V₁ : X.Opens
V₂ : ↑X.affineOpens
hx₁ : x ∈ V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : (ConcreteCategory.hom f.base) x ∈ U₁.carrier
r : ↑Γ(Y, ↑U₂)
hBr : Y.basicOpen r ≤ U₁
hBfx : ↑⟨(ConcreteCategory.hom f.base) x, hfx₁⟩ ∈ Y.basicOpen r
s : ↑Γ(X, ↑V₂)
hBs : X.basicOpen s ≤ V₁
hBx : ↑⟨x, hx₁⟩ ∈ X.basicOpen s
r' : ↑Γ(Y, ↑⟨Y.basicOpen r, ⋯⟩)
s' : ↑Γ(X, ↑⟨X.basicOpen s, ⋯⟩)
hBx' : x ∈ X.basicOpen s'
e' : X.basicOpen s' ≤ f ⁻¹ᵁ Y.basicOpen r'
hf' : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r') (X.basicOpen s') e'))
⊢ ∃ U' V',
    ∃ (_ : ↑U' ≤ U₁) (_ : ↑V' ≤ V₁) (_ : x ∈ ↑V') (e : ↑V' ≤ f ⁻¹ᵁ ↑U'),
      P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U') (↑V') e))