-- Mathlib/AlgebraicGeometry/RationalMap.lean
/-- Two partial maps from reduced schemes to separated schemes with the same domain are equivalent
if and only if they are equal. -/
lemma equiv_iff_of_domain_eq_of_isSeparated [X.Over S] [Y.Over S] [IsReduced X]
    [IsSeparated (Y ↘ S)] {f g : X.PartialMap Y} (hfg : f.domain = g.domain)
    [f.IsOver S] [g.IsOver S] : f.equiv g ↔ f = g

Proof state:
case mk.mk
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
Uf : X.Opens
dense_domain✝¹ : Dense ↑Uf
f : ↑Uf ⟶ Y
inst✝¹ : IsOver S { domain := Uf, dense_domain := dense_domain✝¹, hom := f }
dense_domain✝ : Dense ↑Uf
g : ↑Uf ⟶ Y
inst✝ : IsOver S { domain := Uf, dense_domain := dense_domain✝, hom := g }
⊢ ({ domain := Uf, dense_domain := dense_domain✝¹, hom := f }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom =
      ({ domain := Uf, dense_domain := dense_domain✝, hom := g }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain✝¹, hom := f } =
      { domain := Uf, dense_domain := dense_domain✝, hom := g }

Tactic:
simp

Result:
no goals

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
hfg : f.domain = g.domain
inst✝¹ : IsOver S f
inst✝ : IsOver S g
⊢ (f.restrict f.domain ⋯ ⋯).hom = (g.restrict f.domain ⋯ ⋯).hom ↔ f = g

Tactic:
obtain ⟨Uf, _, f⟩ := f

Result:
case mk
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
g : X.PartialMap Y
inst✝¹ : IsOver S g
Uf : X.Opens
dense_domain✝ : Dense ↑Uf
f : ↑Uf ⟶ Y
hfg : { domain := Uf, dense_domain := dense_domain✝, hom := f }.domain = g.domain
inst✝ : IsOver S { domain := Uf, dense_domain := dense_domain✝, hom := f }
⊢ ({ domain := Uf, dense_domain := dense_domain✝, hom := f }.restrict
          { domain := Uf, dense_domain := dense_domain✝, hom := f }.domain ⋯ ⋯).hom =
      (g.restrict { domain := Uf, dense_domain := dense_domain✝, hom := f }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain✝, hom := f } = g

Proof state:
case mk
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
g : X.PartialMap Y
inst✝¹ : IsOver S g
Uf : X.Opens
dense_domain✝ : Dense ↑Uf
f : ↑Uf ⟶ Y
hfg : { domain := Uf, dense_domain := dense_domain✝, hom := f }.domain = g.domain
inst✝ : IsOver S { domain := Uf, dense_domain := dense_domain✝, hom := f }
⊢ ({ domain := Uf, dense_domain := dense_domain✝, hom := f }.restrict
          { domain := Uf, dense_domain := dense_domain✝, hom := f }.domain ⋯ ⋯).hom =
      (g.restrict { domain := Uf, dense_domain := dense_domain✝, hom := f }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain✝, hom := f } = g

Tactic:
obtain ⟨Ug, _, g⟩ := g

Result:
case mk.mk
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
Uf : X.Opens
dense_domain✝¹ : Dense ↑Uf
f : ↑Uf ⟶ Y
inst✝¹ : IsOver S { domain := Uf, dense_domain := dense_domain✝¹, hom := f }
Ug : X.Opens
dense_domain✝ : Dense ↑Ug
g : ↑Ug ⟶ Y
inst✝ : IsOver S { domain := Ug, dense_domain := dense_domain✝, hom := g }
hfg :
  { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain =
    { domain := Ug, dense_domain := dense_domain✝, hom := g }.domain
⊢ ({ domain := Uf, dense_domain := dense_domain✝¹, hom := f }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom =
      ({ domain := Ug, dense_domain := dense_domain✝, hom := g }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain✝¹, hom := f } =
      { domain := Ug, dense_domain := dense_domain✝, hom := g }

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
hfg : f.domain = g.domain
inst✝¹ : IsOver S f
inst✝ : IsOver S g
⊢ f.equiv g ↔ f = g

Tactic:
rw [equiv_iff_of_isSeparated_of_le (S := S) f.dense_domain le_rfl hfg.le]

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
hfg : f.domain = g.domain
inst✝¹ : IsOver S f
inst✝ : IsOver S g
⊢ (f.restrict f.domain ⋯ ⋯).hom = (g.restrict f.domain ⋯ ⋯).hom ↔ f = g

Proof state:
case mk.mk
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
Uf : X.Opens
dense_domain✝¹ : Dense ↑Uf
f : ↑Uf ⟶ Y
inst✝¹ : IsOver S { domain := Uf, dense_domain := dense_domain✝¹, hom := f }
Ug : X.Opens
dense_domain✝ : Dense ↑Ug
g : ↑Ug ⟶ Y
inst✝ : IsOver S { domain := Ug, dense_domain := dense_domain✝, hom := g }
hfg :
  { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain =
    { domain := Ug, dense_domain := dense_domain✝, hom := g }.domain
⊢ ({ domain := Uf, dense_domain := dense_domain✝¹, hom := f }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom =
      ({ domain := Ug, dense_domain := dense_domain✝, hom := g }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain✝¹, hom := f } =
      { domain := Ug, dense_domain := dense_domain✝, hom := g }

Tactic:
obtain rfl : Uf = Ug := hfg

Result:
case mk.mk
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
Uf : X.Opens
dense_domain✝¹ : Dense ↑Uf
f : ↑Uf ⟶ Y
inst✝¹ : IsOver S { domain := Uf, dense_domain := dense_domain✝¹, hom := f }
dense_domain✝ : Dense ↑Uf
g : ↑Uf ⟶ Y
inst✝ : IsOver S { domain := Uf, dense_domain := dense_domain✝, hom := g }
⊢ ({ domain := Uf, dense_domain := dense_domain✝¹, hom := f }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom =
      ({ domain := Uf, dense_domain := dense_domain✝, hom := g }.restrict
          { domain := Uf, dense_domain := dense_domain✝¹, hom := f }.domain ⋯ ⋯).hom ↔
    { domain := Uf, dense_domain := dense_domain✝¹, hom := f } =
      { domain := Uf, dense_domain := dense_domain✝, hom := g }