-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma affineTargetImageInclusion_app_surjective :
    Function.Surjective <| (affineTargetImageInclusion f).appTop

Proof state:
case hf.hf
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Function.Bijective ⇑(CommRingCat.Hom.hom (Scheme.Hom.app Y.isoSpec.inv ⊤))

Tactic:
exact ConcreteCategory.bijective_of_isIso (Scheme.Hom.app Y.isoSpec.inv ⊤)

Result:
no goals

Proof state:
case hg
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (specTargetImageRingHom (f ≫ Y.isoSpec.hom))) ⊤))

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff
  (toMorphismProperty (fun f ↦ Function.Surjective f))
  (arrowIsoΓSpecOfIsAffine (specTargetImageRingHom (f ≫ Y.isoSpec.hom))).symm).mpr <|
    specTargetImageRingHom_surjective (f ≫ Y.isoSpec.hom)

Result:
no goals

Proof state:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Function.Surjective
    (⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (specTargetImageRingHom (f ≫ Y.isoSpec.hom))) ⊤)) ∘
      ⇑(CommRingCat.Hom.hom (Scheme.Hom.app Y.isoSpec.inv ⊤)))

Tactic:
apply Function.Surjective.comp

Result:
case hg
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (specTargetImageRingHom (f ≫ Y.isoSpec.hom))) ⊤))

case hf
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (Scheme.Hom.app Y.isoSpec.inv ⊤))

Proof state:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f

Tactic:
exact surjective_respectsIso

Result:
no goals

Proof state:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (affineTargetImageInclusion f)))

Tactic:
simp only [Scheme.comp_coeBase, Opens.map_comp_obj, Opens.map_top, Scheme.comp_app,
  CommRingCat.hom_comp, affineTargetImageInclusion, RingHom.coe_comp]

Result:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Function.Surjective
    (⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (specTargetImageRingHom (f ≫ Y.isoSpec.hom))) ⊤)) ∘
      ⇑(CommRingCat.Hom.hom (Scheme.Hom.app Y.isoSpec.inv ⊤)))

Proof state:
case hf
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (Scheme.Hom.app Y.isoSpec.inv ⊤))

Tactic:
apply Function.Bijective.surjective

Result:
case hf.hf
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Function.Bijective ⇑(CommRingCat.Hom.hom (Scheme.Hom.app Y.isoSpec.inv ⊤))

Proof state:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso

Tactic:
rw [← toMorphismProperty_respectsIso_iff]

Result:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f

Proof state:
case hg
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (specTargetImageRingHom (f ≫ Y.isoSpec.hom))) ⊤))

Tactic:
haveI : (toMorphismProperty (fun f ↦ Function.Surjective f)).RespectsIso := by
  rw [← toMorphismProperty_respectsIso_iff]
  exact surjective_respectsIso

Result:
case hg
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (specTargetImageRingHom (f ≫ Y.isoSpec.hom))) ⊤))