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 : Type u
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : Finite ι
R : ι → CommRingCat
h :
  ∀ (b : ι),
    Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) b ≫ sigmaSpec R =
      CategoryStruct.comp (Y := ∐ fun (i : ι) ↦ Spec (R i)) (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) b)
        (Iso.hom
          (colimit.isoColimitCocone
            {
              cocone :=
                Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
                  (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
              isColimit :=
                (Equiv.symm
                      (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                        (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                    (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                      IsColimit
                        ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                          (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
                  (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }))
⊢ sigmaSpec R =
    Iso.hom
      (colimit.isoColimitCocone
        {
          cocone :=
            Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
              (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (Equiv.symm
                  (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                    (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                  IsColimit
                    ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                      (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) })

Tactic:
ext1
-- 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
inst_2 : Finite ι
R : ι → CommRingCat
b : ι
h :
  Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) b)) =
    Spec.map ((CommRingCat.piFan R).proj b)
⊢ Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) b ≫ sigmaSpec R =
    CategoryStruct.comp (Y := ∐ fun (i : ι) ↦ Spec (R i)) (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) b)
      (Iso.hom
        (colimit.isoColimitCocone
          {
            cocone :=
              Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
                (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
            isColimit :=
              (Equiv.symm
                    (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                      (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                  (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                    IsColimit
                      ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                        (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
                (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }))

Tactic:
simp
-- 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
inst_2 : Finite ι
R : ι → CommRingCat
b : ι
⊢ Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) ↦ (↑(R i) : Type u)) b)) =
    Spec.map ((CommRingCat.piFan R).proj b)

Tactic:
rfl
-- 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
inst_2 : Finite ι
R : ι → CommRingCat
⊢ sigmaSpec R =
    Iso.hom
      (colimit.isoColimitCocone
        {
          cocone :=
            Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
              (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (Equiv.symm
                  (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                    (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                  IsColimit
                    ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                      (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) })

Tactic:
have : sigmaSpec R =
      (colimit.isoColimitCocone ⟨_,
        (IsColimit.precomposeHomEquiv Discrete.natIsoFunctor.symm _).symm (isColimitOfPreserves
          Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R)))⟩).hom := by
    ext1
    simp; rfl
-- 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
inst_2 : Finite ι
R : ι → CommRingCat
this :
  sigmaSpec R =
    Iso.hom
      (colimit.isoColimitCocone
        {
          cocone :=
            Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
              (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (Equiv.symm
                  (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                    (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                  IsColimit
                    ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                      (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) })
rw :
  IsIso (X := ∐ fun (i : ι) ↦ Spec (R i))
    (Iso.hom
      (colimit.isoColimitCocone
        {
          cocone :=
            Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
              (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (Equiv.symm
                  (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                    (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                  IsColimit
                    ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                      (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }))
⊢ IsIso (sigmaSpec R)

Tactic:
rw [this]
-- 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
inst_2 : Finite ι
R : ι → CommRingCat
this :
  sigmaSpec R =
    Iso.hom
      (colimit.isoColimitCocone
        {
          cocone :=
            Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
              (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (Equiv.symm
                  (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                    (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                  IsColimit
                    ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                      (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) })
⊢ IsIso (X := ∐ fun (i : ι) ↦ Spec (R i))
    (Iso.hom
      (colimit.isoColimitCocone
        {
          cocone :=
            Functor.obj (Cocone.precompose (Iso.hom (Iso.symm Discrete.natIsoFunctor)))
              (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (Equiv.symm
                  (IsColimit.precomposeHomEquiv (Iso.symm Discrete.natIsoFunctor)
                    (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) :
                (a : IsColimit (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)) →
                  IsColimit
                    ((Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj
                      (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)))
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }))

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
inst_2 : Finite σ
inst_3 : ∀ (i : σ), IsAffine.{u} (g i)
obtain : ∀ (ι : Type u) (e : σ ≃ ι), IsAffine.{u} (∐ g)
⊢ IsAffine.{u} (∐ g)

Tactic:
obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small.{u} (α := σ)
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι_1 : Type u
f : ι_1 → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite σ
inst_3 : ∀ (i : σ), IsAffine.{u} (g i)
ι : Type u
e : σ ≃ ι
⊢ Finite ι

Tactic:
have : Finite ι := e.finite_iff.mp ‹_›
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι_1 : Type u
f : ι_1 → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite σ
inst_3 : ∀ (i : σ), IsAffine.{u} (g i)
ι : Type u
e : σ ≃ ι
this : Finite ι
i : ι
dsimp : IsAffine.{u} (g ((e.symm : (a : ι) → σ) i))
⊢ IsAffine.{u} ((g ∘ (⇑e.symm : (a : ι) → σ)) i)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι_1 : Type u
f : ι_1 → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite σ
inst_3 : ∀ (i : σ), IsAffine.{u} (g i)
ι : Type u
e : σ ≃ ι
this : Finite ι
i : ι
⊢ IsAffine.{u} (g ((e.symm : (a : ι) → σ) i))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι_1 : Type u
f : ι_1 → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite σ
inst_3 : ∀ (i : σ), IsAffine.{u} (g i)
ι : Type u
e : σ ≃ ι
this : Finite ι
⊢ ∀ (i : ι), IsAffine.{u} ((g ∘ (⇑e.symm : (a : ι) → σ)) i)

Tactic:
have (i : _) : IsAffine ((g ∘ e.symm) i) := by dsimp; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι_1 : Type u
f : ι_1 → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite σ
inst_3 : ∀ (i : σ), IsAffine.{u} (g i)
ι : Type u
e : σ ≃ ι
this_1 : Finite ι
this : ∀ (i : ι), IsAffine.{u} ((g ∘ (⇑e.symm : (a : ι) → σ)) i)
⊢ IsAffine.{u} (∐ g)

Tactic:
IsAffine.of_isIso ((Sigma.reindex e.symm g).inv ≫
    (Sigma.mapIso (fun i ↦ Scheme.isoSpec _)).hom ≫ sigmaSpec _)

Premises used: AlgebraicGeometry.IsAffine.of_isIso, AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.Limits.Sigma.mapIso, AlgebraicGeometry.sigmaSpec, CategoryTheory.CategoryStruct.comp, Equiv.symm, CategoryTheory.Iso.hom, CategoryTheory.Limits.Sigma.reindex, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι_1 : Type u
f : ι_1 → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Finite σ
inst_3 : ∀ (i : σ), IsAffine.{u} (g i)
ι : Type u
e : σ ≃ ι
this_1 : Finite ι
this : ∀ (i : ι), IsAffine.{u} ((g ∘ (⇑e.symm : (a : ι) → σ)) i)
⊢ IsAffine.{u} (∐ g)

Tactic:
exact IsAffine.of_isIso ((Sigma.reindex e.symm g).inv ≫
    (Sigma.mapIso (fun i ↦ Scheme.isoSpec _)).hom ≫ sigmaSpec _)

Premises used: AlgebraicGeometry.IsAffine.of_isIso, AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.Limits.Sigma.mapIso, AlgebraicGeometry.sigmaSpec, CategoryTheory.CategoryStruct.comp, Equiv.symm, CategoryTheory.Iso.hom, CategoryTheory.Limits.Sigma.reindex, CategoryTheory.Iso.inv
-- 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
inst_2 : IsAffine X
inst_3 : IsAffine Y
⊢ IsAffine.{u} (X ⨿ Y)

Tactic:
.of_isIso ((coprod.mapIso X.isoSpec Y.isoSpec).hom ≫ coprodSpec _ _)

Premises used: AlgebraicGeometry.IsAffine.of_isIso, AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.Limits.coprod.mapIso, AlgebraicGeometry.coprodSpec, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
i j : ι
e : i ≠ j
⊢ (Disjoint on U) i j

Tactic:
hU' e
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
i j : ι
e : i ≠ j
a :
  Function.onFun (β := Set ↥X) Disjoint (fun (x : ι) ↦ Set.range (ι := ↥(↑(U x) : Scheme)) ⇑((fun (i : ι) ↦ (U i).ι) x))
      i j ↔
    (Disjoint on U) i j
⊢ Function.onFun (β := Set ↥X) Disjoint (fun (x : ι) ↦ Set.range (ι := ↥(↑(U x) : Scheme)) ⇑((fun (i : ι) ↦ (U i).ι) x))
    i j

Tactic:
convert! hU' e using 0
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
i j : ι
e : i ≠ j
⊢ Function.onFun (β := Set ↥X) Disjoint (fun (x : ι) ↦ Set.range (ι := ↥(↑(U x) : Scheme)) ⇑((fun (i : ι) ↦ (U i).ι) x))
      i j ↔
    (Disjoint on U) i j

Tactic:
simp [← Opens.coe_disjoint]

Premises used: TopologicalSpace.Opens.coe_disjoint
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
⊢ IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)

Tactic:
have := isOpenImmersion_sigmaDesc _ (fun i ↦ (U i).ι)
    (fun i j e ↦ by convert! hU' e using 0; simp [← Opens.coe_disjoint])
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)
⊢ IsAffineOpen.{u} (X := X)
    (Scheme.Hom.opensRange (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Sigma.desc fun (i : ι) ↦ (U i).ι))

Tactic:
isAffineOpen_opensRange (Sigma.desc fun i ↦ (U i).ι)

Premises used: AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.Limits.Sigma.desc
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)
h : iSup U = Scheme.Hom.opensRange (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Sigma.desc fun (i : ι) ↦ (U i).ι)
convert! : IsAffine.{u} (∐ fun (i : ι) ↦ (↑(U i) : Scheme))
⊢ IsAffineOpen (iSup U)

Tactic:
convert! isAffineOpen_opensRange (Sigma.desc fun i ↦ (U i).ι)
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)
h :
  ∀ (x : ↥X),
    x ∈ (↑(iSup U) : Set ↥X) ↔
      x ∈
        (↑(Scheme.Hom.opensRange (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Sigma.desc fun (i : ι) ↦ (U i).ι)) : Set ↥X)
⊢ iSup U = Scheme.Hom.opensRange (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Sigma.desc fun (i : ι) ↦ (U i).ι)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)
x : ↥X
⊢ x ∈ (↑(iSup U) : Set ↥X) ↔
    x ∈ (↑(Scheme.Hom.opensRange (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Sigma.desc fun (i : ι) ↦ (U i).ι)) : Set ↥X)

Tactic:
simp [(sigmaMk _).symm.exists_congr_left, ← Scheme.Hom.comp_apply, Scheme.Opens.exists_toScheme]

Premises used: Equiv.exists_congr_left, Homeomorph.toEquiv, AlgebraicGeometry.Scheme.Opens.exists_toScheme, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.sigmaMk, Homeomorph.symm
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)
⊢ ∀ (i : ι), IsAffine.{u} (↑(U i) : Scheme)

Tactic:
have (i : _) : IsAffine _ := hU i
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
X : Scheme
inst : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this_1 : IsOpenImmersion.{u} (X := ∐ fun (i : ι) ↦ (↑(U i) : Scheme)) (Y := X) (Sigma.desc fun (i : ι) ↦ (U i).ι)
this : ∀ (i : ι), IsAffine.{u} (↑(U i) : Scheme)
⊢ IsAffine.{u} (∐ fun (i : ι) ↦ (↑(U i) : Scheme))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
X : Scheme
inst : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
obtain : ∀ (ι : Type u) (e : σ ≃ ι), IsAffineOpen (iSup U)
⊢ IsAffineOpen (iSup U)

Tactic:
obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small.{u} (α := σ)
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
X : Scheme
inst : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
ι : Type u
e : σ ≃ ι
⊢ Finite ι

Tactic:
have : Finite ι := e.finite_iff.mp ‹_›
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
X : Scheme
inst : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
ι : Type u
e : σ ≃ ι
this : Finite ι
rw : IsAffineOpen.{u} (X := X) (⨆ (x : ι), U ((e.symm : (a : ι) → σ) x))
⊢ IsAffineOpen (iSup U)

Tactic:
rw [← e.symm.iSup_congr fun _ ↦ rfl]

Premises used: Equiv.symm, Equiv.iSup_congr, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
X : Scheme
inst : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
ι : Type u
e : σ ≃ ι
this : Finite ι
⊢ ∀ (i : ι), IsAffineOpen (U ((e.symm : (a : ι) → σ) i))

Tactic:
simp [*]
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
X : Scheme
inst : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
ι : Type u
e : σ ≃ ι
this : Finite ι
⊢ IsAffineOpen.{u} (X := X) (⨆ (x : ι), U ((e.symm : (a : ι) → σ) x))

Tactic:
exact .iSup_of_disjoint_aux (by simp [*]) fun i j h ↦ hU' (e.symm.injective.ne h)
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
rw : IsAffineOpen.{u} (X := X) (⨆ (i : (↑s : Type v)), U (↑i : σ))
⊢ IsAffineOpen.{u} (X := X) (⨆ i ∈ s, U i)

Tactic:
rw [← iSup_subtype'']

Premises used: iSup_subtype''
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
⊢ Finite.{v + 1} (↑s : Type v)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
this : Finite.{v + 1} (↑s : Type v)
⊢ ∀ (i : (↑s : Type v)), IsAffineOpen (U (↑i : σ))

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
this : Finite.{v + 1} (↑s : Type v)
i j : (↑s : Type v)
e : i ≠ j
⊢ (↑i : σ) ≠ (↑j : σ)

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
this : Finite.{v + 1} (↑s : Type v)
⊢ IsAffineOpen.{u} (X := X) (⨆ (i : (↑s : Type v)), U (↑i : σ))

Tactic:
exact .iSup_of_disjoint (by simpa) fun i j e ↦ hU' i.2 j.2 (by aesop)
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
H : Disjoint U V
⊢ ∀ (i : Unit ⊕ Unit),
    IsAffineOpen.{u} (X := X)
      ((fun (i : Unit ⊕ Unit) ↦ (Sum.elim (fun (x : Unit) ↦ U) (fun (x : Unit) ↦ V) i : X.Opens)) i)

Tactic:
simp_all
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
H : Disjoint U V
⊢ _root_.Pairwise (α := Unit ⊕ Unit)
    (Function.onFun.{1, u + 1, 1} (β := X.Opens) Disjoint fun (i : Unit ⊕ Unit) ↦
      Sum.elim (fun (x : Unit) ↦ U) (fun (x : Unit) ↦ V) i)

Tactic:
simp_all [_root_.Pairwise, Unique.forall_iff, ← Opens.coe_disjoint, disjoint_comm]

Premises used: disjoint_comm, Unique.forall_iff, Pairwise, TopologicalSpace.Opens.coe_disjoint
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
H : Disjoint U V
h : U ⊔ V = ⨆ (i : Unit ⊕ Unit), Sum.elim (fun (x : Unit) ↦ U) (fun (x : Unit) ↦ V) i
⊢ IsAffineOpen (U ⊔ V)

Tactic:
convert!
    iSup_of_disjoint (U := fun i : Unit ⊕ Unit ↦ i.elim (fun _ ↦ U) (fun _ ↦ V)) (by simp_all)
      (by simp_all [_root_.Pairwise, Unique.forall_iff, ← Opens.coe_disjoint, disjoint_comm])

Premises used: AlgebraicGeometry.IsAffineOpen.iSup_of_disjoint
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
H : Disjoint U V
⊢ U ⊔ V = ⨆ (i : Unit ⊕ Unit), Sum.elim (fun (x : Unit) ↦ U) (fun (x : Unit) ↦ V) i

Tactic:
aesop
-- 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
inst_2 : Finite.{u + 1} ↥X
inst_3 : DiscreteTopology.{u} ↥X
i j : ↥X
e : i ≠ j
⊢ Function.onFun (β := X.Opens) Disjoint (fun (x : ↥X) ↦ { carrier := {x}, is_open' := ⋯ }) i j

Tactic:
simpa [← TopologicalSpace.Opens.coe_disjoint]

Premises used: TopologicalSpace.Opens.coe_disjoint
-- 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
inst_2 : Finite.{u + 1} ↥X
inst_3 : DiscreteTopology.{u} ↥X
this : IsAffineOpen.{u} (X := X) (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ })
⊢ IsAffineOpen.{u} (X := X) (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ })

Tactic:
this
-- 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
inst_2 : Finite.{u + 1} ↥X
inst_3 : DiscreteTopology.{u} ↥X
this : IsAffineOpen.{u} (X := X) (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ })
h : Eq.{u + 1} (α := X.Opens) ⊤ (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ })
⊢ IsAffineOpen.{u} (X := X) ⊤

Tactic:
convert! this
-- 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
inst_2 : Finite.{u + 1} ↥X
inst_3 : DiscreteTopology.{u} ↥X
this : IsAffineOpen.{u} (X := X) (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ })
h : ∀ (x : ↥X), x ∈ (↑⊤ : Set ↥X) ↔ x ∈ (↑(⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ : Opens ↥X }) : Set ↥X)
⊢ Eq.{u + 1} (α := X.Opens) ⊤ (⨆ (x : ↥X), { carrier := {x}, is_open' := ⋯ })

Tactic:
ext