-- Mathlib/AlgebraicGeometry/Morphisms/UniversallyInjective.lean
theorem universallyInjective_eq_diagonal :
    @UniversallyInjective = diagonal @Surjective

Proof state:
case a.a

⊢ diagonal @Surjective ≤ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x => Function.Injective x

Tactic:
intro X Y f hf x₁ x₂ e

Result:
case a.a
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↑↑X.toPresheafedSpace
e : (ConcreteCategory.hom f.base) x₁ = (ConcreteCategory.hom f.base) x₂
⊢ x₁ = x₂

Proof state:
case a.a
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↑↑X.toPresheafedSpace
e : (ConcreteCategory.hom f.base) x₁ = (ConcreteCategory.hom f.base) x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := Scheme.Pullback.exists_preimage_pullback _ _ e

Result:
case a.a.intro.intro
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↑↑X.toPresheafedSpace
e : (ConcreteCategory.hom f.base) x₁ = (ConcreteCategory.hom f.base) x₂
t : ↑↑(pullback f f).toPresheafedSpace
ht₁ : (ConcreteCategory.hom (pullback.fst f f).base) t = x₁
ht₂ : (ConcreteCategory.hom (pullback.snd f f).base) t = x₂
⊢ x₁ = x₂

Proof state:
case a.a.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↑↑X.toPresheafedSpace
e : (ConcreteCategory.hom f.base) x₁ = (ConcreteCategory.hom f.base) x₂
t : ↑↑X.toPresheafedSpace
ht₁ : (ConcreteCategory.hom (pullback.fst f f).base) ((ConcreteCategory.hom (pullback.diagonal f).base) t) = x₁
ht₂ : (ConcreteCategory.hom (pullback.snd f f).base) ((ConcreteCategory.hom (pullback.diagonal f).base) t) = x₂
⊢ x₁ = x₂

Tactic:
rw [← ht₁, ← ht₂, ← Scheme.comp_base_apply, ← Scheme.comp_base_apply, pullback.diagonal_fst,
  pullback.diagonal_snd]

Result:
no goals

Proof state:
case a.a.intro.intro
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↑↑X.toPresheafedSpace
e : (ConcreteCategory.hom f.base) x₁ = (ConcreteCategory.hom f.base) x₂
t : ↑↑(pullback f f).toPresheafedSpace
ht₁ : (ConcreteCategory.hom (pullback.fst f f).base) t = x₁
ht₂ : (ConcreteCategory.hom (pullback.snd f f).base) t = x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨t, rfl⟩ := hf.1 t

Result:
case a.a.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↑↑X.toPresheafedSpace
e : (ConcreteCategory.hom f.base) x₁ = (ConcreteCategory.hom f.base) x₂
t : ↑↑X.toPresheafedSpace
ht₁ : (ConcreteCategory.hom (pullback.fst f f).base) ((ConcreteCategory.hom (pullback.diagonal f).base) t) = x₁
ht₂ : (ConcreteCategory.hom (pullback.snd f f).base) ((ConcreteCategory.hom (pullback.diagonal f).base) t) = x₂
⊢ x₁ = x₂

Proof state:
⊢ @UniversallyInjective = diagonal @Surjective

Tactic:
apply le_antisymm

Result:
case a

⊢ @UniversallyInjective ≤ diagonal @Surjective

case a

⊢ diagonal @Surjective ≤ @UniversallyInjective

Proof state:
case a

⊢ @UniversallyInjective ≤ diagonal @Surjective

Tactic:
intro X Y f hf

Result:
case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
⊢ diagonal (@Surjective) f

Proof state:
case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
⊢ (ConcreteCategory.hom (𝟙 X).base) ((ConcreteCategory.hom (pullback.fst f f).base) x) =
    (ConcreteCategory.hom (pullback.fst f f).base) x

Tactic:
rfl

Result:
no goals

Proof state:
case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.fst f f).base)
      ((ConcreteCategory.hom (pullback.diagonal f).base) ((ConcreteCategory.hom (pullback.fst f f).base) x)) =
    (ConcreteCategory.hom (pullback.fst f f).base) x

Tactic:
rw [← Scheme.comp_base_apply, pullback.diagonal_fst]

Result:
case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
⊢ (ConcreteCategory.hom (𝟙 X).base) ((ConcreteCategory.hom (pullback.fst f f).base) x) =
    (ConcreteCategory.hom (pullback.fst f f).base) x

Proof state:
case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
⊢ diagonal (@Surjective) f

Tactic:
refine ⟨fun x ↦ ⟨(pullback.fst f f).base x, hf.1 _ _ _ (IsPullback.of_hasPullback f f) ?_⟩⟩

Result:
case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
x : ↑↑(pullback.diagonalObj f).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.fst f f).base)
      ((ConcreteCategory.hom (pullback.diagonal f).base) ((ConcreteCategory.hom (pullback.fst f f).base) x)) =
    (ConcreteCategory.hom (pullback.fst f f).base) x

Proof state:
case a

⊢ diagonal @Surjective ≤ @UniversallyInjective

Tactic:
rw [← universally_eq_iff.mpr (inferInstanceAs (IsStableUnderBaseChange (diagonal @Surjective))),
  universallyInjective_eq]

Result:
case a

⊢ (diagonal @Surjective).universally ≤
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x => Function.Injective x).universally

Proof state:
case a

⊢ (diagonal @Surjective).universally ≤
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x => Function.Injective x).universally

Tactic:
apply universally_mono

Result:
case a.a

⊢ diagonal @Surjective ≤ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x => Function.Injective x