-- 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 = ∅
⊢ ∃ U, y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
refine ⟨U, hyU, hU, ?_⟩

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

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

Tactic:
obtain ⟨x, rfl⟩ := hy

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

Proof state:
case pos.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
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
⊢ ∃ U, (ConcreteCategory.hom f.base) x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
obtain ⟨U', hU'U, rfl⟩ : ∃ U' : Y.Opens, U' ≤ U ∧ f ⁻¹ᵁ U' = V := by
  obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2
  exact ⟨⟨U', hU'⟩ ⊓ U, inf_le_right, Opens.ext (by simpa [e] using hVU)⟩

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

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

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
  (isBasis_affine_open X).exists_subset_of_mem_open hxU (f ⁻¹ᵁ U).isOpen

Result:
case pos.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
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
⊢ ∃ U, (ConcreteCategory.hom f.base) x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

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

Tactic:
exact Opens.ext hU'

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑(ConcreteCategory.hom f.base)
hf₂ : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
⊢ IsAffineHom f

Tactic:
apply isAffineHom_of_forall_exists_isAffineOpen

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

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' : Set ↑↑Y.toPresheafedSpace
hU' : IsOpen U'
e : ⇑(ConcreteCategory.hom f.base) ⁻¹' U' = V.carrier
⊢ ↑(f ⁻¹ᵁ ({ carrier := U', is_open' := hU' } ⊓ U)) = ↑V

Tactic:
simpa [e] using hVU

Result:
no goals

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

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hyU, hU'⟩ :=
  (isBasis_affine_open Y).exists_subset_of_mem_open hy hf₂.isOpen_compl

Result:
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' : ↑U ⊆ (Set.range ⇑(ConcreteCategory.hom f.base))ᶜ
⊢ ∃ U, y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

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' : ↑U ⊆ (Set.range ⇑(ConcreteCategory.hom f.base))ᶜ
⊢ ∃ U, y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
rw [Set.subset_compl_iff_disjoint_right, ← Set.preimage_eq_empty_iff] at hU'

Result:
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 = ∅
⊢ ∃ U, y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)