-- Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean
/-- The diagonal of a formally unramified morphism of finite type is an open immersion. -/
lemma AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal {X Y : Scheme.{u}} (f : X ⟶ Y)
    [FormallyUnramified f] [LocallyOfFiniteType f] : IsOpenImmersion (pullback.diagonal f)

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : FormallyUnramified f] [inst : LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
⊢ IsOpenImmersion (pullback.diagonal f)

Tactic:
let 𝒰Y := Y.affineCover

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : FormallyUnramified f] [inst : LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
⊢ IsOpenImmersion (pullback.diagonal f)

Proof state:
case intro.intro.intro.intro
S R : CommRingCat
f : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom f).FormallyUnramified
inst✝ : (CommRingCat.Hom.hom f).FiniteType
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝¹ : Algebra.FormallyUnramified ↑R ↑S
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' ↑R).toRingHom))

Tactic:
infer_instance

Result:
no goals

Proof state:
case intro.intro.intro.intro
S R : CommRingCat
f : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom f).FormallyUnramified
inst✝ : (CommRingCat.Hom.hom f).FiniteType
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝¹ : Algebra.FormallyUnramified ↑R ↑S
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
⊢ IsOpenImmersion (pullback.diagonal (Spec.map f))

Tactic:
rw [show f = CommRingCat.ofHom (algebraMap R S) from rfl, diagonal_Spec_map R S,
  cancel_right_of_respectsIso (P := @IsOpenImmersion)]

Result:
case intro.intro.intro.intro
S R : CommRingCat
f : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom f).FormallyUnramified
inst✝ : (CommRingCat.Hom.hom f).FiniteType
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝¹ : Algebra.FormallyUnramified ↑R ↑S
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' ↑R).toRingHom))

Proof state:
case intro.intro.intro
S R : CommRingCat
f : Spec S ⟶ Spec R
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
⊢ IsOpenImmersion (pullback.diagonal f)

Tactic:
obtain ⟨f, rfl⟩ := Spec.map_surjective f

Result:
case intro.intro.intro.intro
S R : CommRingCat
f : R ⟶ S
inst✝¹ : FormallyUnramified (Spec.map f)
inst✝ : LocallyOfFiniteType (Spec.map f)
⊢ IsOpenImmersion (pullback.diagonal (Spec.map f))

Proof state:
case intro.intro.intro.intro
S R : CommRingCat
f : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom f).FormallyUnramified
inst✝ : (CommRingCat.Hom.hom f).FiniteType
⊢ IsOpenImmersion (pullback.diagonal (Spec.map f))

Tactic:
algebraize [f.hom]

Result:
case intro.intro.intro.intro
S R : CommRingCat
f : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom f).FormallyUnramified
inst✝ : (CommRingCat.Hom.hom f).FiniteType
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝¹ : Algebra.FormallyUnramified ↑R ↑S
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
⊢ IsOpenImmersion (pullback.diagonal (Spec.map f))

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : FormallyUnramified f] [inst : LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Scheme.Cover.pullbackCover Y.affineCover f).J) →
  ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).OpenCover :=
  fun j => ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).affineCover
i : (Scheme.Cover.pullbackCover 𝒰Y f).J
j : (𝒰X i).J
⊢ IsOpenImmersion (pullback.diagonal ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i)))

Tactic:
have hu : FormallyUnramified ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i)) :=
  comp_mem _ _ _ inferInstance (pullback_snd _ _ inferInstance)

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : FormallyUnramified f] [inst : LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Scheme.Cover.pullbackCover Y.affineCover f).J) →
  ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).OpenCover :=
  fun j => ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).affineCover
i : (Scheme.Cover.pullbackCover 𝒰Y f).J
j : (𝒰X i).J
hu : FormallyUnramified ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i))
⊢ IsOpenImmersion (pullback.diagonal ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i)))

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : FormallyUnramified f] [inst : LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Scheme.Cover.pullbackCover Y.affineCover f).J) →
  ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).OpenCover :=
  fun j => ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).affineCover
⊢ IsOpenImmersion (pullback.diagonal f)

Tactic:
apply IsLocalAtTarget.of_range_subset_iSup _
  (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange f 𝒰Y 𝒰X)

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : FormallyUnramified f] [inst : LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Scheme.Cover.pullbackCover Y.affineCover f).J) →
  ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).OpenCover :=
  fun j => ((Scheme.Cover.pullbackCover Y.affineCover f).obj j).affineCover
⊢ ∀ (i : (i : (Scheme.Cover.pullbackCover 𝒰Y f).J) × (𝒰X i).J),
    IsOpenImmersion
      (pullback.diagonal f ∣_
        Scheme.Hom.opensRange ((Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).map ⟨i.fst, (i.snd, i.snd)⟩))

Proof state:
case intro.intro.intro.intro
S R : CommRingCat
f : R ⟶ S
inst✝¹ : FormallyUnramified (Spec.map f)
inst✝ : LocallyOfFiniteType (Spec.map f)
⊢ IsOpenImmersion (pullback.diagonal (Spec.map f))

Tactic:
rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified),
  HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)] at *

Result:
case intro.intro.intro.intro
S R : CommRingCat
f : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom f).FormallyUnramified
inst✝ : (CommRingCat.Hom.hom f).FiniteType
⊢ IsOpenImmersion (pullback.diagonal (Spec.map f))