-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f]
    (hX : (∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
hX : ¬((∃ (S : CommRingCat.{u}), X = Spec S) ∧ ∃ (R : CommRingCat.{u}), Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀
j : (𝒰X i).I₀
inr :
  IsOpenImmersion (Y := pullback.diagonalObj ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))
    (pullback.diagonal ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))
⊢ IsOpenImmersion (X :=
    (↑(pullback.diagonal f ⁻¹ᵁ
          Scheme.Hom.opensRange (X :=
            (Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).X
              (Sigma.mk (β := fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := (Scheme.Pullback.openCoverOfBase 𝒰Y f f).X i)
                  ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
                              (Scheme.Pullback.openCoverOfLeftRight (𝒰X i) (𝒰X i)
                                  (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i)
                                  (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i) :
                                (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i)
                                    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i ⟶ 𝒰Y.X i)
                                    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i ⟶ 𝒰Y.X i)).OpenCover))
                            i) :
                        PreZeroHypercover ((Scheme.Pullback.openCoverOfBase 𝒰Y f f).X i)))
                    i))
                (Sigma.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
                  (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j))
                (Sigma.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
                    (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j),
                  Sigma.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
                    (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j))))
            ((Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).f
              (Sigma.mk (β := fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := (Scheme.Pullback.openCoverOfBase 𝒰Y f f).X i)
                  ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
                              (Scheme.Pullback.openCoverOfLeftRight (𝒰X i) (𝒰X i)
                                  (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i)
                                  (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i) :
                                (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i)
                                    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i ⟶ 𝒰Y.X i)
                                    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i ⟶ 𝒰Y.X i)).OpenCover))
                            i) :
                        PreZeroHypercover ((Scheme.Pullback.openCoverOfBase 𝒰Y f f).X i)))
                    i))
                (Sigma.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
                  (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j))
                (Sigma.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
                    (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j),
                  Sigma.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
                    (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j))))) :
      Scheme))
    (pullback.diagonal f ∣_
      Scheme.Hom.opensRange (X :=
        (Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).X
          (Sigma.mk (β := fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := (Scheme.Pullback.openCoverOfBase 𝒰Y f f).X i)
              ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
                          (Scheme.Pullback.openCoverOfLeftRight (𝒰X i) (𝒰X i)
                              (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i)
                              (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i) :
                            (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i) (Y :=
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i)
                                (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i ⟶ 𝒰Y.X i)
                                (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i ⟶ 𝒰Y.X i)).OpenCover))
                        i) :
                    PreZeroHypercover ((Scheme.Pullback.openCoverOfBase 𝒰Y f f).X i)))
                i))
            (Sigma.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
              (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j))
            (Sigma.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
                (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j),
              Sigma.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
                (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j))))
        ((Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).f
          (Sigma.mk (β := fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := (Scheme.Pullback.openCoverOfBase 𝒰Y f f).X i)
              ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰Y f f).I₀) ↦
                          (Scheme.Pullback.openCoverOfLeftRight (𝒰X i) (𝒰X i)
                              (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i)
                              (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i) :
                            (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i) (Y :=
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i)
                                (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i ⟶ 𝒰Y.X i)
                                (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰Y f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).X i ⟶ 𝒰Y.X i)).OpenCover))
                        i) :
                    PreZeroHypercover ((Scheme.Pullback.openCoverOfBase 𝒰Y f f).X i)))
                i))
            (Sigma.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
              (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j))
            (Sigma.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
                (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j),
              Sigma.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)
                (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀) i j)))))

Tactic:
rw [arrow_mk_iso_iff (P := @IsOpenImmersion)
      (Scheme.Pullback.diagonalRestrictIsoDiagonal f 𝒰Y 𝒰X i j)]

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.IsOpenImmersion, AlgebraicGeometry.Scheme.Pullback.diagonalRestrictIsoDiagonal