-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
Ω : Type u
inst : Field Ω
inst_1 : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑((𝒰.X i).residueField y) : Type u) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst_1 : Algebra (↑(S.residueField ((𝒰.f i) y)) : Type u) (↑(CommRingCat.of Ω) : Type u) :=
  (CommRingCat.Hom.hom a).toAlgebra
b : (↑((𝒰.X i).residueField y) : Type u) →ₐ[(↑(S.residueField ((𝒰.f i) y)) : Type u)] Ω := IsSepClosed.lift
hfac : Hom.residueFieldMap (𝒰.f i) y ≫ CommRingCat.ofHom b.toRingHom = a
h :
  Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) (𝒰.f i)) :
          (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj (𝒰.X i))) →
            (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
        (Spec.map (CommRingCat.ofHom b.toRingHom) ≫ (𝒰.X i).fromSpecResidueField y) :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
    ((Equiv.symm (SpecToEquivOfField Ω S) :
          (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
        (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) ((𝒰.f i) y) a :
          (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) :
      Spec (CommRingCat.of Ω) ⟶ S)
⊢ ∃ (y_1 : Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) (𝒰.X i)),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) (𝒰.f i)) :
            (a : (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj (𝒰.X i))) →
              (fun (X : Type u) ↦ X) ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).obj S))
          y_1 :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj coyoneda (Opposite.op (Spec (CommRingCat.of Ω)))) S))
      ((Equiv.symm (SpecToEquivOfField Ω S) :
            (a : (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) → Spec (CommRingCat.of Ω) ⟶ S)
          (Sigma.mk (β := fun (x : ↥S) ↦ S.residueField x ⟶ CommRingCat.of Ω) ((𝒰.f i) y) a :
            (x : ↥S) × (S.residueField x ⟶ CommRingCat.of Ω)) :
        Spec (CommRingCat.of Ω) ⟶ S)

Tactic:
use Spec.map (CommRingCat.ofHom b.toRingHom) ≫ (𝒰.X i).fromSpecResidueField y

Premises used: CommRingCat.ofHom, AlgebraicGeometry.Spec.map, CategoryTheory.PreZeroHypercover.X, AlgHom.toRingHom, AlgebraicGeometry.Scheme.fromSpecResidueField, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover