awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
left :
  Continuous (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
left₁ :
  Function.Injective (α := (i : ι) × ↥(f i)) (β := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
left₂ :
  IsOpenMap (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
⊢ Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))

Tactic:
refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
⊢ Continuous (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
ix : ι
x : ↥(f ix)
iy : ι
y : ↥(f iy)
e :
  Eq (α := ↥X)
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x))
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) iy y))
⊢ Eq (α := ↥X) ((α ix) x : ↥X) ((α iy) y : ↥X)

Tactic:
simpa [← Scheme.Hom.comp_apply] using e

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
ix : ι
x : ↥(f ix)
iy : ι
y : ↥(f iy)
e :
  Eq (α := ↥X)
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x))
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) iy y))
⊢ Eq (α := ↥X) ((α ix) x : ↥X) ((α iy) y : ↥X)

Tactic:
have : α ix x = α iy y := by
        simpa [← Scheme.Hom.comp_apply] using e
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
ix : ι
x : ↥(f ix)
iy : ι
y : ↥(f iy)
e :
  Eq (α := ↥X)
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x))
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) iy y))
this : Eq (α := ↥X) ((α ix) x : ↥X) ((α iy) y : ↥X)
by_contra : ∀ (h : ¬ix = iy), False
⊢ ix = iy

Tactic:
by_contra h
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
ix : ι
x : ↥(f ix)
iy : ι
y : ↥(f iy)
e :
  Eq (α := ↥X)
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x))
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) iy y))
this : Eq (α := ↥X) ((α ix) x : ↥X) ((α iy) y : ↥X)
h : ¬ix = iy
⊢ False

Tactic:
Set.disjoint_iff_forall_ne.mp (hα h) ⟨x, rfl⟩ ⟨y, this.symm⟩ rfl

Premises used: Set.disjoint_iff_forall_ne, Exists.intro, Iff.mp, Eq.symm, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
ix : ι
x : ↥(f ix)
iy : ι
y : ↥(f iy)
e :
  Eq (α := ↥X)
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x))
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) iy y))
this : Eq (α := ↥X) ((α ix) x : ↥X) ((α iy) y : ↥X)
h : ¬ix = iy
⊢ False

Tactic:
exact Set.disjoint_iff_forall_ne.mp (hα h) ⟨x, rfl⟩ ⟨y, this.symm⟩ rfl

Premises used: Set.disjoint_iff_forall_ne, Exists.intro, Iff.mp, Eq.symm, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
ix : ι
x : ↥(f ix)
iy : ι
y : ↥(f iy)
e :
  Eq (α := ↥X)
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x))
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) iy y))
this : Eq (α := ↥X) ((α ix) x : ↥X) ((α iy) y : ↥X)
left :
  ∀ (y : ↥(f ix))
    (e :
      Eq (α := ↥X)
        (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
          (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x))
        (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
          (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix y)))
    (this : Eq (α := ↥X) ((α ix) x : ↥X) ((α ix) y : ↥X)),
    Eq (α := (i : ι) × ↥(f i)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix y)
⊢ Eq (α := (i : ι) × ↥(f i)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) iy y)

Tactic:
obtain rfl : ix = iy := by
        by_contra h
        exact Set.disjoint_iff_forall_ne.mp (hα h) ⟨x, rfl⟩ ⟨y, this.symm⟩ rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
ix : ι
x y : ↥(f ix)
e :
  Eq (α := ↥X)
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x))
    (Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
      (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix y))
this : Eq (α := ↥X) ((α ix) x : ↥X) ((α ix) y : ↥X)
left left₁ :
  Eq (α := (i : ι) × ↥(f i)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix y) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix y)
⊢ Eq (α := (i : ι) × ↥(f i)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix y)

Tactic:
rw [(α ix).isOpenEmbedding.injective this]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
left :
  ∀ (i : ι),
    IsOpenMap (Y := ↥X) fun (a : ↥(f i)) ↦
      Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α)
        (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i a)
⊢ IsOpenMap (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))

Tactic:
rw [isOpenMap_sigma]

Premises used: isOpenMap_sigma
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
i : ι
⊢ IsOpenMap (Y := ↥X) fun (a : ↥(f i)) ↦
    Function.comp (α := (i : ι) × ↥(f i)) (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f))
      (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i a)

Tactic:
simpa [← Scheme.Hom.comp_apply] using (α i).isOpenEmbedding.isOpenMap

Premises used: Topology.IsOpenEmbedding.isOpenMap, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
x : ↥(∐ f)
right :
  ∀
    (y :
      ↥(PreZeroHypercover.X (S := colimit (Discrete.functor f))
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
            PreZeroHypercover (colimit (Discrete.functor f)))
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x :
            PreZeroHypercover.I₀ (S := colimit (Discrete.functor f))
              (Precoverage.ZeroHypercover.toPreZeroHypercover
                  (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
                PreZeroHypercover (colimit (Discrete.functor f))))))
    (hy :
      (PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
          y =
        x),
    IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)
⊢ IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
have ⟨y, hy⟩ := (Scheme.IsLocallyDirected.openCover (Discrete.functor f)).covers x
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
x : ↥(∐ f)
y :
  ↥(PreZeroHypercover.X (S := colimit (Discrete.functor f))
      (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
        PreZeroHypercover (colimit (Discrete.functor f)))
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x :
        PreZeroHypercover.I₀ (S := colimit (Discrete.functor f))
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
            PreZeroHypercover (colimit (Discrete.functor f)))))
hy :
  (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
right :
  IsIso (X :=
    X.presheaf.stalk
      ((Sigma.desc α)
        ((PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
              (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
            y :
          ↥(colimit (Discrete.functor f)))))
    (Scheme.Hom.stalkMap (Sigma.desc α)
      ((PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y))
⊢ IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
rw [← hy]
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
x : ↥(∐ f)
y :
  ↥(PreZeroHypercover.X (S := colimit (Discrete.functor f))
      (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
        PreZeroHypercover (colimit (Discrete.functor f)))
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x :
        PreZeroHypercover.I₀ (S := colimit (Discrete.functor f))
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
            PreZeroHypercover (colimit (Discrete.functor f)))))
hy :
  (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ IsIso (X :=
    X.presheaf.stalk
      ((Sigma.desc α)
        ((PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
              (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
            y :
          ↥(colimit (Discrete.functor f)))))
    (Scheme.Hom.stalkMap (Sigma.desc α)
      ((PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y))

Tactic:
IsIso.of_isIso_fac_right
      (f := ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f _).stalkMap y)
      (h := (X.presheaf.stalkCongr (.of_eq ?_)).hom ≫ (α _).stalkMap _) ?_

Premises used: CategoryTheory.IsIso.of_isIso_fac_right
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
x : ↥(∐ f)
y :
  ↥(PreZeroHypercover.X (S := colimit (Discrete.functor f))
      (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
        PreZeroHypercover (colimit (Discrete.functor f)))
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x :
        PreZeroHypercover.I₀ (S := colimit (Discrete.functor f))
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) :
            PreZeroHypercover (colimit (Discrete.functor f)))))
hy :
  (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ Eq (α := ↥X)
    ((Sigma.desc α)
        ((PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.IsLocallyDirected.openCover (Discrete.functor f)))
              (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
            y :
          ↥(colimit (Discrete.functor f))) :
      ↥X)
    ((α (Discrete.as (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))) y : ↥X)

Tactic:
simp [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
obtain : ∀ (ι : Type u) (e : σ ≃ ι), IsOpenImmersion (X := ∐ g) (Sigma.desc α)
⊢ IsOpenImmersion (X := ∐ g) (Sigma.desc α)

Tactic:
obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small (α := σ)

Premises used: Small.equiv_small
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ IsOpenImmersion (X := ∐ g) (Y := X)
    (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
      (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i)))

Tactic:
IsOpenImmersion.comp ((Sigma.reindex e.symm g).inv) (Sigma.desc fun i ↦ α _)

Premises used: AlgebraicGeometry.IsOpenImmersion.comp, CategoryTheory.Limits.Sigma.desc, Equiv.symm, CategoryTheory.Limits.Sigma.reindex, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
h :
  Eq (α := ∐ g ⟶ X) (Sigma.desc α)
    (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
      (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i)))
convert! :
  IsOpenImmersion.{u} (X := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Y := X)
    (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i))
⊢ IsOpenImmersion (X := ∐ g) (Sigma.desc α)

Tactic:
convert! IsOpenImmersion.comp ((Sigma.reindex e.symm g).inv) (Sigma.desc fun i ↦ α _)
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ Eq (α := ∐ g ⟶ X) (Sigma.desc α)
    (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
      (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i)))

Tactic:
Sigma.hom_ext _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Sigma.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
h :
  ∀ (i : σ),
    CategoryStruct.comp (Y := ∐ g) (Sigma.ι g i) (Sigma.desc α) =
      CategoryStruct.comp (Y := ∐ g) (Sigma.ι g i)
        (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
          (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i)))
⊢ Eq (α := ∐ g ⟶ X) (Sigma.desc α)
    (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
      (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i)))

Tactic:
refine Sigma.hom_ext _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Sigma.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
i : σ
h :
  ∀ (i : ι),
    Eq (α := g ((e.symm : (a : ι) → σ) i) ⟶ X)
      (CategoryStruct.comp (Y := ∐ g) (Sigma.ι g ((e.symm : (a : ι) → σ) i)) (Sigma.desc α))
      (CategoryStruct.comp (Y := ∐ g) (Sigma.ι g ((e.symm : (a : ι) → σ) i))
        (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
          (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i))))
⊢ CategoryStruct.comp (Y := ∐ g) (Sigma.ι g i) (Sigma.desc α) =
    CategoryStruct.comp (Y := ∐ g) (Sigma.ι g i)
      (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
        (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i)))

Tactic:
obtain ⟨i, rfl⟩ := e.symm.surjective i

Premises used: Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
i : ι
⊢ Eq (α := g ((e.symm : (a : ι) → σ) i) ⟶ X)
    (CategoryStruct.comp (Y := ∐ g) (Sigma.ι g ((e.symm : (a : ι) → σ) i)) (Sigma.desc α))
    (CategoryStruct.comp (Y := ∐ g) (Sigma.ι g ((e.symm : (a : ι) → σ) i))
      (CategoryStruct.comp (Y := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Iso.inv (Sigma.reindex e.symm g))
        (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i))))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
hα₁ :
  _root_.Pairwise.{u} (α := ι)
    (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦
      Set.range (ι := ↥((g ∘ (⇑e.symm : (a : ι) → σ)) x)) ⇑(α ((e.symm : (a : ι) → σ) x)))
⊢ IsOpenImmersion.{u} (X := sigmaObj (β := ι) (g ∘ (⇑e.symm : (a : ι) → σ))) (Y := X)
    (Sigma.desc fun (i : ι) ↦ α ((e.symm : (a : ι) → σ) i))

Tactic:
apply isOpenImmersion_sigmaDesc_aux

Premises used: _private.0.AlgebraicGeometry.isOpenImmersion_sigmaDesc_aux
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
i j : ι
hij : i ≠ j
⊢ Function.onFun (β := Set ↥X) Disjoint
    (fun (x : ι) ↦ Set.range (ι := ↥((g ∘ (⇑e.symm : (a : ι) → σ)) x)) ⇑(α ((e.symm : (a : ι) → σ) x))) i j

Tactic:
hα (fun h ↦ hij (e.symm.injective h))

Premises used: Equiv.injective, Equiv.symm
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst_1 : ∀ (i : σ), IsOpenImmersion (α i)
hα :
  _root_.Pairwise.{v} (α := σ)
    (Function.onFun.{v + 1, u + 1, 1} (β := Set ↥X) Disjoint fun (x : σ) ↦ Set.range (ι := ↥(g x)) ⇑(α x))
ι : Type u
e : σ ≃ ι
i j : ι
hij : i ≠ j
⊢ Function.onFun (β := Set ↥X) Disjoint
    (fun (x : ι) ↦ Set.range (ι := ↥((g ∘ (⇑e.symm : (a : ι) → σ)) x)) ⇑(α ((e.symm : (a : ι) → σ) x))) i j

Tactic:
exact hα (fun h ↦ hij (e.symm.injective h))

Premises used: Equiv.injective, Equiv.symm