-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Limits (goal)
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))))
hα₁ :
  ∀ ⦃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
hα₂ :
  ∀ ⦃ix iy : ι⦄ (h : ix ≠ iy) ⦃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
hα₃ :
  ∀ ⦃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)))))),
    False
⊢ IsOpenImmersion (sigmaSpec R)
have hα₄ : ∀ ⦃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: classical
  apply isOpenImmersion_sigmaDesc
  intro ix iy h
  refine Set.disjoint_iff_forall_ne.mpr ?_
  rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ e
  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])
  simp [← Ideal.eq_top_iff_one, y.2.ne_top] at this