awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
hY : IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
have this₁ : IsAffine X
Tactic: have : IsAffine X := isAffine_of_isAffineHom f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this_1 :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
hY : IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
this : IsAffine X
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
have rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
Tactic: rw [HasRingHomProperty.iff_of_isAffine (P := affineLocally Q)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
h : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
U : Y.Opens
hU : IsAffineOpen U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
have mpr : ∀
  (h :
    ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
  (U : Y.Opens) (hU : IsAffineOpen U), Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Tactic: rw [affineLocally_iff_affineOpens_le] at h
Cleared hypotheses: h, U, hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
h :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
U : Y.Opens
hU : IsAffineOpen U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
have mpr : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry))
Tactic: rw [f.app_eq_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) =
    @IsAffineHom ⊓ affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
have h : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y),
  targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    (@IsAffineHom ⊓ affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
⊢ P (f ≫ g)
have inr : ∀
  (this :
    ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
      {P : MorphismProperty Scheme}
      (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
      (hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y Z : Scheme.{u}}
      (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g))
  (hZ : ¬IsAffine Z), P (f ≫ g)
Tactic: wlog hZ : IsAffine Z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
inr :
  ∀
    (this :
      ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
        {P : MorphismProperty Scheme}
        (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
        (hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y Z : Scheme.{u}}
        (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g))
    (hZ : ¬IsAffine Z), P (f ≫ g)
⊢ P (f ≫ g)
have wlog : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme}
  (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
  (hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y Z : Scheme.{u}}
  (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
Tactic: wlog hZ : IsAffine Z
Cleared hypotheses: P, hA, hQ, X, Y, Z, f, g, hf, hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme}
    (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    (hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
⊢ P (f ≫ g)
have inr : ∀ (i : (↑Z.affineOpens : Type u)), P (X := (↑((f ≫ g) ⁻¹ᵁ (↑i : Z.Opens)) : Scheme)) ((f ≫ g) ∣_ (↑i : Z.Opens))
Tactic: rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme}
    (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    (hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
⊢ P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) ((f ≫ g) ∣_ (↑U : Z.Opens))
have inr : P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens) ≫ g ∣_ (↑U : Z.Opens))
Tactic: rw [morphismRestrict_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
⊢ P (f ≫ g)
have hg₁ : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hZ : IsAffine Z
hg : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g
⊢ P (f ≫ g)
have hY : IsAffine Y
Tactic: obtain ⟨hY, hg⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hZ : IsAffine Z
hg : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g
hY : IsAffine Y
⊢ P (f ≫ g)
have hg₁ : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
Tactic: obtain ⟨hY, hg⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hZ : IsAffine Z
hY : IsAffine Y
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P (f ≫ g)
have hf₁ : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hf
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hZ : IsAffine Z
hY : IsAffine Y
hf : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P (f ≫ g)
have hX : IsAffine X
Tactic: obtain ⟨hX, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hZ : IsAffine Z
hY : IsAffine Y
hf : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine X
⊢ P (f ≫ g)
have hf₁ : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
Tactic: obtain ⟨hX, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hZ : IsAffine Z
hY : IsAffine Y
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ P (f ≫ g)
have rw : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) (f ≫ g)
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ : RingHom.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X : Scheme
⊢ P (𝟙 X)
have rw : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (𝟙 X ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app (𝟙 X) U))
Tactic: rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
      P f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
have simp_rw : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ↔
  ∀ {X Y : Scheme.{u}} (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: simp_rw [isAffineHom_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme.{u}} (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))
have refine_1 : ∀ (h : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)) (X Y : Scheme.{u}) (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, ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
refine_1 :
  ∀ (h : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)) (X Y : Scheme.{u})
    (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))
⊢ HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme.{u}} (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))
have refine_2 : ∀
  (h :
    ∀ {X Y : Scheme.{u}} (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 : Type u} [CommRing R] [CommRing S] ↦ Q)
Tactic: refine ⟨fun h X Y f ↦ ?_, fun h ↦ ⟨affineAnd_isLocal hQi hQl hQs, ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h : HasAffineProperty P (affineAnd fun {R S : Type u} [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))
have refine_1 : (∀ (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: rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme.{u}} (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 : Type u} [CommRing R] [CommRing S] ↦ Q)
have refine_2 : ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y),
  P f ↔ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme.{u}} (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 : Type u} [CommRing R] [CommRing S] ↦ Q) f
have refine_2 : ((∀ (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))
Tactic: rw [targetAffineLocally_affineAnd_iff hQi, h f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
⊢ IsAffineHom f
have inr : ∀
  (this :
    ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
      (P : MorphismProperty Scheme)
      (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)) ⦃X Y : Scheme.{u}⦄
      (f : X ⟶ Y) (hf : P f) (hY : IsAffine Y), IsAffineHom f)
  (hY : ¬IsAffine Y), IsAffineHom f
Tactic: wlog hY : IsAffine Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
inr :
  ∀
    (this :
      ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
        (P : MorphismProperty Scheme)
        (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)) ⦃X Y : Scheme.{u}⦄
        (f : X ⟶ Y) (hf : P f) (hY : IsAffine Y), IsAffineHom f)
    (hY : ¬IsAffine Y), IsAffineHom f
⊢ IsAffineHom f
have wlog : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (P : MorphismProperty Scheme)
  (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)) ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y)
  (hf : P f) (hY : IsAffine Y), IsAffineHom f
Tactic: wlog hY : IsAffine Y
Cleared hypotheses: P, hA, X, Y, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (P : MorphismProperty Scheme)
    (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)) ⦃X Y : Scheme.{u}⦄
    (f : X ⟶ Y) (hf : P f) (hY : IsAffine Y), IsAffineHom f
hY : ¬IsAffine Y
⊢ IsAffineHom f
have inr : ∀ (i : (↑Y.affineOpens : Type u)), IsAffineHom (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))
Tactic: rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsAffineHom) _ (iSup_affineOpens_eq_top _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
hY : IsAffine Y
⊢ IsAffineHom f
have hf₁ : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
hf : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ IsAffineHom f
have rw : IsAffine X
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := @IsAffineHom)]