-- Mathlib/AlgebraicGeometry/Morphisms/Finite.lean
lemma _root_.AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono :
    IsClosedImmersion f ↔ IsFinite f ∧ Mono f

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

Tactic:
show _ ↔ _ ∧ monomorphisms _ f

Result:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ monomorphisms Scheme f

Proof state:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
x✝ : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left✝ : IsAffine X
right✝ : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
⊢ Mono (Scheme.Hom.app f ⊤).op ↔ monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f))

Tactic:
exact (Functor.mono_map_iff_mono Scheme.Spec _).symm

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

Tactic:
wlog hY : IsAffine Y

Result:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

Proof state:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Epi (Scheme.Hom.appTop f) ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Mono f

Tactic:
refine and_congr_right fun ⟨_, _⟩ ↦
  Iff.trans ?_ (arrow_mk_iso_iff (monomorphisms _) (arrowIsoSpecΓOfIsAffine f).symm)

Result:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
x✝ : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left✝ : IsAffine X
right✝ : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
⊢ Epi (Scheme.Hom.appTop f) ↔ monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f))

Proof state:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ Mono f

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @IsClosedImmersion),
  HasAffineProperty.iff_of_isAffine (P := @IsFinite),
  RingHom.surjective_iff_epi_and_finite, @and_comm (Epi _), ← and_assoc]

Result:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Epi (Scheme.Hom.appTop f) ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite) ∧ Mono f

Proof state:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
x✝ : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left✝ : IsAffine X
right✝ : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
⊢ Epi (Scheme.Hom.appTop f) ↔ Mono (Scheme.Hom.app f ⊤).op

Tactic:
exact ⟨fun h ↦ inferInstance, fun h ↦ show Epi (f.app ⊤).op.unop by infer_instance⟩

Result:
no goals

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.1), IsClosedImmersion (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.1), monomorphisms Scheme (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
simp_rw [this, forall_and, monomorphisms]

Result:
no goals

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ monomorphisms Scheme f

Tactic:
rw [IsLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
  IsLocalAtTarget.iff_of_openCover (P := @IsClosedImmersion) Y.affineCover,
  IsLocalAtTarget.iff_of_openCover (P := monomorphisms _) Y.affineCover]

Result:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.1), IsClosedImmersion (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.1), monomorphisms Scheme (Scheme.Cover.pullbackHom Y.affineCover f i)

Proof state:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
x✝ : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left✝ : IsAffine X
right✝ : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
h : Mono (Scheme.Hom.app f ⊤).op
⊢ Epi (Scheme.Hom.app f ⊤).op.unop

Tactic:
infer_instance

Result:
no goals

Proof state:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
x✝ : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left✝ : IsAffine X
right✝ : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
⊢ Epi (Scheme.Hom.appTop f) ↔ monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f))

Tactic:
trans Mono (f.app ⊤).op

Result:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
x✝ : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left✝ : IsAffine X
right✝ : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
⊢ Epi (Scheme.Hom.appTop f) ↔ Mono (Scheme.Hom.app f ⊤).op

X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
x✝ : IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
left✝ : IsAffine X
right✝ : (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
⊢ Mono (Scheme.Hom.app f ⊤).op ↔ monomorphisms Scheme (Spec.map (Scheme.Hom.appTop f))