-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
f₁ f₂ :
  (x : ↥X) ×
    { f : X.presheaf.stalk x ⟶ R //
      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }
mpr :
  ∀ (x₁ : ↥X) (f₁ : X.presheaf.stalk x₁ ⟶ R)
    (h₁ : IsLocalHom (R := (↑(X.presheaf.stalk x₁) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f₁)),
    (∃ (h₁_1 :
        Sigma.fst (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            (Sigma.mk (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
              x₁
              (Subtype.mk (p := fun (f : X.presheaf.stalk x₁ ⟶ R) ↦
                IsLocalHom (R := (↑(X.presheaf.stalk x₁) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f₁
                h₁)) =
          f₂.fst (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })),
        (↑(Sigma.snd (β := fun (x : ↥X) ↦
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
                (Sigma.mk (β := fun (x : ↥X) ↦
                  { f : X.presheaf.stalk x ⟶ R //
                    IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
                  x₁
                  (Subtype.mk (p := fun (f : X.presheaf.stalk x₁ ⟶ R) ↦
                    IsLocalHom (R := (↑(X.presheaf.stalk x₁) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f₁
                    h₁))) :
            X.presheaf.stalk ⟨x₁, ⟨f₁, h₁⟩⟩.fst ⟶ R) =
          Iso.hom (X.presheaf.stalkCongr ⋯) ≫
            (↑(f₂.snd (β := fun (x : ↥X) ↦
                  { f : X.presheaf.stalk x ⟶ R //
                    IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                      (CommRingCat.Hom.hom f) })) :
              X.presheaf.stalk f₂.fst ⟶ R)) →
      Sigma.mk (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
          x₁
          (Subtype.mk (p := fun (f : X.presheaf.stalk x₁ ⟶ R) ↦
            IsLocalHom (R := (↑(X.presheaf.stalk x₁) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f₁ h₁) =
        f₂
⊢ (∃ (h₁ :
      f₁.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
        f₂.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })),
      (↑(f₁.snd (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
          X.presheaf.stalk f₁.fst ⟶ R) =
        Iso.hom (X.presheaf.stalkCongr ⋯) ≫
          (↑(f₂.snd (β := fun (x : ↥X) ↦
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
            X.presheaf.stalk f₂.fst ⟶ R)) →
    f₁ = f₂

Tactic:
obtain ⟨x₁, ⟨f₁, h₁⟩⟩ := f₁