-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
/-- `affineAnd P` is local if `P` is local on the (algebraic) source. -/
lemma affineAnd_isLocal (hPi : RingHom.RespectsIso Q) (hQl : RingHom.LocalizationAwayPreserves Q)
    (hQs : RingHom.OfLocalizationSpan Q) : (affineAnd Q).IsLocal where
  respectsIso := affineAnd_respectsIso hPi
  to_basicOpen {X Y _} f r := fun ⟨hX, hf⟩ ↦ by
    simp only [Opens.map_top] at hf
    constructor
    · simp only [Scheme.preimage_basicOpen, Opens.map_top]
      exact (isAffineOpen_top X).basicOpen _
    · dsimp only
      rw [morphismRestrict_appTop, CommRingCat.hom_comp, hPi.cancel_right_isIso]
      -- Not sure why the `show` fixes the following `rw` complaining about "motive is incorrect"
      show Q (Scheme.Hom.app f ((Y.basicOpen r).ι ''ᵁ ⊤)).hom
      rw [Scheme.Opens.ι_image_top]
      rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map f (isAffineOpen_top X),
        CommRingCat.hom_comp, hPi.cancel_right_isIso, ← Scheme.Hom.appTop]
      dsimp only [Opens.map_top]
      haveI := (isAffineOpen_top X).isLocalization_basicOpen (f.appTop r)
      apply hQl
      exact hf
  of_basicOpenCover {X Y _} f s hs hf

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf :
  ∀ (r : { x // x ∈ s }),
    IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f

Tactic:
refine ⟨inferInstance, hQs.ofIsLocalization' hPi (f.appTop).hom s hs fun a ↦ ?_⟩

Result:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf :
  ∀ (r : { x // x ∈ s }),
    IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
⊢ ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
    ∃ (x_4 : IsLocalization.Away (↑a) Rᵣ) (x_5 :
      IsLocalization.Away ((CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ↑a) Sᵣ),
      Q (IsLocalization.Away.map Rᵣ Sᵣ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ↑a)

Proof state:
case hs₂.intro.intro
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf :
  ∀ (r : { x // x ∈ s }),
    IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
r : ↑Γ(Y, ⊤)
hr : r ∈ ↑s
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r))

Tactic:
simp_rw [Scheme.preimage_basicOpen] at hf

Result:
case hs₂.intro.intro
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
r : ↑Γ(Y, ⊤)
hr : r ∈ ↑s
hf :
  ∀ (r : { x // x ∈ s }),
    IsAffine ↑(X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) ↑r)) ∧
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r))

Proof state:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf :
  ∀ (r : { x // x ∈ s }),
    IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
⊢ Q
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen ↑a))
      (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) ↑a))) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
      ↑a)

Tactic:
obtain ⟨_, hf⟩ := hf a

Result:
case refine_2.intro
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf✝ :
  ∀ (r : { x // x ∈ s }),
    IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
left✝ : IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑a)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑a)))
⊢ Q
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen ↑a))
      (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) ↑a))) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
      ↑a)

Proof state:
case refine_2.intro
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf✝¹ :
  ∀ (r : { x // x ∈ s }),
    IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
this : IsAffine X
a : ↑↑s
left✝ : IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑a)
hf✝ : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen ↑a).ι ''ᵁ ⊤)))
hf :
  Q
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen ↑a))
            (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) ↑a)))
            (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)) ↑a) ≫
        X.presheaf.map (eqToHom ⋯).op))
⊢ Q
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen ↑a))
      (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) ↑a))) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
      ↑a)

Tactic:
rwa [CommRingCat.hom_comp, hPi.cancel_right_isIso] at hf

Result:
no goals