-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
x : ↥(D.obj A.i')
⊢ ∃ (j : (i : A.𝒰S.I₀) × (A.𝒰X i).I₀) (y :
    ↥(PreZeroHypercover.X (S := D.obj A.i')
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Precoverage.ZeroHypercover.pullback₁ A.g (Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X)))
        (Sigma.mk (β := fun (i : (Scheme.Pullback.openCoverOfBase A.𝒰S f f).I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := (Scheme.Pullback.openCoverOfBase A.𝒰S f f).X i)
            ((fun (i : (Scheme.Pullback.openCoverOfBase A.𝒰S f f).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (i : (Scheme.Pullback.openCoverOfBase A.𝒰S f f).I₀) ↦
                        (Scheme.Pullback.openCoverOfLeftRight (A.𝒰X i) (A.𝒰X i)
                            (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i)
                            (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i) :
                          (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i) (Y :=
                              (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i)
                              (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i :
                                (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i ⟶ A.𝒰S.X i)
                              (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i :
                                (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i ⟶ A.𝒰S.X i)).OpenCover))
                      i) :
                  PreZeroHypercover ((Scheme.Pullback.openCoverOfBase A.𝒰S f f).X i)))
              i))
          (j.fst (β := fun (i : A.𝒰S.I₀) ↦ (A.𝒰X i).I₀))
          (j.snd (β := fun (i : A.𝒰S.I₀) ↦ (A.𝒰X i).I₀), j.snd (β := fun (i : A.𝒰S.I₀) ↦ (A.𝒰X i).I₀))))),
    ((fun (i : (i : A.𝒰S.I₀) × (A.𝒰X i).I₀) ↦
            (PreZeroHypercover.f
                (Precoverage.ZeroHypercover.toPreZeroHypercover
                  (Precoverage.ZeroHypercover.pullback₁ A.g (Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X)))
                (Sigma.mk (β := fun (i : (Scheme.Pullback.openCoverOfBase A.𝒰S f f).I₀) ↦
                  PreZeroHypercover.I₀ (C := Scheme) (S := (Scheme.Pullback.openCoverOfBase A.𝒰S f f).X i)
                    ((fun (i : (Scheme.Pullback.openCoverOfBase A.𝒰S f f).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                            ((fun (i : (Scheme.Pullback.openCoverOfBase A.𝒰S f f).I₀) ↦
                                (Scheme.Pullback.openCoverOfLeftRight (A.𝒰X i) (A.𝒰X i)
                                    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i)
                                    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i) :
                                  (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i) (Y :=
                                      (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i)
                                      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i ⟶ A.𝒰S.X i)
                                      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i ⟶ A.𝒰S.X i)).OpenCover))
                              i) :
                          PreZeroHypercover ((Scheme.Pullback.openCoverOfBase A.𝒰S f f).X i)))
                      i))
                  (i.fst (β := fun (i : A.𝒰S.I₀) ↦ (A.𝒰X i).I₀))
                  (i.snd (β := fun (i : A.𝒰S.I₀) ↦ (A.𝒰X i).I₀), i.snd (β := fun (i : A.𝒰S.I₀) ↦ (A.𝒰X i).I₀))) :
              PreZeroHypercover.X (S := D.obj A.i')
                  (Precoverage.ZeroHypercover.toPreZeroHypercover
                    (Precoverage.ZeroHypercover.pullback₁ A.g (Scheme.Pullback.diagonalCover f A.𝒰S A.𝒰X)))
                  (Sigma.mk (β := fun (i : (Scheme.Pullback.openCoverOfBase A.𝒰S f f).I₀) ↦
                    PreZeroHypercover.I₀ (C := Scheme) (S := (Scheme.Pullback.openCoverOfBase A.𝒰S f f).X i)
                      ((fun (i : (Scheme.Pullback.openCoverOfBase A.𝒰S f f).I₀) ↦
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                              ((fun (i : (Scheme.Pullback.openCoverOfBase A.𝒰S f f).I₀) ↦
                                  (Scheme.Pullback.openCoverOfLeftRight (A.𝒰X i) (A.𝒰X i)
                                      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i)
                                      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i) :
                                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i) (Y :=
                                        (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i)
                                        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i :
                                          (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i ⟶ A.𝒰S.X i)
                                        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) A.𝒰S f i :
                                          (Precoverage.ZeroHypercover.pullback₁ f A.𝒰S).X i ⟶ A.𝒰S.X i)).OpenCover))
                                i) :
                            PreZeroHypercover ((Scheme.Pullback.openCoverOfBase A.𝒰S f f).X i)))
                        i))
                    (i.fst (β := fun (i : A.𝒰S.I₀) ↦ (A.𝒰X i).I₀))
                    (i.snd (β := fun (i : A.𝒰S.I₀) ↦ (A.𝒰X i).I₀), i.snd (β := fun (i : A.𝒰S.I₀) ↦ (A.𝒰X i).I₀))) ⟶
                D.obj A.i'))
          j)
        y =
      x

Tactic:
simpa [← Set.mem_range, Scheme.Pullback.range_fst,
        Scheme.Pullback.diagonalCoverDiagonalRange] using A.range_g_subset ⟨x, rfl⟩

Premises used: Set.mem_range, AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange, Exists.intro, AlgebraicGeometry.Scheme.Pullback.range_fst, AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset, rfl