awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V₁ : X.Opens
hV₁ : V₁ ≤ f ⁻¹ᵁ U
V₂ : X.Opens
hV₂ : V₂ ≤ f ⁻¹ᵁ U
a :
  IsAffineOpen V₁ → IsAffineOpen (f ⁻¹ᵁ U ⊓ V₂) → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
a₁ :
  IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
⊢ IsAffineOpen (f ⁻¹ᵁ U ⊓ V₁) → IsAffineOpen (f ⁻¹ᵁ U ⊓ V₂) → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
have a₂ : IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂) ↔ IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
Tactic: rw [inf_eq_right.mpr hV₁, inf_eq_right.mpr hV₂, inf_eq_right.mpr (inf_le_left.trans hV₁)]
-- 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
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
have refine_1 : ∀ {X Y Z : Scheme.{u}} (e : X ≅ Y) (f : Y ⟶ Z),
  (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty f →
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (e.hom ≫ f)
Tactic: refine RespectsIso.mk _ ?_ ?_
-- 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
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
refine_1 :
  ∀ {X Y Z : Scheme.{u}} (e : X ≅ Y) (f : Y ⟶ Z),
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (e.hom ≫ f)
⊢ (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
have refine_2 : ∀ {X Y Z : Scheme.{u}} (e : Y ≅ Z) (f : X ⟶ Y),
  (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty f →
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)
Tactic: refine RespectsIso.mk _ ?_ ?_
-- 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
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
⊢ (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty f →
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (e.hom ≫ f)
have refine_1 : ∀ (hZ : IsAffine Z) (hY : IsAffine Y) (hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))),
  (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (e.hom ≫ f)
Tactic: ⟨hZ, ⟨hY, 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
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
⊢ (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty f →
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)
have refine_2 : ∀ (hZ : IsAffine Y) (hf : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f),
  (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)
Tactic: ⟨hZ, 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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme))
    (f ∣_ Y.basicOpen r)
have left : IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)
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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
left : IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)
⊢ affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme))
    (f ∣_ Y.basicOpen r)
have right : (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (Q : (R →+* S) → Prop)) (↑Γ((↑(Y.basicOpen r) : Scheme), ⊤) : Type u) _
  _ _ (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen r)))
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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)
have left : IsAffine.{u}
  (↑(X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          r)) :
    Scheme)
Tactic: simp only [Scheme.preimage_basicOpen, Opens.map_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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (R := (↑Γ((↑(Y.basicOpen r) : Scheme), ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen r)))
have right : Q (R := (↑Γ((↑(Y.basicOpen r) : Scheme), ⊤) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen r).ι ''ᵁ ⊤)))
Tactic: rw [morphismRestrict_appTop, CommRingCat.hom_comp, hPi.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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (R := (↑Γ(Y, (Y.basicOpen r).ι ''ᵁ ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen r).ι ''ᵁ ⊤)))
have right : Q (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)))
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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)))
have right : Q (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
  (↑(CommRingCat.of
        (↑Γ(X,
              X.basicOpen (U := f ⁻¹ᵁ ⊤)
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (Scheme.Hom.appTop f) :
                    (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                  r)) :
          Type u)) :
    Type u))
  (CommRingCat.Hom.hom
    (CommRingCat.ofHom
      (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
        (↑Γ(X,
              X.basicOpen (U := f ⁻¹ᵁ ⊤)
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (Scheme.Hom.appTop f) :
                    (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                  r)) :
          Type u)
        (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) 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]
-- 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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
    (↑(CommRingCat.of
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ ⊤)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.appTop f) :
                      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                    r)) :
            Type u)) :
      Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ ⊤)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.appTop f) :
                      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) r)))
have right : Q (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
  (↑Γ(X,
        X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r)) :
    Type u))
  (CommRingCat.Hom.hom
    (CommRingCat.ofHom
      (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
        (↑Γ(X,
              X.basicOpen (U := ⊤)
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (Scheme.Hom.appTop f) :
                    (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                  r)) :
          Type u)
        (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) r)))
Tactic: dsimp only [Opens.map_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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
⊢ IsAffine X
have hs₁ : Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
  (Ideal.span
    ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop f)) :
        (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
      (↑s : Set (↑Γ(Y, ⊤) : Type u))))
  ⊤
Tactic: apply isAffine_of_isAffineOpen_basicOpen (f.appTop '' s)
-- 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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
hs₁ :
  Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
        (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    ⊤
⊢ IsAffine X
have hs₂ : ∀ (i : (↑Γ(X, ⊤) : Type u)),
  Membership.mem (γ := Set (↑Γ(X, ⊤) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
        (↑s : Set (↑Γ(Y, ⊤) : Type u)))
      i →
    IsAffineOpen (X.basicOpen i)
Tactic: apply isAffine_of_isAffineOpen_basicOpen (f.appTop '' s)
-- 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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
⊢ Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
        (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    ⊤
have hs₁ : Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
  (Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))))
  (Ideal.map (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤)
Tactic: apply_fun Ideal.map (f.appTop).hom at hs
Cleared hypotheses: hs
-- 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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
hs :
  Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    (Ideal.map (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤)
⊢ Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
        (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    ⊤
have hs₁ : ∀
  (hs :
    Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
      (Ideal.span
        ((⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
          (↑s : Set (↑Γ(Y, ⊤) : Type u))))
      (Ideal.map (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤)),
  Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
        (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    ⊤
Tactic: rwa [Ideal.map_span, Ideal.map_top] at hs
Cleared hypotheses: hs
-- 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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
hs :
  Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    (Ideal.map (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤)
hs₁ :
  ∀
    (hs :
      Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
        (Ideal.span
          ((⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
            (↑s : Set (↑Γ(Y, ⊤) : Type u))))
        (Ideal.map (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤)),
    Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
      (Ideal.span
        ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop f)) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
          (↑s : Set (↑Γ(Y, ⊤) : Type u))))
      ⊤
⊢ Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
        (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    ⊤
have hs₂ : ∀
  (hs :
    Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
      (Ideal.span
        ((⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
          (↑s : Set (↑Γ(Y, ⊤) : Type u))))
      ⊤),
  Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
        (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    ⊤
Tactic: rwa [Ideal.map_span, Ideal.map_top] at hs
Cleared hypotheses: hs
-- 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
hPi : 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
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
r : (↑Γ(Y, ⊤) : Type u)
hr : r ∈ (↑s : Set (↑Γ(Y, ⊤) : Type u))
⊢ IsAffineOpen
    (X.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop f) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
        r))
have hf₁ : ∀ (r : ↥s),
  IsAffine.{u}
      (↑(X.basicOpen (U := f ⁻¹ᵁ ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
              (↑r : (↑Γ(Y, ⊤) : Type u)))) :
        Scheme) ∧
    Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
Tactic: simp_rw [Scheme.preimage_basicOpen] at hf
Cleared hypotheses: hf