-- 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 neg.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))
y : ↑↑Y.toPresheafedSpace
hy : y ∉ Set.range ⇑(ConcreteCategory.hom f.base)
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hyU : y ∈ ↑U
hU' : ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑U = ∅
⊢ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
convert isAffineOpen_bot _

Result:
case h.e'_2.h
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑(ConcreteCategory.hom f.base)
hf₂ : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
y : ↑↑Y.toPresheafedSpace
hy : y ∉ Set.range ⇑(ConcreteCategory.hom f.base)
U : Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hyU : y ∈ ↑U
hU' : ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑U = ∅
⊢ f ⁻¹ᵁ U = ⊥

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

Tactic:
intro y

Result:
case H
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑(ConcreteCategory.hom f.base)
hf₂ : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
y : ↑↑Y.toPresheafedSpace
⊢ ∃ U, y ∈ 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
⊢ f ⁻¹ᵁ Y.basicOpen r =
    X.basicOpen
      ((ConcreteCategory.hom (Scheme.Hom.app f U')) ((ConcreteCategory.hom (Y.presheaf.map (homOfLE hU'U).op)) r))

Tactic:
simp only [Scheme.preimage_basicOpen, ← CommRingCat.comp_apply, f.naturality]

Result:
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)

Proof state:
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)

Tactic:
refine ⟨_, hxr, hU.basicOpen r, ?_⟩

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
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r)

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

Tactic:
by_cases hy : y ∈ Set.range f.base

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

case neg
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑(ConcreteCategory.hom f.base)
hf₂ : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
y : ↑↑Y.toPresheafedSpace
hy : y ∉ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ ∃ U, y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Proof state:
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

Tactic:
exact ⟨⟨U', hU'⟩ ⊓ U, inf_le_right, Opens.ext (by simpa [e] using hVU)⟩

Result:
no goals

Proof state:
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
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r)

Tactic:
convert hV.basicOpen (f.app _ (Y.presheaf.map (homOfLE hU'U).op r)) using 1

Result:
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
⊢ f ⁻¹ᵁ Y.basicOpen r =
    X.basicOpen
      ((ConcreteCategory.hom (Scheme.Hom.app f U')) ((ConcreteCategory.hom (Y.presheaf.map (homOfLE hU'U).op)) r))