-- 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
inr :
  ∀ (i : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) × (𝒰X i).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))
                  (i.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀))
                  (i.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀),
                    i.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀))))
              ((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))
                  (i.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀))
                  (i.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀),
                    i.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀))))) :
        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))
              (i.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀))
              (i.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀),
                i.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀))))
          ((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))
              (i.fst (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀))
              (i.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀),
                i.snd (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀) ↦ (𝒰X i).I₀)))))
⊢ IsOpenImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
apply IsZariskiLocalAtTarget.of_range_subset_iSup _
      (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange f 𝒰Y 𝒰X)

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_range_subset_iSup, AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange