awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
trans :
  Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)) ⊆
    (Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier
⊢ Subset (α := Set (PrimeSpectrum ((i : ι) → (↑(R i) : Type u))))
    (Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)))
    (zeroLocus t)ᶜ
have trans₁ : (Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier ⊆ (zeroLocus t)ᶜ
Tactic: trans (Sigma.ι _ i ≫ sigmaSpec R).opensRange.1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)) ⊆
    (Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier
have simp : Subset.{u} (α := Set (PrimeSpectrum ((i : ι) → (↑(R i) : Type u))))
  (Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)))
  (Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)))
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ (Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier ⊆ (zeroLocus t)ᶜ
have rw : (sigmaSpec R ''ᵁ Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i)).carrier ⊆ (zeroLocus t)ᶜ
Tactic: rw [Scheme.Hom.opensRange_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (hypothesis)
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
⊢ U = ⊤
have this : ∀ (i : ι),
  Eq (α := Ideal (↑(R i) : Type u))
    (Ideal.span
      ((⇑(Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i) :
          (a : (i : ι) → (↑(R i) : Type u)) → (↑(R i) : Type u)) ''
        t))
    ⊤
Tactic: have (i : _) : Ideal.span (Pi.evalRingHom (R ·) i '' t) = ⊤ := by
    rw [← zeroLocus_empty_iff_eq_top, zeroLocus_span, ← preimage_comap_zeroLocus,
      ← Set.compl_univ_iff, ← Set.preimage_compl, Set.preimage_eq_univ_iff]
    trans (Sigma.ι _ i ≫ sigmaSpec R).opensRange.1
    · simp; rfl
    · rw [Scheme.Hom.opensRange_comp]
      exact (Set.image_subset_range _ _).trans (hV.trans ht')
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (hypothesis)
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
this :
  ∀ (i : ι),
    Eq (α := Ideal (↑(R i) : Type u))
      (Ideal.span
        ((⇑(Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i) :
            (a : (i : ι) → (↑(R i) : Type u)) → (↑(R i) : Type u)) ''
          t))
      ⊤
⊢ U = ⊤
have this₁ : Eq (α := Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) (Ideal.span s) ⊤
Tactic: have : Ideal.span s = ⊤ := top_le_iff.mp
    ((Ideal.span_eq_top_of_span_image_evalRingHom _ ht this).ge.trans (Ideal.span_mono hts))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → (↑(R i) : Type u))
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → (↑(R i) : Type u)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
⊢ I = ⊥
have refine : ∀ (x : (i : ι) → (↑(R i) : Type u)) (hx : x ∈ I),
  Membership.mem (γ := Submodule ((i : ι) → (↑(R i) : Type u)) ((i : ι) → (↑(R i) : Type u))) ⊥ x
Tactic: refine le_bot_iff.mp fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → (↑(R i) : Type u))
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → (↑(R i) : Type u)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
x : (i : ι) → (↑(R i) : Type u)
hx : x ∈ I
⊢ Membership.mem (γ := Submodule ((i : ι) → (↑(R i) : Type u)) ((i : ι) → (↑(R i) : Type u))) ⊥ x
have h : ∀ (i : ι), x i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
⊢ Scheme.Hom.coborderRange g = ⊤
have hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆
  Set.range (ι := ↥V) ⇑g
Tactic: apply eq_top_of_sigmaSpec_subset_of_isCompact (hVU := subset_coborder)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
hV :
  (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆
    Set.range (ι := ↥V) ⇑g
⊢ Scheme.Hom.coborderRange g = ⊤
have hV' : IsCompact (X := ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) (Set.range (ι := ↥V) ⇑g)
Tactic: apply eq_top_of_sigmaSpec_subset_of_isCompact (hVU := subset_coborder)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (hypothesis)
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
⊢ IsIso g
have this : Scheme.Hom.coborderRange g = ⊤
Tactic: have : g.coborderRange = ⊤ := by
    apply eq_top_of_sigmaSpec_subset_of_isCompact (hVU := subset_coborder)
    · simpa only [← hU'] using Set.range_comp_subset_range f g
    · exact isCompact_range g.continuous
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
⊢ IsIso (Scheme.Hom.coborderRange g).ι
have rw : IsIso.{u, u + 1} (X := (↑⊤ : Scheme)) (Iso.hom (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).topIso)
Tactic: rw [this, ← Scheme.topIso_hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (hypothesis)
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
⊢ IsClosedImmersion g
have this₁ : IsIso (Scheme.Hom.coborderRange g).ι
Tactic: have : IsIso g.coborderRange.ι := by rw [this, ← Scheme.topIso_hom]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
this_1 : Scheme.Hom.coborderRange g = ⊤
this : IsIso (Scheme.Hom.coborderRange g).ι
⊢ IsClosedImmersion g
have rw : IsClosedImmersion (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)
Tactic: rw [← g.liftCoborder_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
inst : IsImmersion g
inst_1 : CompactSpace.{u} ↥V
hU' : f ≫ g = sigmaSpec R
this_1 : Scheme.Hom.coborderRange g = ⊤
this : IsClosedImmersion g
⊢ IsIso g
have obtain : ∀ (I : Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u))
  (e : V ≅ Spec (CommRingCat.of ((↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u) ⧸ I)))
  [inst : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))]
  (hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R)
  (this : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ⊤)
  (this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))),
  IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
Tactic: obtain ⟨I, e, rfl⟩ := IsClosedImmersion.Spec_iff.mp this
Cleared hypotheses: g, inst, hU', this_1, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
inst : CompactSpace.{u} ↥V
I : Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
e : V ≅ Spec (CommRingCat.of ((↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u) ⧸ I))
inst_1 : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
this_1 : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
⊢ IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
have obtain : ∀
  (e :
    V ≅
      Spec
        (CommRingCat.of
          (HasQuotient.Quotient (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u) (B :=
            Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) ⊥)))
  [inst : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))]
  (hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R)
  (this : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤)
  (this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))),
  IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
Tactic: obtain rfl := eq_bot_of_comp_quotientMk_eq_sigmaSpec R I (f ≫ e.hom) (by rwa [Category.assoc])
Cleared hypotheses: I, e, inst_1, hU', this_1, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun (i : ι) ↦ Spec (R i)) ⟶ V
inst : CompactSpace.{u} ↥V
e :
  V ≅
    Spec
      (CommRingCat.of
        (HasQuotient.Quotient (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u) (B :=
          Ideal (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) ⊥))
inst_1 : IsImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
hU' : f ≫ e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)) = sigmaSpec R
this_1 : Scheme.Hom.coborderRange (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥))) = ⊤
this : IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
⊢ IsIso (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ⊥)))
have convert_to : IsIso (Y := Spec (CommRingCat.of (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)))
  (e.hom ≫
    Spec.map
      (Iso.inv
        (RingEquiv.toCommRingCatIso
          (RingEquiv.quotientBot (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)))))
Tactic: convert_to IsIso (e.hom ≫ Spec.map (RingEquiv.quotientBot _).toCommRingCatIso.inv)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : QuasiSeparatedSpace.{u} ↥X
f g : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X
e : pointsPi R X f = pointsPi R X g
⊢ sigmaSpec R ≫ f = sigmaSpec R ≫ g
have h : ∀ (i : ι),
  Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R ≫ f =
    Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R ≫ g
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (hypothesis)
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : QuasiSeparatedSpace.{u} ↥X
f g : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X
e : pointsPi R X f = pointsPi R X g
⊢ f = g
have this : IsIso (X := equalizer f g) (equalizer.ι f g)
Tactic: have := isIso_of_comp_eq_sigmaSpec R (V := equalizer f g)
    (equalizer.lift (sigmaSpec R) (by ext1 i; simpa using congr_fun e i))
    (equalizer.ι f g) (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : QuasiSeparatedSpace.{u} ↥X
f g : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X
e : pointsPi R X f = pointsPi R X g
this : IsIso (X := equalizer f g) (equalizer.ι f g)
⊢ f = g
have rw : Eq (α := equalizer f g ⟶ X) (equalizer.ι f g ≫ f) (equalizer.ι f g ≫ g)
Tactic: rw [← cancel_epi (equalizer.ι f g), equalizer.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : QuasiSeparatedSpace.{u} ↥X
f g : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X
e : pointsPi R X f = pointsPi R X g
this : IsIso (X := equalizer f g) (equalizer.ι f g)
rw : Eq (α := equalizer f g ⟶ X) (equalizer.ι f g ≫ f) (equalizer.ι f g ≫ g)
⊢ f = g
have rw₁ : Eq (α := equalizer f g ⟶ X) (equalizer.ι f g ≫ g) (equalizer.ι f g ≫ g)
Tactic: rw [← cancel_epi (equalizer.ι f g), equalizer.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
⊢ ∃ (a : Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))) ⟶ X), pointsPi R X a = f
have refine : pointsPi R X
    (Spec.map
        (CommRingCat.ofHom
          (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦
            (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫
      X.isoSpec.inv) =
  f
Tactic: refine ⟨Spec.map (CommRingCat.ofHom
    (Pi.ringHom fun i ↦ (Spec.preimage (f i ≫ X.isoSpec.hom)).1)) ≫ X.isoSpec.inv, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
⊢ pointsPi R X
      (Spec.map
          (CommRingCat.ofHom
            (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦
              (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫
        X.isoSpec.inv) =
    f
have h : ∀ (i : ι),
  pointsPi R X
      (Spec.map
          (CommRingCat.ofHom
            (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦
              (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫
        X.isoSpec.inv)
      i =
    f i
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
i : ι
⊢ pointsPi R X
      (Spec.map
          (CommRingCat.ofHom
            (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦
              (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫
        X.isoSpec.inv)
      i =
    f i
have h : Spec.map
    (CategoryStruct.comp (Y := CommRingCat.of ((i : ι) → (↑(R i) : Type u)))
      (CommRingCat.ofHom
        (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦ (Spec.preimage (f i ≫ X.isoSpec.hom)).hom'))
      (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i))) =
  f i ≫ X.isoSpec.hom
Tactic: simp only [pointsPi, ← Spec.map_comp_assoc, Iso.comp_inv_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ TopologicalSpace.IsTopologicalBasis
    (Set.image (α := TopologicalSpace.Opens ↥(Proj 𝒜)) SetLike.coe (Set.range (basicOpen 𝒜)))
have h : ↥(Proj 𝒜) = ProjectiveSpectrum 𝒜 →
  Set.image (α := TopologicalSpace.Opens ↥(Proj 𝒜)) SetLike.coe (Set.range (basicOpen 𝒜)) =
    Set.range fun (r : A) ↦ (↑(ProjectiveSpectrum.basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))
Tactic: convert! ProjectiveSpectrum.isTopologicalBasis_basic_opens 𝒜
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
⊢ Eq.{u + 1} (α := (Proj 𝒜).Opens) (⨆ (i : ι), basicOpen 𝒜 (f i)) ⊤
have refine : ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x),
  ∃ (i : ι), Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x
Tactic: refine top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x
⊢ ∃ (i : ι), Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x
have by_contra! : ∀ (H : ∀ (i : ι), x ∉ basicOpen 𝒜 (f i)), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (hypothesis)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x
H : ∀ (i : ι), x ∉ basicOpen 𝒜 (f i)
⊢ False
have H₁ : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
Tactic: simp only [mem_basicOpen, Decidable.not_not] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
⊢ False
have refine : Ideal.span (Set.range f) ≤ x.asHomogeneousIdeal.toSubmodule
Tactic: refine x.not_irrelevant_le (hf.trans ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
⊢ Ideal.span (Set.range f) ≤ x.asHomogeneousIdeal.toSubmodule
have rwa : Set.range f ⊆ (↑x.asHomogeneousIdeal.toSubmodule : Set A)
Tactic: rwa [Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x
H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal
rwa : Set.range f ⊆ (↑x.asHomogeneousIdeal.toSubmodule : Set A)
⊢ Ideal.span (Set.range f) ≤ x.asHomogeneousIdeal.toSubmodule
have rwa₁ : ∀ (y : ι), f y ∈ (↑x.asHomogeneousIdeal.toSubmodule : Set A)
Tactic: rwa [Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
⊢ Eq.{u + 1} (α := (Proj 𝒜).Opens) (⨆ (i : ι), basicOpen 𝒜 (f i)) ⊤
have refine : ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x),
  ∃ (i : ι), Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x
Tactic: classical
  refine top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_
  by_contra! H
  simp only [mem_basicOpen, Decidable.not_not] at H
  refine x.not_irrelevant_le (hf.trans ?_)
  rwa [Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
refine :
  ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x),
    ∃ (i : ι), Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x
⊢ Eq.{u + 1} (α := (Proj 𝒜).Opens) (⨆ (i : ι), basicOpen 𝒜 (f i)) ⊤
have refine₁ : ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x)
  (H : ∀ (i : ι), x ∉ basicOpen 𝒜 (f i)), False
Tactic: classical
  refine top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_
  by_contra! H
  simp only [mem_basicOpen, Decidable.not_not] at H
  refine x.not_irrelevant_le (hf.trans ?_)
  rwa [Ideal.span_le, Set.range_subset_iff]