-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → OpenCover.{u_1, u} (pullback f (𝒰.f i))
inst : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
inst_1 : ∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), IsAffine.{u} ((𝒱 i).X j)
U : (i : 𝒰.I₀) × (𝒱 i).I₀ → (↑(diagonalCoverDiagonalRange f 𝒰 𝒱) : Scheme).Opens :=
  fun (i : (i : 𝒰.I₀) × (𝒱 i).I₀) ↦
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ
      Hom.opensRange (X :=
        (diagonalCover f 𝒰 𝒱).X
          (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
            PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
              ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                      ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                          (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                            OpenCover.{u_1, u}
                              (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                        i) :
                    PreZeroHypercover.{u_1, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                i))
            (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀))
            (i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀), i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀))))
        ((diagonalCover f 𝒰 𝒱).f
          (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
            PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
              ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                      ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                          (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                            OpenCover.{u_1, u}
                              (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                        i) :
                    PreZeroHypercover.{u_1, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                i))
            (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀))
            (i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀), i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀))))
i : (i : 𝒰.I₀) × (𝒱 i).I₀
rw :
  Hom.opensRange (X :=
      (diagonalCover f 𝒰 𝒱).X
        (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
          PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                            (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                          OpenCover.{u_1, u}
                            (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                              (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                      i) :
                  PreZeroHypercover.{u_1, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
              i))
          (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀))
          (i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀), i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀))))
      ((diagonalCover f 𝒰 𝒱).f
        (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
          PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                            (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                          OpenCover.{u_1, u}
                            (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                              (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                      i) :
                  PreZeroHypercover.{u_1, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
              i))
          (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀))
          (i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀), i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀)))) ≤
    diagonalCoverDiagonalRange f 𝒰 𝒱
⊢ (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i =
    Hom.opensRange (X :=
      (diagonalCover f 𝒰 𝒱).X
        (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
          PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                            (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                          OpenCover.{u_1, u}
                            (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                              (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                      i) :
                  PreZeroHypercover.{u_1, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
              i))
          (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀))
          (i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀), i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀))))
      ((diagonalCover f 𝒰 𝒱).f
        (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
          PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                            (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                          OpenCover.{u_1, u}
                            (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                              (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                      i) :
                  PreZeroHypercover.{u_1, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
              i))
          (i.fst (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀))
          (i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀), i.snd (β := fun (i : 𝒰.I₀) ↦ (𝒱 i).I₀))))

Tactic:
rw [Scheme.Hom.image_preimage_eq_opensRange_inf, inf_eq_right, Opens.opensRange_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.Scheme.Opens.opensRange_ι, inf_eq_right