-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma RationalMap.isOver_iff [X.Over S] [Y.Over S] {f : X ⤏ Y} :
    f.IsOver S ↔ f.compHom (Y ↘ S) = (X ↘ S).toRationalMap

Proof state:
case mpr.intro.intro.intro.intro.intro
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
e✝ : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
U : X.Opens
hU : Dense ↑U
hUl : U ≤ ((fun x => x.compHom (Y ↘ S)) f).domain
hUr : U ≤ (Hom.toPartialMap (X ↘ S)).domain
e : (((fun x => x.compHom (Y ↘ S)) f).restrict U hU hUl).hom = ((Hom.toPartialMap (X ↘ S)).restrict U hU hUr).hom
⊢ IsOver S f.toRationalMap

Tactic:
exact ⟨⟨f.restrict U hU hUl, by simpa using e, by simp⟩⟩

Result:
no goals

Proof state:
case mpr
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) → IsOver S f

Tactic:
intro e

Result:
case mpr
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
e : f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
⊢ IsOver S f

Proof state:
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
e✝ : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
U : X.Opens
hU : Dense ↑U
hUl : U ≤ ((fun x => x.compHom (Y ↘ S)) f).domain
hUr : U ≤ (Hom.toPartialMap (X ↘ S)).domain
e : (((fun x => x.compHom (Y ↘ S)) f).restrict U hU hUl).hom = ((Hom.toPartialMap (X ↘ S)).restrict U hU hUr).hom
⊢ (f.restrict U hU hUl).toRationalMap = f.toRationalMap

Tactic:
simp

Result:
no goals

Proof state:
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
e✝ : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
U : X.Opens
hU : Dense ↑U
hUl : U ≤ ((fun x => x.compHom (Y ↘ S)) f).domain
hUr : U ≤ (Hom.toPartialMap (X ↘ S)).domain
e : (((fun x => x.compHom (Y ↘ S)) f).restrict U hU hUl).hom = ((Hom.toPartialMap (X ↘ S)).restrict U hU hUr).hom
⊢ PartialMap.IsOver S (f.restrict U hU hUl)

Tactic:
simpa using e

Result:
no goals

Proof state:
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
⊢ IsOver S f ↔ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Tactic:
constructor

Result:
case mp
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
⊢ IsOver S f → f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

case mpr
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S) → IsOver S f

Proof state:
case mp.intro.intro
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
h : IsOver S f
g : X.PartialMap Y
hg : PartialMap.IsOver S g
e : g.toRationalMap = f
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Tactic:
rw [← e, Hom.toRationalMap, ← compHom_toRationalMap, PartialMap.isOver_iff_eq_restrict.mp hg,
  PartialMap.restrict_toRationalMap]

Result:
no goals

Proof state:
case mp
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
h : IsOver S f
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Tactic:
obtain ⟨g, hg, e⟩ := f.exists_partialMap_over S

Result:
case mp.intro.intro
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
h : IsOver S f
g : X.PartialMap Y
hg : PartialMap.IsOver S g
e : g.toRationalMap = f
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Proof state:
case mpr.intro
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
e : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
⊢ IsOver S f.toRationalMap

Tactic:
obtain ⟨U, hU, hUl, hUr, e⟩ := PartialMap.toRationalMap_eq_iff.mp e

Result:
case mpr.intro.intro.intro.intro.intro
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
e✝ : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
U : X.Opens
hU : Dense ↑U
hUl : U ≤ ((fun x => x.compHom (Y ↘ S)) f).domain
hUr : U ≤ (Hom.toPartialMap (X ↘ S)).domain
e : (((fun x => x.compHom (Y ↘ S)) f).restrict U hU hUl).hom = ((Hom.toPartialMap (X ↘ S)).restrict U hU hUr).hom
⊢ IsOver S f.toRationalMap

Proof state:
case mp
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
⊢ IsOver S f → f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Tactic:
intro h

Result:
case mp
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
h : IsOver S f
⊢ f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)

Proof state:
case mpr
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X ⤏ Y
e : f.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
⊢ IsOver S f

Tactic:
obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f

Result:
case mpr.intro
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
e : f.toRationalMap.compHom (Y ↘ S) = Hom.toRationalMap (X ↘ S)
⊢ IsOver S f.toRationalMap