awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
R S : CommRingCat
this :
  CategoryStruct.comp (Y := Scheme.Spec.obj (op R ⨿ op S))
      (coprodComparison Scheme.Spec (op R) (op S) :
        Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S) ⟶ Scheme.Spec.obj (op R ⨿ op S))
      (Spec.map
          (CategoryStruct.comp (Y := limit (pair R S))
            (Iso.inv (limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }))
            (Iso.inv (Iso.unop (opProdIsoCoprod R S)))) :
        Spec (unop (op R ⨿ op S)) ⟶
          Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt) =
    coprodSpec (↑R : Type u) (↑S : Type u)
rw :
  IsIso (Y := Scheme.Spec.obj (op R ⨿ op S))
    (coprodSpec (↑R : Type u) (↑S : Type u) ≫
        inv
          (Spec.map
            (CategoryStruct.comp (Y := limit (pair R S))
              (Iso.inv (limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }))
              (Iso.inv (Iso.unop (opProdIsoCoprod R S))))) :
      Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S) ⟶ Scheme.Spec.obj (op R ⨿ op S))
⊢ IsIso (X := Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S)) (Y := Scheme.Spec.obj (op R ⨿ op S))
    (coprodComparison Scheme.Spec (op R) (op S))

Tactic:
rw [(IsIso.eq_comp_inv _).mpr this]

Premises used: Iff.mpr, CategoryTheory.IsIso.eq_comp_inv
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S_1 : Type u
inst : CommRing R_1
inst_1 : CommRing S_1
R S : CommRingCat
this :
  CategoryStruct.comp (Y := Scheme.Spec.obj (op R ⨿ op S))
      (coprodComparison Scheme.Spec (op R) (op S) :
        Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S) ⟶ Scheme.Spec.obj (op R ⨿ op S))
      (Spec.map
          (CategoryStruct.comp (Y := limit (pair R S))
            (Iso.inv (limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }))
            (Iso.inv (Iso.unop (opProdIsoCoprod R S)))) :
        Spec (unop (op R ⨿ op S)) ⟶
          Spec { cone := R.prodFan S, isLimit := R.prodFanIsLimit S : LimitCone (pair R S) }.cone.pt) =
    coprodSpec (↑R : Type u) (↑S : Type u)
⊢ IsIso (Y := Scheme.Spec.obj (op R ⨿ op S))
    (coprodSpec (↑R : Type u) (↑S : Type u) ≫
        inv
          (Spec.map
            (CategoryStruct.comp (Y := limit (pair R S))
              (Iso.inv (limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }))
              (Iso.inv (Iso.unop (opProdIsoCoprod R S))))) :
      Scheme.Spec.obj (op R) ⨿ Scheme.Spec.obj (op S) ⟶ Scheme.Spec.obj (op R ⨿ op S))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
⊢ PreservesColimitsOfShape (Discrete WalkingPair) Scheme.Spec

Tactic:
⟨fun {_} ↦
    have (X Y : CommRingCat.{u}ᵒᵖ) := PreservesColimitPair.of_iso_coprod_comparison Scheme.Spec X Y
    preservesColimit_of_iso_diagram _ (diagramIsoPair _).symm⟩

Premises used: CategoryTheory.Limits.PreservesColimitPair.of_iso_coprod_comparison, AlgebraicGeometry.Scheme.Spec, CategoryTheory.Limits.preservesColimit_of_iso_diagram, CategoryTheory.Iso.symm, CategoryTheory.Limits.PreservesColimitsOfShape.mk, CategoryTheory.Limits.diagramIsoPair
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
⊢ IsEmpty.{u + 1} ↥(Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ))

Tactic:
have : IsEmpty (Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ)) :=
    @Function.isEmpty _ _ spec_punit_isEmpty (Scheme.Spec.mapIso
      (initialIsoIsInitial (initialOpOfTerminal CommRingCat.punitIsTerminal))).hom
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
this : IsEmpty.{u + 1} ↥(Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ))
⊢ PreservesColimit (Functor.empty CommRingCatᵒᵖ) Scheme.Spec

Tactic:
have := preservesInitial_of_iso Scheme.Spec (asIso (initial.to _))
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
this_1 : IsEmpty.{u + 1} ↥(Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ))
this : PreservesColimit (Functor.empty CommRingCatᵒᵖ) Scheme.Spec
⊢ PreservesColimitsOfShape (Discrete PEmpty.{1}) Scheme.Spec

Tactic:
preservesColimitsOfShape_pempty_of_preservesInitial _

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_pempty_of_preservesInitial
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
this_1 : IsEmpty.{u + 1} ↥(Scheme.Spec.obj (⊥_ CommRingCatᵒᵖ))
this : PreservesColimit (Functor.empty CommRingCatᵒᵖ) Scheme.Spec
⊢ PreservesColimitsOfShape (Discrete PEmpty.{1}) Scheme.Spec

Tactic:
exact preservesColimitsOfShape_pempty_of_preservesInitial _

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_pempty_of_preservesInitial
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
J : Type u_1
inst_2 : Finite J
⊢ PreservesColimitsOfShape.{u_1, u_1, u, u, u + 1, u + 1} (Discrete J) Scheme.Spec

Tactic:
PreservesFiniteCoproducts.of_preserves_binary_and_initial _ _

Premises used: CategoryTheory.PreservesFiniteCoproducts.of_preserves_binary_and_initial
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
R : ι → CommRingCat
i : ι
⊢ Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec.{u, u_1} R =
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type (max u u_1))) i))

Tactic:
Sigma.ι_desc _ _

Premises used: CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
he : IsIdempotentElem (M := (a : ι) → R a) (Function.update (β := R) 0 i 1)
H :
  ∀ (x y : (a : ι) → R a),
    Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
        ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i) ↔
      Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y
H' :
  Function.Surjective (α := (a : ι) → R a) (β := R i) (⇑(algebraMap ((a : ι) → R a) (R i)) : (a : (a : ι) → R a) → R i)
⊢ IsLocalization.Away (R := (a : ι) → R a) (Function.update (β := R) 0 i 1) (R i)

Tactic:
apply IsLocalization.away_of_isIdempotentElem_of_mul

Premises used: IsLocalization.away_of_isIdempotentElem_of_mul
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
he :
  ∀ (j : ι),
    HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1)
        (Function.update (β := R) 0 i 1) j =
      Function.update (β := R) 0 i 1 j
⊢ IsIdempotentElem (M := (a : ι) → R a) (Function.update (β := R) 0 i 1)

Tactic:
ext j
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
j : ι
pos :
  ∀ (h : j = i),
    HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1)
        (Function.update (β := R) 0 i 1) j =
      Function.update (β := R) 0 i 1 j
neg :
  ∀ (h : ¬j = i),
    HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1)
        (Function.update (β := R) 0 i 1) j =
      Function.update (β := R) 0 i 1 j
⊢ HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1) (Function.update (β := R) 0 i 1)
      j =
    Function.update (β := R) 0 i 1 j

Tactic:
by_cases h : j = i
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
j : ι
h : j = i
⊢ HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1) (Function.update (β := R) 0 i 1)
      j =
    Function.update (β := R) 0 i 1 j

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
j : ι
h : ¬j = i
⊢ HMul.hMul (α := (a : ι) → R a) (β := (a : ι) → R a) (Function.update (β := R) 0 i 1) (Function.update (β := R) 0 i 1)
      j =
    Function.update (β := R) 0 i 1 j

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
x y : (a : ι) → R a
H :
  Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
      ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i) →
    Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y
H₁ :
  Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y →
    Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
      ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i)
⊢ Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
      ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i) ↔
    Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
x y : (a : ι) → R a
e :
  Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
    ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i)
H :
  ∀ (j : ι),
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
      HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j
⊢ Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y

Tactic:
ext j
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
x y : (a : ι) → R a
e :
  Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
    ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i)
j : ι
pos :
  ∀ (h : j = i),
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
      HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j
neg :
  ∀ (h : ¬j = i),
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
      HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j
⊢ HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j

Tactic:
by_cases h : j = i
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
x y : (a : ι) → R a
e :
  Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
    ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i)
j : ι
h : j = i
⊢ HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
x y : (a : ι) → R a
e :
  Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
    ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i)
j : ι
h : ¬j = i
⊢ HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) x j =
    HMul.hMul (α := (a : ι) → R a) (Function.update (β := R) 0 i 1) y j

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
x y : (a : ι) → R a
e : Function.update (β := R) 0 i 1 * x = Function.update (β := R) 0 i 1 * y
⊢ Eq (α := R i) ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) x : R i)
    ((algebraMap ((a : ι) → R a) (R i) : (a : (a : ι) → R a) → R i) y : R i)

Tactic:
simpa using congr_fun e i

Premises used: congr_fun
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
⊢ Function.Surjective (α := (a : ι) → R a) (β := R i) (⇑(algebraMap ((a : ι) → R a) (R i)) : (a : (a : ι) → R a) → R i)

Tactic:
Function.surjective_eval _

Premises used: Function.surjective_eval
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
⊢ Function.Surjective (α := (a : ι) → R a) (β := R i) (⇑(algebraMap ((a : ι) → R a) (R i)) : (a : (a : ι) → R a) → R i)

Tactic:
exact Function.surjective_eval _

Premises used: Function.surjective_eval
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
⊢ IsLocalization.Away (R := (a : ι) → R a) (Function.update (β := R) 0 i 1) (R i)

Tactic:
have : IsLocalization.Away (Function.update (β := R) 0 i 1) (R i) := by
    apply IsLocalization.away_of_isIdempotentElem_of_mul
    · ext j; by_cases h : j = i <;> aesop
    · intro x y
      constructor
      · intro e; ext j; by_cases h : j = i <;> aesop
      · intro e; simpa using congr_fun e i
    · exact Function.surjective_eval _
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this_1 : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
this : IsLocalization.Away (R := (a : ι) → R a) (Function.update (β := R) 0 i 1) (R i)
⊢ IsOpenImmersion (X := Spec (CommRingCat.of (R i))) (Y := Spec (CommRingCat.of ((i : ι) → R i)))
    (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ R x) i)))

Tactic:
IsOpenImmersion.of_isLocalization (Function.update 0 i 1)

Premises used: Function.update, AlgebraicGeometry.IsOpenImmersion.of_isLocalization, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
this_1 : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i)
this : IsLocalization.Away (R := (a : ι) → R a) (Function.update (β := R) 0 i 1) (R i)
⊢ IsOpenImmersion (X := Spec (CommRingCat.of (R i))) (Y := Spec (CommRingCat.of ((i : ι) → R i)))
    (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ R x) i)))

Tactic:
exact IsOpenImmersion.of_isLocalization (Function.update 0 i 1)
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst_2 : (i : ι) → CommRing (R i)
letI letI₁ letI₂ :
  IsOpenImmersion (X := Spec (CommRingCat.of (R i))) (Y := Spec (CommRingCat.of ((i : ι) → R i)))
    (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ R x) i)))
letI₃ :
  let this : Algebra ((i : ι) → R i) (R i) := RingHom.toAlgebra (Pi.evalRingHom R i);
  ∀ (this : IsLocalization.Away (R := (a : ι) → R a) (Function.update (β := R) 0 i 1) (R i)),
    IsOpenImmersion (X := Spec (CommRingCat.of (R i))) (Y := Spec (CommRingCat.of ((i : ι) → R i)))
      (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ R x) i)))
⊢ IsOpenImmersion (X := Spec (CommRingCat.of (R i))) (Y := Spec (CommRingCat.of ((i : ι) → R i)))
    (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (x : ι) ↦ R x) i)))

Tactic:
classical
  letI := (Pi.evalRingHom R i).toAlgebra
  have : IsLocalization.Away (Function.update (β := R) 0 i 1) (R i) := by
    apply IsLocalization.away_of_isIdempotentElem_of_mul
    · ext j; by_cases h : j = i <;> aesop
    · intro x y
      constructor
      · intro e; ext j; by_cases h : j = i <;> aesop
      · intro e; simpa using congr_fun e i
    · exact Function.surjective_eval _
  exact IsOpenImmersion.of_isLocalization (Function.update 0 i 1)
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
hα :
  _root_.Pairwise.{u} (α := ι)
    (Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint fun (x : ι) ↦
      Set.range (ι := ↥(Spec (R x)))
        ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
⊢ IsOpenImmersion (sigmaSpec R)

Tactic:
apply isOpenImmersion_sigmaDesc

Premises used: AlgebraicGeometry.isOpenImmersion_sigmaDesc
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
ix iy : ι
h : ix ≠ iy
⊢ Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint
    (fun (x : ι) ↦
      Set.range (ι := ↥(Spec (R x)))
        ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
    ix iy

Tactic:
Set.disjoint_iff_forall_ne.mpr ?_

Premises used: Iff.mpr, Set.disjoint_iff_forall_ne
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
ix iy : ι
h : ix ≠ iy
hα :
  ∀ ⦃a : ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))⦄,
    Membership.mem (γ := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
        ((fun (x : ι) ↦
            (Set.range (ι := ↥(Spec (R x)))
                ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))) :
              Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))))
          ix)
        a →
      ∀ ⦃b : ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))⦄,
        Membership.mem (γ := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
            ((fun (x : ι) ↦
                (Set.range (ι := ↥(Spec (R x)))
                    ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))) :
                  Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))))
              iy)
            b →
          a ≠ b
⊢ Function.onFun (β := Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) Disjoint
    (fun (x : ι) ↦
      Set.range (ι := ↥(Spec (R x)))
        ⇑(Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) x))))
    ix iy

Tactic:
refine Set.disjoint_iff_forall_ne.mpr ?_

Premises used: Iff.mpr, Set.disjoint_iff_forall_ne
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
ix iy : ι
h : ix ≠ iy
x : ↥(Spec (R ix))
y : ↥(Spec (R iy))
e :
  Eq (α := ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
    ((Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) ix))) x :
      ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
    ((Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) iy))) y :
      ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
⊢ (DFinsupp.single (β := fun (x : ι) ↦ (↑(R x) : Type u)) iy 1 : (a : ι) → (↑(R a) : Type u)) ix ∈ x.asIdeal

Tactic:
simp [h.symm]

Premises used: Ne.symm
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
ix iy : ι
h : ix ≠ iy
x : ↥(Spec (R ix))
y : ↥(Spec (R iy))
e :
  Eq (α := ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
    ((Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) ix))) x :
      ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
    ((Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) iy))) y :
      ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
⊢ (DFinsupp.single (β := fun (x : ι) ↦ (↑(R x) : Type u)) iy 1 : (a : ι) → (↑(R a) : Type u)) iy ∈ y.asIdeal

Tactic:
have : DFinsupp.single (β := (R ·)) iy 1 iy ∈ y.asIdeal :=
    (PrimeSpectrum.ext_iff.mp e).le (x := DFinsupp.single iy 1)
      (show DFinsupp.single (β := (R ·)) iy 1 ix ∈ x.asIdeal by simp [h.symm])
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R_1 S : Type u
inst : CommRing R_1
inst_1 : CommRing S
R : ι → CommRingCat
ix iy : ι
h : ix ≠ iy
x : ↥(Spec (R ix))
y : ↥(Spec (R iy))
e :
  Eq (α := ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
    ((Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) ix))) x :
      ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
    ((Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) iy))) y :
      ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
this : (DFinsupp.single (β := fun (x : ι) ↦ (↑(R x) : Type u)) iy 1 : (a : ι) → (↑(R a) : Type u)) iy ∈ y.asIdeal
⊢ False

Tactic:
simp [← Ideal.eq_top_iff_one, y.2.ne_top] at this

Premises used: PrimeSpectrum.isPrime, Ideal.eq_top_iff_one, Ideal.IsPrime.ne_top