awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : (↑Y.affineOpens : Type u)),
      IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
        Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
          (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
have refine_1 : ∀
  (hf :
    ∀ (U : (↑Y.affineOpens : Type u)),
      IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
        Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
          (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤))))
  (U : Y.Opens) (hU : IsAffineOpen U), IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Tactic: refine ⟨fun hf U hU ↦ ?_, fun h U ↦ ?_⟩
-- 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
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
refine_1 :
  ∀
    (hf :
      ∀ (U : (↑Y.affineOpens : Type u)),
        IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
          Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
            (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤))))
    (U : Y.Opens) (hU : IsAffineOpen U), IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ (∀ (U : (↑Y.affineOpens : Type u)),
      IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
        Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
          (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
have refine_2 : ∀ (h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U)))
  (U : (↑Y.affineOpens : Type u)),
  IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
    Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
Tactic: refine ⟨fun hf U hU ↦ ?_, fun h U ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf :
  ∀ (U : (↑Y.affineOpens : Type u)),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
      Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
have hfU : IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme)
Tactic: obtain ⟨hfU, hf⟩ := hf ⟨U, hU⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf :
  ∀ (U : (↑Y.affineOpens : Type u)),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
      Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
hfU : IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme)
⊢ IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
have hf₁ : Q (R := (↑Γ((↑(↑⟨U, hU⟩ : Y.Opens) : Scheme), ⊤) : Type u))
  (CommRingCat.Hom.hom
    (Scheme.Hom.app f ((↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤)))
Tactic: obtain ⟨hfU, hf⟩ := hf ⟨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
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf_1 :
  ∀ (U : (↑Y.affineOpens : Type u)),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
      Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
hfU : IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme)
hf :
  Q (R := (↑Γ((↑(↑⟨U, hU⟩ : Y.Opens) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom
      (Scheme.Hom.app f ((↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
have right : ∀
  (hf :
    Q (R := (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤) : Type u))
      (CommRingCat.Hom.hom
        (Scheme.Hom.app f ((↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤)))),
  Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Tactic: have hf : Q (Scheme.Hom.app f (((⟨U, hU⟩ : Y.affineOpens) : Y.Opens).ι ''ᵁ ⊤)).hom := 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
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf_1 :
  ∀ (U : (↑Y.affineOpens : Type u)),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
      Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
hfU : IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Scheme)
hf_2 :
  Q (R := (↑Γ((↑(↑⟨U, hU⟩ : Y.Opens) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom
      (Scheme.Hom.app f ((↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤)))
hf :
  Q (R := (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤) : Type u))
    (CommRingCat.Hom.hom
      (Scheme.Hom.app f ((↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens).ι ''ᵁ ⊤)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
have right : ∀
  (hf :
    Q (R := (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Type u))
      (CommRingCat.Hom.hom
        (Scheme.Hom.app f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)))),
  Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Tactic: rwa [Scheme.Opens.ι_image_top] at hf
Cleared hypotheses: 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
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
⊢ IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
    Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
have refine_2 : Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
Tactic: refine ⟨(h U U.2).1, ?_⟩
-- 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
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
⊢ Q (R := (↑Γ(Y, (↑U : Y.Opens).ι ''ᵁ ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
have refine_2 : Q (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f (↑U : Y.Opens)))
Tactic: rw [Scheme.Opens.ι_image_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
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
have rw : (∀ (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 [targetAffineLocally_affineAnd_iff hQi, isAffineHom_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
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
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    IsAffineHom f ∧ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
have this : HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
  fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Tactic: haveI : HasRingHomProperty (affineLocally Q) Q := ⟨hQ, rfl⟩
-- 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
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    IsAffineHom f ∧ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
have rw : (IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
  IsAffineHom f ∧ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
Tactic: rw [targetAffineLocally_affineAnd_iff' hQ.respectsIso]
-- 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
⊢ (IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    IsAffineHom f ∧ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
have simp : IsAffineHom f →
  ((∀ (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)
Tactic: simp only [and_congr_right_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
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
⊢ (∀ (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 mp : (∀ (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
Tactic: constructor
-- 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
mp :
  (∀ (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
⊢ (∀ (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 mpr : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f →
  ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Tactic: constructor
-- 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
⊢ (∀ (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 mp : ∀
  (this :
    ∀ {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.{u}} (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),
      (∀ (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)
  (hY : ¬IsAffine Y),
  (∀ (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
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
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
mp :
  ∀
    (this :
      ∀ {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.{u}}
        (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),
        (∀ (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)
    (hY : ¬IsAffine Y),
    (∀ (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
⊢ (∀ (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 wlog : ∀ {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.{u}} (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),
  (∀ (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
Tactic: wlog hY : IsAffine Y
Cleared hypotheses: hQ, X, Y, f, this, 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
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
this :
  ∀ {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.{u}} (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),
    (∀ (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
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 mp : ∀ (i : (↑Y.affineOpens : Type u)),
  affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme))
    (f ∣_ (↑i : Y.Opens))
Tactic: rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := affineLocally Q)
        _ (iSup_affineOpens_eq_top _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
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_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
this :
  ∀ {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.{u}} (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),
    (∀ (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
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
⊢ affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme))
    (f ∣_ (↑U : Y.Opens))
have this₁ : IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)
Tactic: have : IsAffine (f ⁻¹ᵁ U) := hf.isAffine_preimage U U.2
-- 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_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
this_2 :
  ∀ {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.{u}} (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),
    (∀ (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
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
this : IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)
⊢ affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme))
    (f ∣_ (↑U : Y.Opens))
have mp : Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
Tactic: rw [HasRingHomProperty.iff_of_isAffine (P := affineLocally Q),
        morphismRestrict_appTop, CommRingCat.hom_comp, hQ.respectsIso.cancel_right_isIso]
-- 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_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
this_2 :
  ∀ {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.{u}} (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),
    (∀ (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
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
this : IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)
⊢ Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))
have mp : IsAffineOpen ((↑U : Y.Opens).ι ''ᵁ ⊤)
Tactic: apply h
-- 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_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
this_2 :
  ∀ {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.{u}} (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),
    (∀ (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
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
this : IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)
⊢ IsAffineOpen ((↑U : Y.Opens).ι ''ᵁ ⊤)
have mp : IsAffineOpen (↑U : Y.Opens)
Tactic: rw [Scheme.Opens.ι_image_top]