-- 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:
case left
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
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ IsAffine ↑(f ⁻¹ᵁ Y.basicOpen r)

Tactic:
simp only [Scheme.preimage_basicOpen, Opens.map_top]

Result:
case left
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
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ IsAffine ↑(X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) r))

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.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)

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

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.app 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 right
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
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)))

Tactic:
rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map f (isAffineOpen_top X),
  CommRingCat.hom_comp, hPi.cancel_right_isIso, ← Scheme.Hom.appTop]

Result:
case right
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
r : ↑Γ(Y, ⊤)
x✝ : affineAnd (fun {R S} [CommRing R] [CommRing S] => Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r))
          (↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r)))
          (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) r)))

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)))
⊢ IsAffine X

Tactic:
apply isAffine_of_isAffineOpen_basicOpen (f.appTop '' s)

Result:
case hs
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)))
⊢ Ideal.span (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) '' ↑s) = ⊤

case hs₂
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)))
⊢ ∀ i ∈ ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) '' ↑s, IsAffineOpen (X.basicOpen i)