-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
/-- A convenience constructor for `HasAffineProperty P (affineAnd Q)`. The `IsAffineHom` is bundled,
since this goes well with defining morphism properties via `extends IsAffineHom`. -/
lemma HasAffineProperty.affineAnd_iff (P : MorphismProperty Scheme.{u})
    (hQi : RingHom.RespectsIso Q) (hQl : RingHom.LocalizationAwayPreserves Q)
    (hQs : RingHom.OfLocalizationSpan Q) :
    HasAffineProperty P (affineAnd Q) ↔
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y), P f ↔
        (IsAffineHom f ∧ ∀ U : Y.Opens, IsAffineOpen U → Q (f.app U).hom)

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
⊢ HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) ↔
    ∀ {X Y : Scheme} (f : X ⟶ Y),
      P f ↔
        (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
          ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
refine ⟨fun h X Y f ↦ ?_, fun h ↦ ⟨affineAnd_isLocal hQi hQl hQs, ?_⟩⟩

Result:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
h : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ P = targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)

Proof state:
case refine_2.h
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f

Tactic:
rw [targetAffineLocally_affineAnd_iff hQi, h f]

Result:
case refine_2.h
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
X Y : Scheme
f : X ⟶ Y
⊢ ((∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
⊢ HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) ↔
    ∀ {X Y : Scheme} (f : X ⟶ Y),
      P f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
simp_rw [isAffineHom_iff]

Result:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
⊢ HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) ↔
    ∀ {X Y : Scheme} (f : X ⟶ Y),
      P f ↔
        (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
          ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Proof state:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
h : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
aesop

Result:
no goals

Proof state:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ P = targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)

Tactic:
ext X Y f

Result:
case refine_2.h
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f