awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g_1 : σ → Scheme
inst : Small.{u, v} σ
g : σ → Scheme
⊢ CoproductDisjoint g
have refine : {i j : σ} →
  (hij : i ≠ j) →
    IsInitial (C := Scheme)
      (Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
        ((fun {i j : σ} (x : i ≠ j) ↦
            (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
          hij))
Tactic: refine .of_hasCoproduct (fun _ ↦ pullback.cone _ _) (fun _ ↦ pullback.isLimit _ _) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g_1 : σ → Scheme
inst : Small.{u, v} σ
g : σ → Scheme
i j : σ
hij : i ≠ j
⊢ IsInitial (C := Scheme)
    (Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
      ((fun {i j : σ} (x : i ≠ j) ↦
          (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
        hij))
have h : Nonempty.{u + 2}
  (IsInitial (C := Scheme)
    (Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
      ((fun {i j : σ} (x : i ≠ j) ↦
          (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
        hij)))
Tactic: apply Nonempty.some
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g_1 : σ → Scheme
inst : Small.{u, v} σ
g : σ → Scheme
i j : σ
hij : i ≠ j
⊢ Nonempty.{u + 2}
    (IsInitial (C := Scheme)
      (Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
        ((fun {i j : σ} (x : i ≠ j) ↦
            (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
          hij)))
have h : IsEmpty.{u + 1}
  ↥(Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
      ((fun {i j : σ} (x : i ≠ j) ↦
          (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
        hij))
Tactic: rw [isInitial_iff_isEmpty]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ Eq (α := ↥(∐ f)) ((sigmaMk f : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i x) : ↥(∐ f))
    ((Sigma.ι f i) x : ↥(∐ f))
have change : Eq (α := (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
          Scheme.forgetToTop.obj (∐ f))
          (CategoryStruct.comp (Y :=
            Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
              (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
            (Cofan.inj (f := fun (x : ι) ↦ (f x).toTopCat) (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) i :
              (f i).toTopCat ⟶
                Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
                  (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
            (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
                (Iso.inv
                  (colimit.isoColimitCocone
                    { cocone := TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat,
                      isColimit := TopCat.sigmaCofanIsColimit fun (x : ι) ↦ (f x).toTopCat }))
                (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))) :
              Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
                  (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) ⟶
                Scheme.forgetToTop.obj (∐ f))) :
        (a : (↑(f i).toTopCat : Type u)) → (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
      x :
    (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
          Scheme.forgetToTop.obj (∐ f)) (Scheme.forgetToTop.map (Sigma.ι f i)) :
        (a : (↑(Scheme.forgetToTop.obj (f i)) : Type u)) → (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
      x :
    (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
Tactic: change ((TopCat.sigmaCofan (fun x ↦ (f x).toTopCat)).inj i ≫
    (colimit.isoColimitCocone ⟨_, TopCat.sigmaCofanIsColimit _⟩).inv ≫ _) x =
      Scheme.forgetToTop.map (Sigma.ι f i) x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ Eq (α := (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
            Scheme.forgetToTop.obj (∐ f))
            (CategoryStruct.comp (Y :=
              Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
                (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
              (Cofan.inj (f := fun (x : ι) ↦ (f x).toTopCat) (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) i :
                (f i).toTopCat ⟶
                  Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
                    (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
              (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
                  (Iso.inv
                    (colimit.isoColimitCocone
                      { cocone := TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat,
                        isColimit := TopCat.sigmaCofanIsColimit fun (x : ι) ↦ (f x).toTopCat }))
                  (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))) :
                Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
                    (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) ⟶
                  Scheme.forgetToTop.obj (∐ f))) :
          (a : (↑(f i).toTopCat : Type u)) → (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
        x :
      (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
            Scheme.forgetToTop.obj (∐ f)) (Scheme.forgetToTop.map (Sigma.ι f i)) :
          (a : (↑(Scheme.forgetToTop.obj (f i)) : Type u)) → (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
        x :
      (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
have e_a : Eq (α := (f i).toTopCat ⟶ Scheme.forgetToTop.obj (∐ f))
  (CategoryStruct.comp (Y :=
    Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
      (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
    (Cofan.inj (f := fun (x : ι) ↦ (f x).toTopCat) (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) i :
      (f i).toTopCat ⟶
        Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
          (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
    (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
        (Iso.inv
          (colimit.isoColimitCocone
            { cocone := TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat,
              isColimit := TopCat.sigmaCofanIsColimit fun (x : ι) ↦ (f x).toTopCat }))
        (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))) :
      Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
          (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) ⟶
        Scheme.forgetToTop.obj (∐ f)))
  (Scheme.forgetToTop.map (Sigma.ι f i))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
Goal:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ Eq (α := (f i).toTopCat ⟶ Scheme.forgetToTop.obj (∐ f))
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
        (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
      (Cofan.inj (f := fun (x : ι) ↦ (f x).toTopCat) (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) i :
        (f i).toTopCat ⟶
          Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
            (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
      (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
          (Iso.inv
            (colimit.isoColimitCocone
              { cocone := TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat,
                isColimit := TopCat.sigmaCofanIsColimit fun (x : ι) ↦ (f x).toTopCat }))
          (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))) :
        Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
            (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) ⟶
          Scheme.forgetToTop.obj (∐ f)))
    (Scheme.forgetToTop.map (Sigma.ι f i))
have e_a : Eq (α :=
  Functor.obj (Discrete.functor fun (x : ι) ↦ (f x).toTopCat) { as := i : Discrete ι } ⟶ Scheme.forgetToTop.obj (∐ f))
  (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
    (colimit.ι (Discrete.functor fun (x : ι) ↦ (f x).toTopCat) { as := i })
    (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))))
  (Scheme.forgetToTop.map (Sigma.ι f i))
Tactic: refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.sigmaCofanIsColimit _⟩ _ _).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))
⊢ IsOpenImmersion (X := ∐ f) (Sigma.desc α)
have rw : Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α) ∧
  ∀ (x : ↥(∐ f)), IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)
Tactic: rw [IsOpenImmersion.iff_isIso_stalkMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))
⊢ Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α) ∧
    ∀ (x : ↥(∐ f)), IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)
have left : Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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 : Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α)
⊢ Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α) ∧
    ∀ (x : ↥(∐ f)), IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)
have right : ∀ (x : ↥(∐ f)), IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))
this :
  Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
⊢ Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α)
have h : Eq (α := ↥(∐ f) → ↥X) (⇑(Sigma.desc α))
  (Function.comp (β := (i : ι) × ↥(f i))
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
    (⇑(sigmaMk f).symm : (a : ↥(∐ f)) → (i : ι) × ↥(f i)))
Tactic: convert! this.comp (sigmaMk f).symm.isOpenEmbedding
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))
this :
  Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
⊢ Eq (α := ↥(∐ f) → ↥X) (⇑(Sigma.desc α))
    (Function.comp (β := (i : ι) × ↥(f i))
      (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
      (⇑(sigmaMk f).symm : (a : ↥(∐ f)) → (i : ι) × ↥(f i)))
have h : ∀ (x : ↥(∐ f)),
  Eq (α := ↥X) ((Sigma.desc α) x : ↥X)
    (Function.comp (β := (i : ι) × ↥(f i))
        (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
        (⇑(sigmaMk f).symm : (a : ↥(∐ f)) → (i : ι) × ↥(f i)) x :
      ↥X)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))
⊢ Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α)
have left : Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
  (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
Tactic: suffices Topology.IsOpenEmbedding (Sigma.desc α ∘ sigmaMk f) by
      convert! this.comp (sigmaMk f).symm.isOpenEmbedding; ext; simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))
⊢ Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
have left : Continuous (X := (i : ι) × ↥(f i)) (Y := ↥X)
  (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
Tactic: refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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)))
⊢ Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
have left₁ : Function.Injective (α := (i : ι) × ↥(f i)) (β := ↥X)
  (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
Tactic: refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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)))
⊢ Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
have left₂ : IsOpenMap (X := (i : ι) × ↥(f i)) (Y := ↥X)
  (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
Tactic: refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (hypothesis)
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 (α := (i : ι) × ↥(f i)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) iy y)
have this : Eq (α := ↥X) ((α ix) x : ↥X) ((α iy) y : ↥X)
Tactic: have : α ix x = α iy y := by
        simpa [← Scheme.Hom.comp_apply] using e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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)
⊢ ix = iy
have by_contra : ∀ (h : ¬ix = iy), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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)
⊢ Eq (α := (i : ι) × ↥(f i)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) iy y)
have 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)
Tactic: obtain rfl : ix = iy := by
        by_contra h
        exact Set.disjoint_iff_forall_ne.mp (hα h) ⟨x, rfl⟩ ⟨y, this.symm⟩ rfl
Cleared hypotheses: iy, y, e, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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)
⊢ Eq (α := (i : ι) × ↥(f i)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix x) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix y)
have left : Eq (α := (i : ι) × ↥(f i)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix y) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) ix y)
Tactic: rw [(α ix).isOpenEmbedding.injective this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))
⊢ IsOpenMap (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
have 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)
Tactic: rw [isOpenMap_sigma]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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)
⊢ IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)
have 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)
Tactic: have ⟨y, hy⟩ := (Scheme.IsLocallyDirected.openCover (Discrete.functor f)).covers x