-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma equiv_of_fromSpecStalkOfMem_eq [IrreducibleSpace X]
    {x : X} [X.IsGermInjectiveAt x] (f g : X.PartialMap Y)
    (hxf : x ∈ f.domain) (hxg : x ∈ g.domain)
    (H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg) : f.equiv g

Proof state:
case refine_2.intro.intro
X Y : Scheme
inst✝¹ : IrreducibleSpace ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ (Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom =
    (Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom

Tactic:
simp only [TopologicalSpace.Opens.carrier_eq_coe, IsOpenMap.coe_functor_obj,
  TopologicalSpace.Opens.coe_inf, restrict_hom, ← Category.assoc] at e ⊢

Result:
case refine_2.intro.intro
X Y : Scheme
inst✝¹ : IrreducibleSpace ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : (U.ι ≫ X.homOfLE ⋯) ≫ f.hom = (U.ι ≫ X.homOfLE ⋯) ≫ g.hom
⊢ ((Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ X.homOfLE ⋯) ≫ f.hom =
    ((Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ X.homOfLE ⋯) ≫ g.hom

Proof state:
case refine_2
X Y : Scheme
inst✝¹ : IrreducibleSpace ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this✝ : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
this : ∃ U, ⟨x, ⋯⟩ ∈ U ∧ U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ f.equiv g

Tactic:
obtain ⟨U, hxU, e⟩ := this

Result:
case refine_2.intro.intro
X Y : Scheme
inst✝¹ : IrreducibleSpace ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ f.equiv g

Proof state:
X Y : Scheme
inst✝¹ : IrreducibleSpace ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
⊢ f.equiv g

Tactic:
have hdense : Dense ((f.domain ⊓ g.domain) : Set X) :=
  f.dense_domain.inter_of_isOpen_left g.dense_domain f.domain.2

Result:
X Y : Scheme
inst✝¹ : IrreducibleSpace ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
⊢ f.equiv g