-- 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)
𝒰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))
hfin : LocallyOfFiniteType ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i))
⊢ IsOpenImmersion (pullback.diagonal ((𝒰X i).map j ≫ pullback.snd f (𝒰Y.map i)))

Tactic:
exact this _ ⟨⟨_, rfl⟩, ⟨_, rfl⟩⟩

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
⊢ IsOpenImmersion (pullback.diagonal f)

Tactic:
wlog hX : (∃ S, X = Spec S) ∧ ∃ R, Y = Spec R

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)
⊢ IsOpenImmersion (pullback.diagonal f)

X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
hX : (∃ S, X = Spec S) ∧ ∃ R, Y = Spec R
⊢ 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)
𝒰Y : Y.OpenCover := Y.affineCover
⊢ IsOpenImmersion (pullback.diagonal f)

Tactic:
let 𝒰X (j : (Y.affineCover.pullbackCover f).J) :
    ((Y.affineCover.pullbackCover f).obj j).OpenCover := Scheme.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
𝒰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)

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 f ∣_
      Scheme.Hom.opensRange ((Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).map ⟨⟨i, j⟩.fst, (⟨i, j⟩.snd, ⟨i, j⟩.snd)⟩))

Tactic:
rw [arrow_mk_iso_iff (P := @IsOpenImmersion)
  (Scheme.Pullback.diagonalRestrictIsoDiagonal f 𝒰Y 𝒰X i j)]

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
⊢ 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
⊢ ∀ (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)⟩))

Tactic:
intro ⟨i, j⟩

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
⊢ IsOpenImmersion
    (pullback.diagonal f ∣_
      Scheme.Hom.opensRange ((Scheme.Pullback.diagonalCover f 𝒰Y 𝒰X).map ⟨⟨i, j⟩.fst, (⟨i, j⟩.snd, ⟨i, j⟩.snd)⟩))

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
hX : (∃ S, X = Spec S) ∧ ∃ R, Y = Spec R
⊢ IsOpenImmersion (pullback.diagonal f)

Tactic:
obtain ⟨⟨S, rfl⟩, R, rfl⟩ := hX

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