awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
h : t' ∉ ⇑fT '' Z
⊢ ∀ (a : ↥X), ∃ (i : 𝒰.I₀) (_ : i ∈ σ), a ∈ (U i).carrier
have contrapose! : ∀ (h : ∃ (a : ↥X), ∀ (i : 𝒰.I₀) (j : i ∈ σ), a ∉ (U i).carrier), Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
h : ∃ (a : ↥X), ∀ (i : 𝒰.I₀) (j : i ∈ σ), a ∉ (U i).carrier
⊢ Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'
have obtain : ∀ (x : ↥X) (hx : ∀ (i : 𝒰.I₀) (j : i ∈ σ), x ∉ (U i).carrier), Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'
Tactic: obtain ⟨x, hx⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
x : ↥X
hx : ∀ (i : 𝒰.I₀) (j : i ∈ σ), x ∉ (U i).carrier
⊢ Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'
have obtain : ∀ (z : ↥(pullback f q)) (hzr : (pullback.snd f q) z = t')
  (hx : ∀ (i : 𝒰.I₀) (j : i ∈ σ), ((pullback.fst f q) z : ↥X) ∉ (U i).carrier),
  Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'
Tactic: obtain ⟨z, rfl, hzr⟩ := exists_preimage_pullback x t' (Subsingleton.elim (f x) (q t'))
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ (i : 𝒰.I₀) (j : i ∈ σ), ((pullback.fst f q) z : ↥X) ∉ (U i).carrier
⊢ Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'
have suffices : ∀ (i : 𝒰.I₀),
  Membership.mem (γ := Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
      ((Opens.comap
              { toFun := comap φ, continuous_toFun := sorry :
                C(PrimeSpectrum (MvPolynomial 𝒰.I₀ K), PrimeSpectrum (MvPolynomial 𝒰.I₀ K)) } :
            (a : Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K))) → Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
          (Ti i) :
        Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
      t →
    (p z : ↥X) ∉ U i
Tactic: suffices ∀ i, t ∈ (Ti i).comap ⟨_, continuous_comap φ⟩ → p z ∉ U i from
    ⟨z, by simpa [Z, p, fT, hzr], hzr⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (hypothesis)
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ (i : 𝒰.I₀) (j : i ∈ σ), ((pullback.fst f q) z : ↥X) ∉ (U i).carrier
i : 𝒰.I₀
hi₁ :
  Membership.mem (γ := Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
    ((Opens.comap
            { toFun := comap φ, continuous_toFun := ⋯ :
              C(PrimeSpectrum (MvPolynomial 𝒰.I₀ K), PrimeSpectrum (MvPolynomial 𝒰.I₀ K)) } :
          (a : Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K))) → Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
        (Ti i) :
      Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
    t
hi₂ : Membership.mem (α := ↥X) (U i) (p z : ↥X)
⊢ False
have hi₃ : Membership.mem (γ := Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K))) ⊥ t
Tactic: rw [comap_basicOpen, show φ (.X i) = 0 by simpa [φ] using (hx i · hi₂), basicOpen_zero] at hi₁
Cleared hypotheses: hi₁, hi₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
let let₁ let₂ let₃ let₄ let₅ let₆ let₇ let₈ let₉ : CompactSpace.{u} ↥X
⊢ CompactSpace.{u} ↥X
have let₁₀ : let 𝒰 := X.affineCover;
let U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i);
let T := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K));
let q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C);
let Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i);
let fT : pullback f q ⟶ T := pullback.snd f q;
let p : pullback f q ⟶ X := pullback.fst f q;
let Z := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ;
∀ (hZ : IsClosed Z), CompactSpace.{u} ↥X
Tactic: classical
  let 𝒰 : X.OpenCover := X.affineCover
  let U (i : 𝒰.I₀) : X.Opens := (𝒰.f i).opensRange
  let T : Scheme := Spec (.of <| MvPolynomial 𝒰.I₀ K)
  let q : T ⟶ Spec (.of K) := Spec.map (CommRingCat.ofHom MvPolynomial.C)
  let Ti (i : 𝒰.I₀) : T.Opens := basicOpen (MvPolynomial.X i)
  let fT : pullback f q ⟶ T := pullback.snd f q
  let p : pullback f q ⟶ X := pullback.fst f q
  let Z : Set (pullback f q :) := (⨆ i, fT ⁻¹ᵁ (Ti i) ⊓ p ⁻¹ᵁ (U i) : (pullback f q).Opens)ᶜ
  have hZ : IsClosed Z := by
    simp only [Z, isClosed_compl_iff, Opens.coe_iSup, Opens.coe_inf, Opens.map_coe]
    exact isOpen_iUnion fun i ↦ (fT.continuous.1 _ (Ti i).2).inter (p.continuous.1 _ (U i).2)
  let Zc : T.Opens := ⟨(fT '' Z)ᶜ, (fT.isClosedMap _ hZ).isOpen_compl⟩
  let ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := MvPolynomial.aeval (fun _ ↦ 1)
  let t : T := Spec.map (CommRingCat.ofHom ψ.toRingHom) default
  have ht (i : 𝒰.I₀) : t ∈ Ti i := show ψ (.X i) ≠ 0 by simp [ψ]
  have htZc : t ∈ Zc := by
    intro ⟨z, hz, hzt⟩
    suffices ∃ i, fT z ∈ Ti i ∧ p z ∈ U i from hz (by simpa)
    exact ⟨𝒰.idx (p z), hzt ▸ ht _, by simpa [U] using 𝒰.covers (p z)⟩
  obtain ⟨U', ⟨g, rfl⟩, htU', hU'le⟩ := Opens.isBasis_iff_nbhd.mp isBasis_basic_opens htZc
  let σ : Finset 𝒰.I₀ := MvPolynomial.vars g
  let φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
    (MvPolynomial.aeval fun i : 𝒰.I₀ ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
  let t' : T := Spec.map (CommRingCat.ofHom φ) t
  have ht'g : t' ∈ PrimeSpectrum.basicOpen g :=
    show φ g ∉ t.asIdeal from (show φ g = g from aeval_ite_mem_eq_self g subset_rfl).symm ▸ htU'
  have h : t' ∉ fT '' Z := hU'le ht'g
  suffices ⋃ i ∈ σ, (U i).1 = Set.univ from
    ⟨this ▸ Finset.isCompact_biUnion _ fun i _ ↦ isCompact_range (𝒰.f i).continuous⟩
  rw [Set.iUnion₂_eq_univ_iff]
  contrapose! h
  obtain ⟨x, hx⟩ := h
  obtain ⟨z, rfl, hzr⟩ := exists_preimage_pullback x t' (Subsingleton.elim (f x) (q t'))
  suffices ∀ i, t ∈ (Ti i).comap ⟨_, continuous_comap φ⟩ → p z ∉ U i from
    ⟨z, by simpa [Z, p, fT, hzr], hzr⟩
  intro i hi₁ hi₂
  rw [comap_basicOpen, show φ (.X i) = 0 by simpa [φ] using (hx i · hi₂), basicOpen_zero] at hi₁
  cases hi₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
⊢ IsProperMap (X := ↥X) (Y := ↥Y) ⇑f
have rw : Continuous (X := ↥X) (Y := ↥Y) ⇑f ∧
  IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f ∧ ∀ (y : ↥Y), IsCompact (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
Tactic: rw [isProperMap_iff_isClosedMap_and_compact_fibers]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
⊢ Continuous (X := ↥X) (Y := ↥Y) ⇑f ∧
    IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f ∧ ∀ (y : ↥Y), IsCompact (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
have refine : ∀ (y : ↥Y), IsCompact (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
Tactic: refine ⟨f.continuous, f.isClosedMap, fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
y : ↥Y
⊢ IsCompact (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
have this : CompactSpace.{u} ↥(pullback f (Y.fromSpecResidueField y))
Tactic: have := compactSpace_of_universallyClosed (pullback.snd f (Y.fromSpecResidueField y))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
y : ↥Y
this : CompactSpace.{u} ↥(pullback f (Y.fromSpecResidueField y))
⊢ IsCompact (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
have rw : IsCompact (X := ↥X)
  (Set.range (ι := ↥(pullback f (Y.fromSpecResidueField y))) ⇑(pullback.fst f (Y.fromSpecResidueField y)))
Tactic: rw [← Scheme.range_fromSpecResidueField, ← Scheme.Pullback.range_fst]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
⊢ @UniversallyClosed = (topologically @SpecializingMap).universally ⊓ @QuasiCompact
have rw : @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally
Tactic: rw [← universally_eq_iff (P := @QuasiCompact).mpr inferInstance, ← universally_inf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
⊢ @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally
have a : @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
a : @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally
⊢ @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally
have a₁ : (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ @UniversallyClosed
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
⊢ @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally
have a : universally @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally
Tactic: rw [← universally_eq_iff (P := @UniversallyClosed).mpr inferInstance]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ @UniversallyClosed
have a : (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ (topologically @IsClosedMap).universally
Tactic: rw [universallyClosed_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsDominant f
⊢ Surjective f
have rw : Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
Tactic: rw [surjective_iff, ← Set.range_eq_univ, ← f.denseRange.closure_range,
    f.isClosedMap.isClosed_range.closure_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsDominant f
rw : Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
⊢ Surjective f
have rw₁ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) Set.univ
Tactic: rw [surjective_iff, ← Set.range_eq_univ, ← f.denseRange.closure_range,
    f.isClosedMap.isClosed_range.closure_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsDominant f
rw : Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
rw₁ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) Set.univ
⊢ Surjective f
have rw₂ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (closure (Set.range (ι := ↥X) ⇑f))
Tactic: rw [surjective_iff, ← Set.range_eq_univ, ← f.denseRange.closure_range,
    f.isClosedMap.isClosed_range.closure_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsDominant f
rw : Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
rw₁ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) Set.univ
rw₂ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (closure (Set.range (ι := ↥X) ⇑f))
⊢ Surjective f
have rw₃ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥X) ⇑f)
Tactic: rw [surjective_iff, ← Set.range_eq_univ, ← f.denseRange.closure_range,
    f.isClosedMap.isClosed_range.closure_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
⊢ @UniversallyInjective =
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally
have h : ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y),
  UniversallyInjective f ↔
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally
      f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyInjective f ↔
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally
      f
have h : (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally f ↔
  (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally f
Tactic: rw [universallyInjective_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
⊢ @UniversallyInjective = diagonal @Surjective
have a : @UniversallyInjective ≤ diagonal @Surjective
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
a : @UniversallyInjective ≤ diagonal @Surjective
⊢ @UniversallyInjective = diagonal @Surjective
have a₁ : diagonal @Surjective ≤ @UniversallyInjective
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
⊢ diagonal (@Surjective) f
have a : ∀ (x : ↥(pullback.diagonalObj f)),
  Eq (α := ↥X) ((pullback.fst f f) ((pullback.diagonal f) ((pullback.fst f f) x : ↥X) : ↥(pullback.diagonalObj f)) : ↥X)
    ((pullback.fst f f) x : ↥X)
Tactic: refine ⟨fun x ↦ ⟨pullback.fst f f x, hf.1 _ _ _ (IsPullback.of_hasPullback f f) ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
x : ↥(pullback.diagonalObj f)
⊢ Eq (α := ↥X) ((pullback.fst f f) ((pullback.diagonal f) ((pullback.fst f f) x : ↥X) : ↥(pullback.diagonalObj f)) : ↥X)
    ((pullback.fst f f) x : ↥X)
have a : Eq (α := ↥X) ((𝟙 X) ((pullback.fst f f) x : ↥X) : ↥X) ((pullback.fst f f) x : ↥X)
Tactic: rw [← Scheme.Hom.comp_apply, pullback.diagonal_fst]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
⊢ diagonal @Surjective ≤ @UniversallyInjective
have a : (diagonal @Surjective).universally ≤
  (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally
Tactic: rw [← universally_eq_iff.mpr (inferInstance : IsStableUnderBaseChange (diagonal @Surjective)),
      universallyInjective_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
⊢ (diagonal @Surjective).universally ≤
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally
have a : diagonal @Surjective ≤
  topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x
Tactic: apply universally_mono
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : Eq (α := ↥Y) (f x₁ : ↥Y) (f x₂ : ↥Y)
⊢ x₁ = x₂
have a : ∀ (t : ↥(pullback f f)) (ht₁ : (pullback.fst f f) t = x₁) (ht₂ : (pullback.snd f f) t = x₂), x₁ = x₂
Tactic: obtain ⟨t, ht₁, ht₂⟩ := Scheme.Pullback.exists_preimage_pullback _ _ e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : Eq (α := ↥Y) (f x₁ : ↥Y) (f x₂ : ↥Y)
t : ↥(pullback f f)
ht₁ : (pullback.fst f f) t = x₁
ht₂ : (pullback.snd f f) t = x₂
⊢ x₁ = x₂
have a : ∀ (t : ↥X) (ht₁ : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₁)
  (ht₂ : (pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂), x₁ = x₂
Tactic: obtain ⟨t, rfl⟩ := hf.1 t
Cleared hypotheses: t, ht₁, ht₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : Eq (α := ↥Y) (f x₁ : ↥Y) (f x₂ : ↥Y)
t : ↥X
ht₁ : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₁
ht₂ : (pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
⊢ x₁ = x₂
have a : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
Tactic: rw [← ht₁, ← ht₂, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.diagonal_fst,
      pullback.diagonal_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : Eq (α := ↥Y) (f x₁ : ↥Y) (f x₂ : ↥Y)
t : ↥X
ht₁ : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₁
ht₂ : (pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
a : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
⊢ x₁ = x₂
have a₁ : Eq (α := ↥X) ((pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
  ((pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
Tactic: rw [← ht₁, ← ht₂, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.diagonal_fst,
      pullback.diagonal_snd]