-- 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
⊢ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom = (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom

Tactic:
rw [← cancel_epi (Scheme.Hom.isoImage _ _).hom]

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 ≫ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom =
    (Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom

Proof state:
case refine_1
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, ⋯⟩
⊢ (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ f.hom =
    (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ g.hom

Tactic:
rw [← f.fromSpecStalkOfMem_restrict hdense inf_le_left ⟨hxf, hxg⟩,
  ← g.fromSpecStalkOfMem_restrict hdense inf_le_right ⟨hxf, hxg⟩] at H

Result:
case refine_1
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
hdense : Dense (↑f.domain ⊓ ↑g.domain)
H :
  (f.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯ =
    (g.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
⊢ (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ f.hom =
    (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ g.hom

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 ≫ X.homOfLE ⋯) ≫ f.hom =
    ((Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ X.homOfLE ⋯) ≫ g.hom

Tactic:
convert e using 2 <;> rw [← cancel_mono (Scheme.Opens.ι _)] <;> simp

Result:
no goals

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
⊢ f.equiv g

Tactic:
refine ⟨(f.domain ⊓ g.domain).ι ''ᵁ U, ((f.domain ⊓ g.domain).ι ''ᵁ U).2.dense
  ⟨_, ⟨_, hxU, rfl⟩⟩,
  ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_left,
  ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_right, ?_⟩

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.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom = (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom

Proof state:
case refine_1
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
hdense : Dense (↑f.domain ⊓ ↑g.domain)
H :
  (f.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯ =
    (g.restrict (f.domain ⊓ g.domain) hdense ⋯).fromSpecStalkOfMem ⋯
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
⊢ (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ f.hom =
    (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ g.hom

Tactic:
simpa only [fromSpecStalkOfMem, restrict_domain, Opens.fromSpecStalkOfMem, Spec.map_inv,
  restrict_hom, Category.assoc, IsIso.eq_inv_comp, IsIso.hom_inv_id_assoc] using H

Result:
no goals

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
hdense : Dense (↑f.domain ⊓ ↑g.domain)
⊢ f.equiv g

Tactic:
have := (isGermInjectiveAt_iff_of_isOpenImmersion (f := (f.domain ⊓ g.domain).ι)
  (x := ⟨x, hxf, hxg⟩)).mp ‹_›

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)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
⊢ 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
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
⊢ f.equiv g

Tactic:
have := spread_out_unique_of_isGermInjective' (X := (f.domain ⊓ g.domain).toScheme)
  (X.homOfLE inf_le_left ≫ f.hom) (X.homOfLE inf_le_right ≫ g.hom) (x := ⟨x, hxf, hxg⟩) ?_

Result:
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

case refine_1
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, ⋯⟩
⊢ (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ f.hom =
    (↑(f.domain ⊓ g.domain)).fromSpecStalk ⟨x, ⋯⟩ ≫ X.homOfLE ⋯ ≫ g.hom