-- Mathlib/AlgebraicGeometry/FunctionField.lean
theorem genericPoint_eq_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f]
    [hX : IrreducibleSpace X] [IrreducibleSpace Y] :
    f.base (genericPoint X) = genericPoint Y

Proof state:
case h.e'_4.h.e'_3
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ ⇑(ConcreteCategory.hom f.base) '' Set.univ = Set.univ ∩ Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.toLRSHom f).base)

Tactic:
rw [Set.univ_inter, Set.image_univ]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ IsGenericPoint ((ConcreteCategory.hom f.base) (genericPoint ↑↑X.toPresheafedSpace)) Set.univ

Tactic:
convert (genericPoint_spec X).image (show Continuous f.base by fun_prop)

Result:
case h.e'_4
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ Set.univ = closure (⇑(ConcreteCategory.hom f.base) '' Set.univ)

Proof state:
case h.e'_4
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ Set.univ ⊆ closure (⇑(ConcreteCategory.hom f.base) '' Set.univ)

Tactic:
convert subset_closure_inter_of_isPreirreducible_of_isOpen _ H.base_open.isOpen_range _

Result:
case h.e'_4.h.e'_3
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ ⇑(ConcreteCategory.hom f.base) '' Set.univ = Set.univ ∩ Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.toLRSHom f).base)

case h.e'_4.convert_2
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ IsPreirreducible Set.univ

case h.e'_4.convert_3
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ (Set.univ ∩ Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.toLRSHom f).base)).Nonempty

Proof state:
case h.e'_4.convert_2
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ IsPreirreducible Set.univ

Tactic:
apply PreirreducibleSpace.isPreirreducible_univ (X := Y)

Result:
no goals

Proof state:
case h.e'_4
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ closure (⇑(ConcreteCategory.hom f.base) '' Set.univ) = Set.univ

Tactic:
rw [← Set.univ_subset_iff]

Result:
case h.e'_4
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ Set.univ ⊆ closure (⇑(ConcreteCategory.hom f.base) '' Set.univ)

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom f.base) (genericPoint ↑↑X.toPresheafedSpace) = genericPoint ↑↑Y.toPresheafedSpace

Tactic:
apply ((genericPoint_spec Y).eq _).symm

Result:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ IsGenericPoint ((ConcreteCategory.hom f.base) (genericPoint ↑↑X.toPresheafedSpace)) Set.univ

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ Continuous ⇑(ConcreteCategory.hom f.base)

Tactic:
fun_prop

Result:
no goals

Proof state:
case h.e'_4.convert_3
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ (Set.univ ∩ Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.toLRSHom f).base)).Nonempty

Tactic:
exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩

Result:
no goals

Proof state:
case h.e'_4
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ Set.univ = closure (⇑(ConcreteCategory.hom f.base) '' Set.univ)

Tactic:
symm

Result:
case h.e'_4
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
hX : IrreducibleSpace ↑↑X.toPresheafedSpace
inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace
⊢ closure (⇑(ConcreteCategory.hom f.base) '' Set.univ) = Set.univ