-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma PartialMap.isOver_toRationalMap_iff_of_isSeparated [X.Over S] [Y.Over S] [IsReduced X]
    [S.IsSeparated] {f : X.PartialMap Y} :
    f.toRationalMap.IsOver S ↔ f.IsOver S

Proof state:
X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
⊢ RationalMap.IsOver S f.toRationalMap ↔ IsOver S f

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Result:
X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
⊢ IsOver S f

Proof state:
case intro.intro.intro
X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
⊢ IsOver S f

Tactic:
rw [isOver_iff]

Result:
case intro.intro.intro
X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
⊢ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S

Proof state:
X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
⊢ IsOver S f

Tactic:
obtain ⟨U, hU, hU', H⟩ := f.exists_restrict_isOver (S := S)

Result:
case intro.intro.intro
X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
⊢ IsOver S f

Proof state:
X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
this : IsDominant (X.homOfLE hU')
⊢ X.homOfLE hU' ≫ (f.compHom (Y ↘ S)).hom = X.homOfLE hU' ≫ f.domain.ι ≫ X ↘ S

Tactic:
simpa using H.1

Result:
no goals

Proof state:
case intro.intro.intro
X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
this : IsDominant (X.homOfLE hU')
⊢ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S

Tactic:
exact ext_of_isDominant (ι := X.homOfLE hU') (by simpa using H.1)

Result:
no goals

Proof state:
case intro.intro.intro
X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
⊢ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S

Tactic:
have : IsDominant (X.homOfLE hU') := Opens.isDominant_homOfLE hU _

Result:
case intro.intro.intro
X Y S : Scheme
inst✝³ : X.Over S
inst✝² : Y.Over S
inst✝¹ : IsReduced X
inst✝ : S.IsSeparated
f : X.PartialMap Y
x✝ : RationalMap.IsOver S f.toRationalMap
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
H : IsOver S (f.restrict U hU hU')
this : IsDominant (X.homOfLE hU')
⊢ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S