awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (hypothesis)
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
inst_3 : LocallyOfFiniteType f
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
this_1 : Field (↑Γ(Spec (CommRingCat.of K), ⊤) : Type u) := IsField.toField ⋯
this : Field (↑Γ(X, ⊤) : Type u) := ⋯.toField
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
have this₁ : Nonempty.{u + 1} ↥(↑U : Scheme)
Tactic: have : Nonempty U := ⟨⟨x, hxU⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Proper (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : IsIntegral X
inst_2 : UniversallyClosed f
inst_3 : LocallyOfFiniteType f
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
this_1 : Field (↑Γ(Spec (CommRingCat.of K), ⊤) : Type u) := IsField.toField ⋯
this_2 : Field (↑Γ(X, ⊤) : Type u) := ⋯.toField
this : Nonempty.{u + 1} ↥(↑U : Scheme)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
have hfg : RingHom.FiniteType (B := (↑Γ(X, U) : Type u))
  (RingHom.comp (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))))
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)))
Tactic: apply RingHom.finite_of_algHom_finiteType_of_isJacobsonRing (A := Γ(X, U))
    (g := (X.presheaf.map (homOfLE le_top).op).hom)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
⊢ QuasiCompact f
have isCompact_preimage : ∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Set ↥Y
h : IsOpen U
hU' : IsCompact U
⊢ IsCompact (X := ↥X) (⇑f ⁻¹' U)
have h : ⇑f ⁻¹' U = (TopCat.Hom.hom (inv f.base)).toFun '' U
Tactic: convert! hU'.image (inv f.base).hom.continuous_toFun using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Set ↥Y
h : IsOpen U
hU' : IsCompact U
⊢ ⇑f ⁻¹' U = (TopCat.Hom.hom (inv f.base)).toFun '' U
have h : Function.LeftInverse (⇑f) (TopCat.Hom.hom (inv f.base)).toFun
Tactic: rw [Set.image_eq_preimage_of_inverse]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Set ↥Y
h_1 : IsOpen U
hU' : IsCompact U
h : Function.LeftInverse (⇑f) (TopCat.Hom.hom (inv f.base)).toFun
⊢ ⇑f ⁻¹' U = (TopCat.Hom.hom (inv f.base)).toFun '' U
have h₁ : Function.RightInverse (⇑f) (TopCat.Hom.hom (inv f.base)).toFun
Tactic: rw [Set.image_eq_preimage_of_inverse]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
⊢ QuasiCompact (f ≫ g)
have isCompact_preimage : ∀ (U : Set ↥Z), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑(f ≫ g) ⁻¹' U)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (X := ↥X) (⇑(f ≫ g) ⁻¹' U)
have isCompact_preimage : IsCompact (X := ↥X) (Set.preimage (β := ↥Y) (⇑f) (⇑g ⁻¹' U))
Tactic: rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.preimage_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (X := ↥X) (Set.preimage (β := ↥Y) (⇑f) (⇑g ⁻¹' U))
have isCompact_preimage : IsOpen (X := ↥Y) (⇑g ⁻¹' U)
Tactic: apply QuasiCompact.isCompact_preimage
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
isCompact_preimage : IsOpen (X := ↥Y) (⇑g ⁻¹' U)
⊢ IsCompact (X := ↥X) (Set.preimage (β := ↥Y) (⇑f) (⇑g ⁻¹' U))
have isCompact_preimage₁ : IsCompact (X := ↥Y) (⇑g ⁻¹' U)
Tactic: apply QuasiCompact.isCompact_preimage
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : Set ↥X
⊢ IsCompact U ∧ IsOpen U ↔ ∃ (s : Set (↑X.affineOpens : Type u)), s.Finite ∧ U = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)
have hb : Opens.IsBasis.{u} (α := ↥X) (Set.range fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens))
Tactic: apply Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion
    (fun (U : X.affineOpens) => (U : X.Opens))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : Set ↥X
hb : Opens.IsBasis.{u} (α := ↥X) (Set.range fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens))
⊢ IsCompact U ∧ IsOpen U ↔ ∃ (s : Set (↑X.affineOpens : Type u)), s.Finite ∧ U = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)
have hb' : ∀ (i : (↑X.affineOpens : Type u)), IsCompact (↑(↑i : X.Opens) : Set ↥X)
Tactic: apply Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion
    (fun (U : X.affineOpens) => (U : X.Opens))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : Set ↥X
⊢ Opens.IsBasis.{u} (α := ↥X) (Set.range fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens))
have hb : Opens.IsBasis X.affineOpens
Tactic: rw [Subtype.range_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
⊢ IsCompact (↑U : Set ↥X) ↔ ∃ (s : Set (↑X.affineOpens : Type u)), s.Finite ∧ U = ⨆ i ∈ s, (↑i : X.Opens)
have h : IsCompact (↑U : Set ↥X) ↔ IsCompact U.carrier ∧ IsOpen U.carrier
Tactic: convert! isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens (U := U.1) using 4 with s
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
h : IsCompact (↑U : Set ↥X) ↔ IsCompact U.carrier ∧ IsOpen U.carrier
⊢ IsCompact (↑U : Set ↥X) ↔ ∃ (s : Set (↑X.affineOpens : Type u)), s.Finite ∧ U = ⨆ i ∈ s, (↑i : X.Opens)
have h₁ : ∀ (s : Set (↑X.affineOpens : Type u)), U = ⨆ i ∈ s, (↑i : X.Opens) ↔ U.carrier = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)
Tactic: convert! isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens (U := U.1) using 4 with s
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑X.affineOpens : Type u)
⊢ U = ⨆ i ∈ s, (↑i : X.Opens) ↔ U.carrier = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)
have h : ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X) = (↑(⨆ i ∈ s, (↑i : X.Opens)) : Set ↥X)
Tactic: convert! SetLike.coe_injective.eq_iff.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ QuasiCompact f ↔ ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)
have rw : (∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)) ↔
  ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)
Tactic: rw [quasiCompact_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)
have refine : (∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)) →
  ∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)
Tactic: refine ⟨fun H U hU => H U U.isOpen hU.isCompact, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)
U : Set ↥Y
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (X := ↥X) (⇑f ⁻¹' U)
have obtain : ∀ (S : Set (↑Y.affineOpens : Type u)) (hS : S.Finite) (hU : IsOpen.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y)))
  (hU' : IsCompact.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y))),
  IsCompact (X := ↥X) (Set.preimage (β := ↥Y) (⇑f) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y)))
Tactic: obtain ⟨S, hS, rfl⟩ := isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens.mp ⟨hU', hU⟩
Cleared hypotheses: U, hU, hU'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)
S : Set (↑Y.affineOpens : Type u)
hS : S.Finite
hU : IsOpen.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y))
hU' : IsCompact.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y))
⊢ IsCompact (X := ↥X) (Set.preimage (β := ↥Y) (⇑f) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y)))
have simp : IsCompact.{u} (X := ↥X) (⋃ i ∈ S, ⇑f ⁻¹' (↑(↑i : Y.Opens) : Set ↥Y))
Tactic: simp only [Set.preimage_iUnion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
⊢ IsCompact (↑(X.basicOpen f) : Set ↥X)
have refine : ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
Tactic: refine isCompact_iff_finite_and_eq_biUnion_affineOpens.mpr ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
⊢ ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
have obtain : ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens)),
  ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
Tactic: obtain ⟨s, hs, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
V : (↑s : Type u_1)
⊢ (↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f ∈ X.affineOpens
have rw : X.basicOpen (U := (↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X.presheaf.map (homOfLE sorry).op) :
        (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, (↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens)) : Type u_1))
      f) ∈
  X.affineOpens
Tactic: rw [← X.basicOpen_res _ (homOfLE ((le_iSup₂ V.1 V.2).trans_eq e.symm)).op]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) :=
  fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯
⊢ ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
have this : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: haveI : Finite s := hs.to_subtype
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) :=
  fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
have refine : X.basicOpen f = ⨆ i ∈ Set.range g, (↑i : X.Opens)
Tactic: refine ⟨Set.range g, Set.finite_range g, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) :=
  fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ X.basicOpen f = ⨆ i ∈ Set.range g, (↑i : X.Opens)
have rw : X.basicOpen f = ⨆ (i : (↑s : Type u_1)), (↑(g i) : X.Opens)
Tactic: rw [iSup_range, ← iSup_inf_eq, iSup_subtype, ← e, inf_eq_right.mpr (X.basicOpen_le f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) :=
  fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯
this : Finite.{u_1 + 1} (↑s : Type u_1)
rw : X.basicOpen f = ⨆ (i : (↑s : Type u_1)), (↑(g i) : X.Opens)
⊢ X.basicOpen f = ⨆ i ∈ Set.range g, (↑i : X.Opens)
have rw₁ : X.basicOpen f = (⨆ (i : (↑s : Type u_1)), (↑(↑i : (↑X.affineOpens : Type u_1)) : X.Opens)) ⊓ X.basicOpen f
Tactic: rw [iSup_range, ← iSup_inf_eq, iSup_subtype, ← e, inf_eq_right.mpr (X.basicOpen_le f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) :=
  fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯
this : Finite.{u_1 + 1} (↑s : Type u_1)
rw : X.basicOpen f = ⨆ (i : (↑s : Type u_1)), (↑(g i) : X.Opens)
rw₁ : X.basicOpen f = (⨆ (i : (↑s : Type u_1)), (↑(↑i : (↑X.affineOpens : Type u_1)) : X.Opens)) ⊓ X.basicOpen f
⊢ X.basicOpen f = ⨆ i ∈ Set.range g, (↑i : X.Opens)
have rw₂ : X.basicOpen f =
  (⨆ (i : (↑X.affineOpens : Type u_1)),
      ⨆ (h : i ∈ s),
        (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u_1)) ↦ x ∈ s) i h) : (↑X.affineOpens : Type u_1)) :
          X.Opens)) ⊓
    X.basicOpen f
Tactic: rw [iSup_range, ← iSup_inf_eq, iSup_subtype, ← e, inf_eq_right.mpr (X.basicOpen_le f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) :=
  fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯
this : Finite.{u_1 + 1} (↑s : Type u_1)
rw : X.basicOpen f = ⨆ (i : (↑s : Type u_1)), (↑(g i) : X.Opens)
rw₁ : X.basicOpen f = (⨆ (i : (↑s : Type u_1)), (↑(↑i : (↑X.affineOpens : Type u_1)) : X.Opens)) ⊓ X.basicOpen f
rw₂ :
  X.basicOpen f =
    (⨆ (i : (↑X.affineOpens : Type u_1)),
        ⨆ (h : i ∈ s),
          (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u_1)) ↦ x ∈ s) i h) : (↑X.affineOpens : Type u_1)) :
            X.Opens)) ⊓
      X.basicOpen f
⊢ X.basicOpen f = ⨆ i ∈ Set.range g, (↑i : X.Opens)
have rw₃ : X.basicOpen f = U ⊓ X.basicOpen f
Tactic: rw [iSup_range, ← iSup_inf_eq, iSup_subtype, ← e, inf_eq_right.mpr (X.basicOpen_le f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) :=
  fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯
this : Finite.{u_1 + 1} (↑s : Type u_1)
rw : X.basicOpen f = ⨆ (i : (↑s : Type u_1)), (↑(g i) : X.Opens)
rw₁ : X.basicOpen f = (⨆ (i : (↑s : Type u_1)), (↑(↑i : (↑X.affineOpens : Type u_1)) : X.Opens)) ⊓ X.basicOpen f
rw₂ :
  X.basicOpen f =
    (⨆ (i : (↑X.affineOpens : Type u_1)),
        ⨆ (h : i ∈ s),
          (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u_1)) ↦ x ∈ s) i h) : (↑X.affineOpens : Type u_1)) :
            X.Opens)) ⊓
      X.basicOpen f
rw₃ : X.basicOpen f = U ⊓ X.basicOpen f
⊢ X.basicOpen f = ⨆ i ∈ Set.range g, (↑i : X.Opens)
have rw₄ : X.basicOpen f = X.basicOpen f
Tactic: rw [iSup_range, ← iSup_inf_eq, iSup_subtype, ← e, inf_eq_right.mpr (X.basicOpen_le f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
⊢ IsCompact (↑(X.basicOpen f) : Set ↥X)
have refine : ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
Tactic: classical
  refine isCompact_iff_finite_and_eq_biUnion_affineOpens.mpr ?_
  obtain ⟨s, hs, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hU
  let g : s → X.affineOpens := fun V ↦ ⟨V.1 ⊓ X.basicOpen f, by
    rw [← X.basicOpen_res _ (homOfLE ((le_iSup₂ V.1 V.2).trans_eq e.symm)).op]
    exact V.1.2.basicOpen _⟩
  haveI : Finite s := hs.to_subtype
  refine ⟨Set.range g, Set.finite_range g, ?_⟩
  rw [iSup_range, ← iSup_inf_eq, iSup_subtype, ← e, inf_eq_right.mpr (X.basicOpen_le f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
refine : ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
⊢ IsCompact (↑(X.basicOpen f) : Set ↥X)
have refine₁ : ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens)),
  ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
Tactic: classical
  refine isCompact_iff_finite_and_eq_biUnion_affineOpens.mpr ?_
  obtain ⟨s, hs, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hU
  let g : s → X.affineOpens := fun V ↦ ⟨V.1 ⊓ X.basicOpen f, by
    rw [← X.basicOpen_res _ (homOfLE ((le_iSup₂ V.1 V.2).trans_eq e.symm)).op]
    exact V.1.2.basicOpen _⟩
  haveI : Finite s := hs.to_subtype
  refine ⟨Set.range g, Set.finite_range g, ?_⟩
  rw [iSup_range, ← iSup_inf_eq, iSup_subtype, ← e, inf_eq_right.mpr (X.basicOpen_le f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
refine : ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
refine₁ :
  ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens)),
    ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
refine₂ :
  ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens)),
    ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
⊢ IsCompact (↑(X.basicOpen f) : Set ↥X)
have refine₃ : ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens))
  (this : Finite.{u_1 + 1} (↑s : Type u_1)),
  ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
Tactic: classical
  refine isCompact_iff_finite_and_eq_biUnion_affineOpens.mpr ?_
  obtain ⟨s, hs, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hU
  let g : s → X.affineOpens := fun V ↦ ⟨V.1 ⊓ X.basicOpen f, by
    rw [← X.basicOpen_res _ (homOfLE ((le_iSup₂ V.1 V.2).trans_eq e.symm)).op]
    exact V.1.2.basicOpen _⟩
  haveI : Finite s := hs.to_subtype
  refine ⟨Set.range g, Set.finite_range g, ?_⟩
  rw [iSup_range, ← iSup_inf_eq, iSup_subtype, ← e, inf_eq_right.mpr (X.basicOpen_le f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
refine : ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
refine₁ :
  ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens)),
    ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
refine₂ :
  ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens)),
    ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
refine₃ :
  ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens))
    (this : Finite.{u_1 + 1} (↑s : Type u_1)),
    ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
⊢ IsCompact (↑(X.basicOpen f) : Set ↥X)
have refine₄ : ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens)),
  let g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) := fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) sorry;
  ∀ (this : Finite.{u_1 + 1} (↑s : Type u_1)), X.basicOpen f = ⨆ i ∈ Set.range g, (↑i : X.Opens)
Tactic: classical
  refine isCompact_iff_finite_and_eq_biUnion_affineOpens.mpr ?_
  obtain ⟨s, hs, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hU
  let g : s → X.affineOpens := fun V ↦ ⟨V.1 ⊓ X.basicOpen f, by
    rw [← X.basicOpen_res _ (homOfLE ((le_iSup₂ V.1 V.2).trans_eq e.symm)).op]
    exact V.1.2.basicOpen _⟩
  haveI : Finite s := hs.to_subtype
  refine ⟨Set.range g, Set.finite_range g, ?_⟩
  rw [iSup_range, ← iSup_inf_eq, iSup_subtype, ← e, inf_eq_right.mpr (X.basicOpen_le f)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    CompactSpace.{u_1} ↥X
have respectsIso : (AffineTargetMorphismProperty.toProperty fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    CompactSpace.{u_1} ↥X).RespectsIso
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
respectsIso :
  (AffineTargetMorphismProperty.toProperty fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
      CompactSpace.{u_1} ↥X).RespectsIso
⊢ AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    CompactSpace.{u_1} ↥X
have to_basicOpen : ∀ {X Y : Scheme.{u_1}} [IsAffine Y] (f : X ⟶ Y) (r : (↑Γ(Y, ⊤) : Type u_1)),
  CompactSpace.{u_1} ↥X → CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
respectsIso :
  (AffineTargetMorphismProperty.toProperty fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
      CompactSpace.{u_1} ↥X).RespectsIso
to_basicOpen :
  ∀ {X Y : Scheme.{u_1}} [IsAffine Y] (f : X ⟶ Y) (r : (↑Γ(Y, ⊤) : Type u_1)),
    CompactSpace.{u_1} ↥X → CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)
⊢ AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    CompactSpace.{u_1} ↥X
have of_basicOpenCover : ∀ {X Y : Scheme.{u_1}} [IsAffine Y] (f : X ⟶ Y) (s : Finset (↑Γ(Y, ⊤) : Type u_1)),
  Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤ →
    (∀ (r : ↥s), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)) →
      CompactSpace.{u_1} ↥X
Tactic: constructor