-- Mathlib/AlgebraicGeometry/RationalMap.lean
/-- Two partial maps from reduced schemes to separated schemes are equivalent if and only if
they are equal on **any** open dense subset. -/
lemma equiv_iff_of_isSeparated_of_le [X.Over S] [Y.Over S] [IsReduced X]
    [IsSeparated (Y ↘ S)] {f g : X.PartialMap Y} [f.IsOver S] [g.IsOver S]
    {W : X.Opens} (hW : Dense (X := X) W) (hWl : W ≤ f.domain) (hWr : W ≤ g.domain) : f.equiv g ↔
      (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Proof state:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
inst✝¹ : IsOver S f
inst✝ : IsOver S g
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
x✝ : f.equiv g
V : X.Opens
hV : Dense ↑V
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
this : IsDominant (X.homOfLE ⋯)
⊢ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Tactic:
apply ext_of_isDominant_of_isSeparated' S (X.homOfLE (inf_le_left : W ⊓ V ≤ W))

Result:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
inst✝¹ : IsOver S f
inst✝ : IsOver S g
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
x✝ : f.equiv g
V : X.Opens
hV : Dense ↑V
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
this : IsDominant (X.homOfLE ⋯)
⊢ X.homOfLE ⋯ ≫ (f.restrict W hW hWl).hom = X.homOfLE ⋯ ≫ (g.restrict W hW hWr).hom

Proof state:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
inst✝¹ : IsOver S f
inst✝ : IsOver S g
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
⊢ f.equiv g ↔ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Tactic:
refine ⟨fun ⟨V, hV, hVl, hVr, e⟩ ↦ ?_, fun e ↦ ⟨_, _, _, _, e⟩⟩

Result:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
inst✝¹ : IsOver S f
inst✝ : IsOver S g
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
x✝ : f.equiv g
V : X.Opens
hV : Dense ↑V
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
⊢ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Proof state:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
inst✝¹ : IsOver S f
inst✝ : IsOver S g
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
x✝ : f.equiv g
V : X.Opens
hV : Dense ↑V
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
⊢ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Tactic:
have : IsDominant (X.homOfLE (inf_le_left : W ⊓ V ≤ W)) :=
  Opens.isDominant_homOfLE (hW.inter_of_isOpen_left hV W.2) _

Result:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
inst✝¹ : IsOver S f
inst✝ : IsOver S g
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
x✝ : f.equiv g
V : X.Opens
hV : Dense ↑V
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
this : IsDominant (X.homOfLE ⋯)
⊢ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Proof state:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f g : X.PartialMap Y
inst✝¹ : IsOver S f
inst✝ : IsOver S g
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
x✝ : f.equiv g
V : X.Opens
hV : Dense ↑V
hVl : V ≤ f.domain
hVr : V ≤ g.domain
e : (f.restrict V hV hVl).hom = (g.restrict V hV hVr).hom
this : IsDominant (X.homOfLE ⋯)
⊢ X.homOfLE ⋯ ≫ (f.restrict W hW hWl).hom = X.homOfLE ⋯ ≫ (g.restrict W hW hWr).hom

Tactic:
simpa using congr(X.homOfLE (inf_le_right : W ⊓ V ≤ V) ≫ $e)

Result:
no goals