[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ @LocallyOfFiniteType = affineLocally @RingHom.FiniteType
[PROOFSTEP]
ext X Y f
[GOAL]
case h.h.h.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ LocallyOfFiniteType f ↔ affineLocally (@RingHom.FiniteType) f
[PROOFSTEP]
rw [LocallyOfFiniteType_iff, affineLocally_iff_affineOpens_le]
[GOAL]
case h.h.h.a.hP
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ RingHom.RespectsIso @RingHom.FiniteType
[PROOFSTEP]
exact RingHom.finiteType_respectsIso
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : LocallyOfFiniteType (f ≫ g)
⊢ LocallyOfFiniteType f
[PROOFSTEP]
revert hf
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ [hf : LocallyOfFiniteType (f ≫ g)], LocallyOfFiniteType f
[PROOFSTEP]
rw [locallyOfFiniteType_eq]
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ [hf : affineLocally (@RingHom.FiniteType) (f ≫ g)], affineLocally (@RingHom.FiniteType) f
[PROOFSTEP]
apply RingHom.finiteType_is_local.affineLocally_of_comp
[GOAL]
case H
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {R S T : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    RingHom.FiniteType (RingHom.comp g f) → RingHom.FiniteType g
[PROOFSTEP]
introv H
[GOAL]
case H
X✝ Y✝ : Scheme
f✝¹ : X✝ ⟶ Y✝
X Y Z : Scheme
f✝ : X ⟶ Y
g✝ : Y ⟶ Z
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
H : RingHom.FiniteType (RingHom.comp g f)
⊢ RingHom.FiniteType g
[PROOFSTEP]
exact RingHom.FiniteType.of_comp_finiteType H
