Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
⊢ [UniversallyInjective f, ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f,
      Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable,
      Surjective (pullback.diagonal f)].TFAE

Tactic:
tfae_have 4 → 3 := fun hf ↦ by
    have := tfae_1_iff_4.mpr hf
    refine ⟨f.injective, ?_⟩
    rw [surjective_iff] at hf
    intro x
    algebraize [(f.residueFieldMap x).hom]
    rw [RingHom.IsPurelyInseparable, isPurelyInseparable_iff_subsingleton_emb, subsingleton_iff]
    intro σ₁ σ₂
    apply AlgHom.coe_ringHom_injective
    let g₁ := (X.SpecToEquivOfField _).symm ⟨_, CommRingCat.ofHom σ₁.toRingHom⟩
    let g₂ := (X.SpecToEquivOfField _).symm ⟨_, CommRingCat.ofHom σ₂.toRingHom⟩
    suffices X.SpecToEquivOfField _ g₁ = X.SpecToEquivOfField _ g₂ by
      rw [Equiv.apply_symm_apply, Equiv.apply_symm_apply] at this
      exact congr($(this).2.hom)
    let q := pullback.lift (f := f) (g := f) g₁ g₂ <| by
      simp only [g₁, g₂, Scheme.SpecToEquivOfField_symm_apply, AlgHom.toRingHom_eq_coe,
        Category.assoc, ← f.SpecMap_residueFieldMap_fromSpecResidueField x, ← Spec.map_comp_assoc]
      congr 2
      ext a
      simp only [CommRingCat.hom_comp, RingHom.comp_apply]
      exact (AlgHom.commutes σ₁ a).trans (AlgHom.commutes σ₂ a).symm
    have q_fst : q ≫ pullback.fst f f = g₁ := pullback.lift_fst _ _ _
    have q_snd : q ≫ pullback.snd f f = g₂ := pullback.lift_snd _ _ _
    rw [Scheme.SpecToEquivOfField_eq_iff, ← q_fst, ← q_snd]
    obtain ⟨u, hu⟩ := hf (q (IsLocalRing.closedPoint _))
    have hux : u = x := by
      have := congr(pullback.fst f f $(hu))
      rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply] at this
      simpa [Scheme.SpecToEquivOfField_symm_apply, q_fst, g₁] using this
    refine ⟨by simp [g₁, g₂, q_fst, q_snd], ?_⟩
    dsimp
    simp only [Scheme.descResidueField_stalkClosedPointTo_comp, ← Category.assoc]
    congr 1
    rw [← cancel_mono (Scheme.residueFieldCongr (hux ▸ hu).symm).hom]
    have : Mono (Scheme.Hom.residueFieldMap (pullback.diagonal f) x) :=
      ConcreteCategory.mono_of_injective _ (RingHom.injective _)
    simp [← cancel_mono ((pullback.diagonal f).residueFieldMap x), ← Scheme.residueFieldMap_comp,
      (pullback.fst f f).residueFieldMap_congr', (pullback.snd f f).residueFieldMap_congr'_assoc,
      Scheme.Hom.residueFieldMap_congr (pullback.diagonal_snd f),
      Scheme.Hom.residueFieldMap_congr (pullback.diagonal_fst f)]

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
tfae_4_to_3 :
  Surjective (pullback.diagonal f) →
    Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
⊢ [UniversallyInjective f, ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f,
      Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable,
      Surjective (pullback.diagonal f)].TFAE