-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
theorem isAffine_surjective_of_isAffine [IsClosedImmersion f] :
    IsAffine X ∧ Function.Surjective (f.appTop)

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

Tactic:
rw [← affineTargetImageFactorization_comp f] at i ⊢

Result:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
i : IsClosedImmersion (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)
⊢ IsAffine X ∧
    Function.Surjective
      ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)))

Proof state:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
i : IsClosedImmersion (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)
this : IsClosedImmersion (affineTargetImageInclusion f)
⊢ IsAffine X ∧
    Function.Surjective
      ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)))

Tactic:
haveI := IsClosedImmersion.of_comp_isClosedImmersion (affineTargetImageFactorization f)
  (affineTargetImageInclusion f)

Result:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
i : IsClosedImmersion (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)
this✝ : IsClosedImmersion (affineTargetImageInclusion f)
this : IsClosedImmersion (affineTargetImageFactorization f)
⊢ IsAffine X ∧
    Function.Surjective
      ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)))

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

Tactic:
haveI i : IsClosedImmersion f := inferInstance

Result:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ i : IsClosedImmersion f
⊢ IsAffine X ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Proof state:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
i : IsClosedImmersion (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)
this✝¹ : IsClosedImmersion (affineTargetImageInclusion f)
this✝ : IsClosedImmersion (affineTargetImageFactorization f)
this : IsIso (affineTargetImageFactorization f)
⊢ IsAffine X ∧
    Function.Surjective
      ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)))

Tactic:
exact ⟨isAffine_of_isIso (affineTargetImageFactorization f),
  (ConcreteCategory.bijective_of_isIso
    ((affineTargetImageFactorization f).appTop)).surjective.comp <|
    affineTargetImageInclusion_app_surjective f⟩

Result:
no goals

Proof state:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
i : IsClosedImmersion (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)
⊢ IsAffine X ∧
    Function.Surjective
      ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)))

Tactic:
haveI := of_surjective_of_isAffine (affineTargetImageInclusion f)
  (affineTargetImageInclusion_app_surjective f)

Result:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
i : IsClosedImmersion (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)
this : IsClosedImmersion (affineTargetImageInclusion f)
⊢ IsAffine X ∧
    Function.Surjective
      ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)))

Proof state:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
i : IsClosedImmersion (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)
this✝ : IsClosedImmersion (affineTargetImageInclusion f)
this : IsClosedImmersion (affineTargetImageFactorization f)
⊢ IsAffine X ∧
    Function.Surjective
      ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)))

Tactic:
haveI := isIso_of_injective_of_isAffine (affineTargetImageFactorization_app_injective f)

Result:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
i : IsClosedImmersion (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)
this✝¹ : IsClosedImmersion (affineTargetImageInclusion f)
this✝ : IsClosedImmersion (affineTargetImageFactorization f)
this : IsIso (affineTargetImageFactorization f)
⊢ IsAffine X ∧
    Function.Surjective
      ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (affineTargetImageFactorization f ≫ affineTargetImageInclusion f)))