-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma PartialMap.toPartialMap_toRationalMap_restrict [IsReduced X] [Y.IsSeparated]
    (f : X.PartialMap Y) : (f.toRationalMap.toPartialMap.restrict _ f.dense_domain
      f.le_domain_toRationalMap).hom = f.hom

Proof state:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom = f.hom

Tactic:
generalize_proofs _ _ H _

Result:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
pf✝² : f.domain ∈ {x | ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = x}
pf✝¹ : ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = f.domain
H : ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = ↑⟨f.domain, pf✝¹⟩
pf✝ : H.choose.domain = ↑⟨f.domain, pf✝²⟩
⊢ (X.isoOfEq pf✝).inv ≫ H.choose.hom = f.hom

Proof state:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
pf✝² : f.domain ∈ {x | ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = x}
pf✝¹ : ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = f.domain
H : ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = ↑⟨f.domain, pf✝¹⟩
pf✝ : H.choose.domain = ↑⟨f.domain, pf✝²⟩
this : H.choose = f
⊢ (X.isoOfEq pf✝).inv ≫ H.choose.hom = f.hom

Tactic:
exact ((ext_iff _ _).mp this.symm).choose_spec.symm

Result:
no goals

Proof state:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ X.homOfLE ⋯ ≫
      Cover.glueMorphisms f.toRationalMap.openCoverDomain (fun x => (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom) ⋯ =
    f.hom

Tactic:
refine (f.toRationalMap.openCoverDomain.ι_glueMorphisms _ _ ⟨_, f, rfl, rfl⟩).trans ?_

Result:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom = f.hom

Proof state:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).hom = f.hom

Tactic:
dsimp [RationalMap.toPartialMap]

Result:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ X.homOfLE ⋯ ≫
      Cover.glueMorphisms f.toRationalMap.openCoverDomain (fun x => (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom) ⋯ =
    f.hom

Proof state:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
pf✝² : f.domain ∈ {x | ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = x}
pf✝¹ : ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = f.domain
H : ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = ↑⟨f.domain, pf✝¹⟩
pf✝ : H.choose.domain = ↑⟨f.domain, pf✝²⟩
⊢ (X.isoOfEq pf✝).inv ≫ H.choose.hom = f.hom

Tactic:
have : H.choose = f := (equiv_iff_of_domain_eq_of_isSeparated (S := ⊤_ _) H.choose_spec.2).mp
  (toRationalMap_eq_iff.mp H.choose_spec.1)

Result:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
pf✝² : f.domain ∈ {x | ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = x}
pf✝¹ : ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = f.domain
H : ∃ g, ∃ (_ : g.toRationalMap = f.toRationalMap), g.domain = ↑⟨f.domain, pf✝¹⟩
pf✝ : H.choose.domain = ↑⟨f.domain, pf✝²⟩
this : H.choose = f
⊢ (X.isoOfEq pf✝).inv ≫ H.choose.hom = f.hom