awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
⊢ U.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = U.ι ⁻¹ᵁ X.basicOpen r
have dsimp : Functor.obj (Opens.map (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (↑U : Scheme).toSpecΓ))))
    (PrimeSpectrum.basicOpen
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
        r)) =
  U.ι ⁻¹ᵁ X.basicOpen r
Tactic: dsimp [toSpecΓ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
⊢ Functor.obj
      (Opens.map (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (↑U : Scheme).toSpecΓ))))
      (PrimeSpectrum.basicOpen
        ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
              (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
          r)) =
    U.ι ⁻¹ᵁ X.basicOpen r
have simp : Eq.{u + 1} (α := (↑U : Scheme).Opens)
  ((↑U : Scheme).basicOpen (U := ⊤)
    ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
      r))
  ((↑U : Scheme).basicOpen (U := U.ι ⁻¹ᵁ U)
    ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier) (X :=
          Γ(X, U)) (Y := Γ((↑U : Scheme), U.ι ⁻¹ᵁ U)) (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), U.ι ⁻¹ᵁ U) : Type u))
      r))
Tactic: simp only [Scheme.toSpecΓ_preimage_basicOpen, preimage_basicOpen, ι_app, homOfLE_leOfHom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
⊢ Eq.{u + 1} (α := (↑U : Scheme).Opens)
    ((↑U : Scheme).basicOpen (U := ⊤)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
        r))
    ((↑U : Scheme).basicOpen (U := U.ι ⁻¹ᵁ U)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier) (X :=
            Γ(X, U)) (Y := Γ((↑U : Scheme), U.ι ⁻¹ᵁ U)) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), U.ι ⁻¹ᵁ U) : Type u))
        r))
have rw : Eq.{u + 1} (α := (↑U : Scheme).Opens)
  ((↑U : Scheme).basicOpen (U := ⊤)
    ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
      r))
  ((↑U : Scheme).basicOpen (U := ⊤)
    ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier) (X :=
          Γ(X, U))
          (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
      r))
Tactic: rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.ι_preimage_self.symm).op,
    ← ConcreteCategory.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
⊢ Eq.{u + 1} (α := (↑U : Scheme).Opens)
    ((↑U : Scheme).basicOpen (U := ⊤)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
        r))
    ((↑U : Scheme).basicOpen (U := ⊤)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier) (X :=
            Γ(X, U))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
        r))
have e_f : X.presheaf.map (Quiver.Hom.op (eqToHom sorry)) =
  X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom sorry))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
⊢ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
    X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))
have e_f : Eq (α := Γ(X, U) ⟶ Γ((↑U : Scheme), ⊤)) (X.presheaf.map (eqToHom sorry))
  (X.presheaf.map
    (CategoryStruct.comp (Y := op (U.ι ''ᵁ U.ι ⁻¹ᵁ U)) (Quiver.Hom.op (homOfLE sorry))
      (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom sorry)))))
Tactic: simp [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
⊢ Eq (α := Set ↥(↑U : Scheme)) (Set.preimage (β := ↥(Spec Γ(X, U))) (⇑U.toSpecΓ) (PrimeSpectrum.zeroLocus s))
    (U.carrier ↓∩ X.zeroLocus s)
have h : ∀ (x : ↥(↑U : Scheme)),
  Membership.mem (γ := Set ↥(↑U : Scheme))
      (Set.preimage (β := ↥(Spec Γ(X, U))) (⇑U.toSpecΓ) (PrimeSpectrum.zeroLocus s)) x ↔
    Membership.mem (γ := Set ↥(↑U : Scheme)) (U.carrier ↓∩ X.zeroLocus s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥(↑U : Scheme)
⊢ Membership.mem (γ := Set ↥(↑U : Scheme))
      (Set.preimage (β := ↥(Spec Γ(X, U))) (⇑U.toSpecΓ) (PrimeSpectrum.zeroLocus s)) x ↔
    Membership.mem (γ := Set ↥(↑U : Scheme)) (U.carrier ↓∩ X.zeroLocus s) x
have h : ∀ (y : (↑Γ(X, U) : Type u)) (hy : y ∈ s),
  y ∈ (↑(PrimeSpectrum.asIdeal (U.toSpecΓ x)) : Set (↑Γ(X, U) : Type u)) ↔
    (↑x : ↥X) ∈ (↑(X.toRingedSpace.basicOpen y) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ
Tactic: refine .trans (forall₂_congr fun y hy ↦ ?_) Set.mem_iInter₂.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' X.zeroLocus s) (PrimeSpectrum.zeroLocus s)
have h : ∀ (x : ↥(Spec Γ(X, U))),
  Membership.mem (γ := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' X.zeroLocus s) x ↔
    Membership.mem (γ := Set ↥(Spec Γ(X, U))) (PrimeSpectrum.zeroLocus s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
x : ↥(Spec Γ(X, U))
⊢ Membership.mem (γ := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' X.zeroLocus s) x ↔
    Membership.mem (γ := Set ↥(Spec Γ(X, U))) (PrimeSpectrum.zeroLocus s) x
have h : (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ (↑x.asIdeal : Set (↑Γ(X, U) : Type u))
Tactic: suffices (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ x.asIdeal by
    simpa [← hU.fromSpec_image_basicOpen, -not_not] using this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
x : ↥(Spec Γ(X, U))
⊢ (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ (↑x.asIdeal : Set (↑Γ(X, U) : Type u))
have h : (∀ f ∈ s, f ∈ x.asIdeal) ↔ s ⊆ (↑x.asIdeal : Set (↑Γ(X, U) : Type u))
Tactic: simp_rw [not_not]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (PrimeSpectrum.zeroLocus s) = X.zeroLocus s ∩ (↑U : Set ↥X)
have rw : Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (⇑hU.fromSpec ⁻¹' X.zeroLocus s) = X.zeroLocus s ∩ (↑U : Set ↥X)
Tactic: rw [← hU.fromSpec_preimage_zeroLocus, Set.image_preimage_eq_inter_range, range_fromSpec]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
rw : Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (⇑hU.fromSpec ⁻¹' X.zeroLocus s) = X.zeroLocus s ∩ (↑U : Set ↥X)
⊢ Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (PrimeSpectrum.zeroLocus s) = X.zeroLocus s ∩ (↑U : Set ↥X)
have rw₁ : X.zeroLocus s ∩ Set.range (ι := ↥(Spec Γ(X, U))) ⇑hU.fromSpec = X.zeroLocus s ∩ (↑U : Set ↥X)
Tactic: rw [← hU.fromSpec_preimage_zeroLocus, Set.image_preimage_eq_inter_range, range_fromSpec]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
rw : Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (⇑hU.fromSpec ⁻¹' X.zeroLocus s) = X.zeroLocus s ∩ (↑U : Set ↥X)
rw₁ : X.zeroLocus s ∩ Set.range (ι := ↥(Spec Γ(X, U))) ⇑hU.fromSpec = X.zeroLocus s ∩ (↑U : Set ↥X)
⊢ Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (PrimeSpectrum.zeroLocus s) = X.zeroLocus s ∩ (↑U : Set ↥X)
have rw₂ : X.zeroLocus s ∩ (↑U : Set ↥X) = X.zeroLocus s ∩ (↑U : Set ↥X)
Tactic: rw [← hU.fromSpec_preimage_zeroLocus, Set.image_preimage_eq_inter_range, range_fromSpec]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
this :
  Eq (α := Set (↑U.carrier : Type u)) (U.carrier ↓∩ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)))
    (U.carrier ↓∩ (X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))))
⊢ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) =
    X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
have h : ∀ (x : ↥X),
  x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
    x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
this :
  Eq (α := Set (↑U.carrier : Type u)) (U.carrier ↓∩ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)))
    (U.carrier ↓∩ (X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))))
x : ↥X
⊢ x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
    x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
have pos : ∀ (hxU : x ∈ U),
  x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
    x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
Tactic: by_cases hxU : x ∈ U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
this :
  Eq (α := Set (↑U.carrier : Type u)) (U.carrier ↓∩ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)))
    (U.carrier ↓∩ (X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))))
x : ↥X
pos :
  ∀ (hxU : x ∈ U),
    x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
      x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
⊢ x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
    x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
have neg : ∀ (hxU : x ∉ U),
  x ∈ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) ↔
    x ∈ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
Tactic: by_cases hxU : x ∈ U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
⊢ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)) =
    X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
have suffices : Eq (α := Set (↑U.carrier : Type u)) (U.carrier ↓∩ X.zeroLocus (↑(I ⊓ J) : Set (↑Γ(X, U) : Type u)))
  (U.carrier ↓∩ (X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))))
Tactic: suffices U.1 ↓∩ (X.zeroLocus (U := U) ↑(I ⊓ J)) =
      U.1 ↓∩ (X.zeroLocus (U := U) I ∪ X.zeroLocus (U := U) J) by
    ext x
    by_cases hxU : x ∈ U
    · simpa [hxU] using congr(⟨x, hxU⟩ ∈ $this)
    · simp only [Submodule.coe_inf, Set.mem_union,
        codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I ∩ J)) hxU,
        codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) I) hxU, true_or]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t : Set ι
ht : t.Finite
⊢ X.zeroLocus (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)) =
    (⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ
have refine : ∀ {i : ι} {t : Set ι} (hit : i ∉ t) (ht : t.Finite)
  (IH :
    X.zeroLocus (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)) =
      (⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ),
  X.zeroLocus (↑(⨅ i_1 ∈ insert i t, I i_1) : Set (↑Γ(X, U) : Type u)) =
    (⋃ i_1 ∈ insert i t, X.zeroLocus (↑(I i_1) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ
Tactic: refine ht.induction_on _ (by simp) fun {i t} hit ht IH ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t_1 : Set ι
ht_1 : t_1.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH :
  X.zeroLocus (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)) =
    (⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ
⊢ X.zeroLocus (↑(⨅ i_1 ∈ insert i t, I i_1) : Set (↑Γ(X, U) : Type u)) =
    (⋃ i_1 ∈ insert i t, X.zeroLocus (↑(I i_1) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ
have simp : X.zeroLocus (↑(⨅ (i_1 : ι), ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) : Set (↑Γ(X, U) : Type u)) =
  X.zeroLocus ((↑(I i) : Set (↑Γ(X, U) : Type u)) ∩ (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)))
Tactic: simp only [Set.mem_insert_iff, Set.iUnion_iUnion_eq_or_left, ← IH, ← zeroLocus_inf,
    Submodule.coe_inf, Set.union_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t_1 : Set ι
ht_1 : t_1.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH :
  X.zeroLocus (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)) =
    (⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))) ∪ (↑U : Set ↥X)ᶜ
⊢ X.zeroLocus (↑(⨅ (i_1 : ι), ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) : Set (↑Γ(X, U) : Type u)) =
    X.zeroLocus ((↑(I i) : Set (↑Γ(X, U) : Type u)) ∩ (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)))
have h : (↑(⨅ (i_1 : ι), ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) : Set (↑Γ(X, U) : Type u)) =
  (↑(I i) : Set (↑Γ(X, U) : Type u)) ∩ (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u))
Tactic: congr!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ X.zeroLocus (↑(⨅ i ∈ t, I i) : Set (↑Γ(X, U) : Type u)) = ⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))
have rw : (↑U : Set ↥X)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))
Tactic: rw [zeroLocus_biInf I ht, Set.union_eq_left]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal (↑Γ(X, U) : Type u)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ (↑U : Set ↥X)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))
have obtain : ∀ (i : ι) (hi : i ∈ t), (↑U : Set ↥X)ᶜ ⊆ ⋃ i ∈ t, X.zeroLocus (↑(I i) : Set (↑Γ(X, U) : Type u))
Tactic: obtain ⟨i, hi⟩ := ht'
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal (↑A : Type u)
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ f.liftQuotient I hI ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = f
have rw : X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))) = f
Tactic: rw [Scheme.Hom.liftQuotient, Category.assoc, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
    Ideal.Quotient.lift_comp_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal (↑A : Type u)
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))) = f
have simp : f ≫ Spec.map (ΓSpecIso A).hom ≫ Spec.map (ΓSpecIso A).inv = f
Tactic: simp only [CommRingCat.hom_comp, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom, Spec.map_comp, ←
    Scheme.toSpecΓ_naturality_assoc, ← SpecMap_ΓSpecIso_hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) :=
  Quiver.Hom.unop
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (op A)) :
        (a : X ⟶ Scheme.Spec.obj (op A)) → Scheme.Γ.rightOp.obj X ⟶ op A)
      f)
φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (CommRingCat.Hom.hom φ).kerLift
⊢ Function.Injective (α := (↑Γ(Spec (specTargetImage f), ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (specTargetImageFactorization f))) :
      (a : (↑Γ(Spec (specTargetImage f), ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
have change : Function.Injective (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (X := Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤)) (Y := Γ(X, ⊤))
        (Scheme.Hom.appTop
          ((ΓSpec.adjunction.homEquiv X (op (specTargetImage f)) :
              (a : Scheme.Γ.rightOp.obj X ⟶ op (specTargetImage f)) → X ⟶ Scheme.Spec.obj (op (specTargetImage f)))
            φ'.op))) :
    (a : (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
Tactic: change Function.Injective <| ((ΓSpec.adjunction.homEquiv X _) φ'.op).appTop
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) :=
  Quiver.Hom.unop
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (op A)) :
        (a : X ⟶ Scheme.Spec.obj (op A)) → Scheme.Γ.rightOp.obj X ⟶ op A)
      f)
φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (CommRingCat.Hom.hom φ).kerLift
⊢ Function.Injective (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤)) (Y := Γ(X, ⊤))
          (Scheme.Hom.appTop
            ((ΓSpec.adjunction.homEquiv X (op (specTargetImage f)) :
                (a : Scheme.Γ.rightOp.obj X ⟶ op (specTargetImage f)) → X ⟶ Scheme.Spec.obj (op (specTargetImage f)))
              φ'.op))) :
      (a : (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
have rw : Function.Injective (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (Iso.hom (Scheme.ΓSpecIso (specTargetImage f)) ≫ φ')) :
    (a : (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
Tactic: rw [ΓSpec_adjunction_homEquiv_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
A : CommRingCat
f : X ⟶ Spec A
φ : A ⟶ Γ(X, ⊤) :=
  Quiver.Hom.unop
    ((Equiv.symm (ΓSpec.adjunction.homEquiv X (op A)) :
        (a : X ⟶ Scheme.Spec.obj (op A)) → Scheme.Γ.rightOp.obj X ⟶ op A)
      f)
φ' : specTargetImage f ⟶ Scheme.Γ.obj (op X) := CommRingCat.ofHom (CommRingCat.Hom.hom φ).kerLift
⊢ Function.Injective (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β := (↑Γ(X, ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Iso.hom (Scheme.ΓSpecIso (specTargetImage f)) ≫ φ')) :
      (a : (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
have apply : Function.Injective.{u + 1, u + 1} (α := (↑Γ(Scheme.Spec.obj (op (specTargetImage f)), ⊤) : Type u)) (β :=
  HasQuotient.Quotient (↑A : Type u) (B := Ideal (↑A : Type u)) (RingHom.ker (CommRingCat.Hom.hom φ)))
  (⇑(CommRingCat.Hom.hom' (Iso.hom (Scheme.ΓSpecIso (specTargetImage f)))) :
    (a : (↑Γ(Spec (specTargetImage f), ⊤) : Type u)) → (↑(specTargetImage f) : Type u))
Tactic: apply (RingHom.kerLift_injective φ.hom).comp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
R : CommRingCat
x : PrimeSpectrum (↑R : Type u)
⊢ CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.AtPrime x.asIdeal)) ≫ (stalkIso R x).inv =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial
have hf : ∀ (s : (↑(CommRingCat.of (↑R : Type u)) : Type u)),
  Eq (α := (↑((Spec R).presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.AtPrime x.asIdeal)) ≫ (stalkIso R x).inv) :
          (a : (↑(CommRingCat.of (↑R : Type u)) : Type u)) → (↑((Spec R).presheaf.stalk x) : Type u))
        s :
      (↑((Spec R).presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) :
          (a : (↑(CommRingCat.of (↑R : Type u)) : Type u)) → (↑((Spec R).presheaf.stalk x) : Type u))
        s :
      (↑((Spec R).presheaf.stalk x) : Type u))
Tactic: ext s : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
R_1 S_1 : CommRingCat
f_1 : R_1 ⟶ S_1
p_1 : PrimeSpectrum (↑S_1 : Type u)
x : PrimeSpectrum (↑R_1 : Type u)
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
⊢ Iso.hom (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) ≫
      (Arrow.mk (X := CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal))
          (Y := CommRingCat.of (Localization.AtPrime p.asIdeal))
          (CommRingCat.ofHom
            (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
              (CommRingCat.Hom.hom f) ⋯))).hom =
    (Arrow.mk (Hom.stalkMap (Spec.map f) p)).hom ≫ (Spec.stalkIso S p).hom
have rw : Iso.hom (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) ≫
    (Arrow.mk (X := CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal)) (Y :=
        CommRingCat.of (Localization.AtPrime p.asIdeal))
        (CommRingCat.ofHom
          (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
            (CommRingCat.Hom.hom f) sorry))).hom =
  (Arrow.mk
        (Iso.hom (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) ≫
          CommRingCat.ofHom
              (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
                (CommRingCat.Hom.hom f) sorry) ≫
            (Spec.stalkIso S p).inv)).hom ≫
    (Spec.stalkIso S p).hom
Tactic: rw [← Scheme.localRingHom_comp_stalkIso]