-- Mathlib/AlgebraicGeometry/Morphisms/Affine.lean
/-- If the underlying map of a morphism is inducing and has closed range, then it is affine. -/
@[stacks 04DE]
lemma isAffineHom_of_isInducing
    (hf₁ : Topology.IsInducing f.base)
    (hf₂ : IsClosed (Set.range f.base)) :
    IsAffineHom f

Proof state:
case pos.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑(ConcreteCategory.hom f.base)
hf₂ : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
x : ↑↑X.toPresheafedSpace
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ ↑(f ⁻¹ᵁ U')
hVU : ↑(f ⁻¹ᵁ U') ⊆ ↑(f ⁻¹ᵁ U)
⊢ ∃ U, (ConcreteCategory.hom f.base) x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
obtain ⟨r, hrU', hxr⟩ := hU.exists_basicOpen_le ⟨f.base x, hxV⟩ hxU

Result:
case pos.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑(ConcreteCategory.hom f.base)
hf₂ : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
x : ↑↑X.toPresheafedSpace
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ ↑(f ⁻¹ᵁ U')
hVU : ↑(f ⁻¹ᵁ U') ⊆ ↑(f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
hrU' : Y.basicOpen r ≤ U'
hxr : ↑⟨(ConcreteCategory.hom f.base) x, hxV⟩ ∈ Y.basicOpen r
⊢ ∃ U, (ConcreteCategory.hom f.base) x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Proof state:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑(ConcreteCategory.hom f.base)
hf₂ : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
x : ↑↑X.toPresheafedSpace
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
⊢ ∃ U' ≤ U, f ⁻¹ᵁ U' = V

Tactic:
obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2

Result:
case intro.intro
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑(ConcreteCategory.hom f.base)
hf₂ : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
x : ↑↑X.toPresheafedSpace
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
U' : Set ↑↑Y.toPresheafedSpace
hU' : IsOpen U'
e : ⇑(ConcreteCategory.hom f.base) ⁻¹' U' = V.carrier
⊢ ∃ U' ≤ U, f ⁻¹ᵁ U' = V

Proof state:
case pos.intro
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑(ConcreteCategory.hom f.base)
hf₂ : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
x : ↑↑X.toPresheafedSpace
⊢ ∃ U, (ConcreteCategory.hom f.base) x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
  (isBasis_affine_open Y).exists_subset_of_mem_open (Set.mem_univ (f.base x)) isOpen_univ

Result:
case pos.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑(ConcreteCategory.hom f.base)
hf₂ : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
x : ↑↑X.toPresheafedSpace
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
⊢ ∃ U, (ConcreteCategory.hom f.base) x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Proof state:
case h.e'_2
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑(ConcreteCategory.hom f.base)
hf₂ : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
x : ↑↑X.toPresheafedSpace
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ ↑(f ⁻¹ᵁ U')
hVU : ↑(f ⁻¹ᵁ U') ⊆ ↑(f ⁻¹ᵁ U)
r : ↑Γ(Y, U)
hrU' : Y.basicOpen r ≤ U'
hxr : ↑⟨(ConcreteCategory.hom f.base) x, hxV⟩ ∈ Y.basicOpen r
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f U)) r) =
    X.basicOpen
      ((ConcreteCategory.hom (Scheme.Hom.app f U ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE hU'U).op.unop).op))
        r)

Tactic:
simpa using ((Opens.map f.base).map (homOfLE hrU')).le

Result:
no goals