-- Mathlib/AlgebraicGeometry/Stalk.lean
/-- useful lemma for applications of `SpecToEquivOfLocalRing` -/
lemma SpecToEquivOfLocalRing_eq_iff
    {f₁ f₂ : Σ x, { f : X.presheaf.stalk x ⟶ R // IsLocalHom f.hom }} :
    f₁ = f₂ ↔ ∃ h₁ : f₁.1 = f₂.1, f₁.2.1 =
      (X.presheaf.stalkCongr (by rw [h₁]; rfl)).hom ≫ f₂.2.1

Proof state:
X Y : Scheme
f : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
h₁ : f₁.fst = f₂.fst
⊢ Inseparable f₂.fst f₂.fst

Tactic:
rfl

Result:
no goals

Proof state:
case mp
X : Scheme
R : CommRingCat
f₁ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ ∃ (h₁ : f₁.fst = f₁.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₁.snd

Tactic:
simp

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
h₁ : f₁.fst = f₂.fst
⊢ Inseparable f₁.fst f₂.fst

Tactic:
rw [h₁]

Result:
X Y : Scheme
f : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
h₁ : f₁.fst = f₂.fst
⊢ Inseparable f₂.fst f₂.fst

Proof state:
case mpr.mk.mk.mk.mk.intro
X : Scheme
R : CommRingCat
x₁ : ↑↑X.toPresheafedSpace
f₁ : X.presheaf.stalk x₁ ⟶ R
h₁ : IsLocalHom (CommRingCat.Hom.hom f₁)
f₂ : X.presheaf.stalk x₁ ⟶ R
h₂ : IsLocalHom (CommRingCat.Hom.hom f₂)
e : f₁ = (X.presheaf.stalkCongr ⋯).hom ≫ ↑⟨x₁, ⟨f₂, h₂⟩⟩.snd
⊢ ⟨x₁, ⟨f₁, h₁⟩⟩ = ⟨x₁, ⟨f₂, h₂⟩⟩

Tactic:
simp [e]

Result:
no goals

Proof state:
X : Scheme
R : CommRingCat
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ f₁ = f₂ ↔ ∃ (h₁ : f₁.fst = f₂.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₂.snd

Tactic:
constructor

Result:
case mp
X : Scheme
R : CommRingCat
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ f₁ = f₂ → ∃ (h₁ : f₁.fst = f₂.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₂.snd

case mpr
X : Scheme
R : CommRingCat
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ (∃ (h₁ : f₁.fst = f₂.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₂.snd) → f₁ = f₂

Proof state:
case mp
X : Scheme
R : CommRingCat
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ f₁ = f₂ → ∃ (h₁ : f₁.fst = f₂.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₂.snd

Tactic:
rintro rfl

Result:
case mp
X : Scheme
R : CommRingCat
f₁ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ ∃ (h₁ : f₁.fst = f₁.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₁.snd

Proof state:
case mpr.mk.mk.mk.mk
X : Scheme
R : CommRingCat
x₁ : ↑↑X.toPresheafedSpace
f₁ : X.presheaf.stalk x₁ ⟶ R
h₁ : IsLocalHom (CommRingCat.Hom.hom f₁)
x₂ : ↑↑X.toPresheafedSpace
f₂ : X.presheaf.stalk x₂ ⟶ R
h₂ : IsLocalHom (CommRingCat.Hom.hom f₂)
⊢ (∃ (h₁_1 : ⟨x₁, ⟨f₁, h₁⟩⟩.fst = ⟨x₂, ⟨f₂, h₂⟩⟩.fst),
      ↑⟨x₁, ⟨f₁, h₁⟩⟩.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑⟨x₂, ⟨f₂, h₂⟩⟩.snd) →
    ⟨x₁, ⟨f₁, h₁⟩⟩ = ⟨x₂, ⟨f₂, h₂⟩⟩

Tactic:
rintro ⟨rfl : x₁ = x₂, e : f₁ = _⟩

Result:
case mpr.mk.mk.mk.mk.intro
X : Scheme
R : CommRingCat
x₁ : ↑↑X.toPresheafedSpace
f₁ : X.presheaf.stalk x₁ ⟶ R
h₁ : IsLocalHom (CommRingCat.Hom.hom f₁)
f₂ : X.presheaf.stalk x₁ ⟶ R
h₂ : IsLocalHom (CommRingCat.Hom.hom f₂)
e : f₁ = (X.presheaf.stalkCongr ⋯).hom ≫ ↑⟨x₁, ⟨f₂, h₂⟩⟩.snd
⊢ ⟨x₁, ⟨f₁, h₁⟩⟩ = ⟨x₁, ⟨f₂, h₂⟩⟩

Proof state:
case mpr.mk.mk
X : Scheme
R : CommRingCat
f₂ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
x₁ : ↑↑X.toPresheafedSpace
f₁ : X.presheaf.stalk x₁ ⟶ R
h₁ : IsLocalHom (CommRingCat.Hom.hom f₁)
⊢ (∃ (h₁_1 : ⟨x₁, ⟨f₁, h₁⟩⟩.fst = f₂.fst), ↑⟨x₁, ⟨f₁, h₁⟩⟩.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₂.snd) →
    ⟨x₁, ⟨f₁, h₁⟩⟩ = f₂

Tactic:
obtain ⟨x₂, ⟨f₂, h₂⟩⟩ := f₂

Result:
case mpr.mk.mk.mk.mk
X : Scheme
R : CommRingCat
x₁ : ↑↑X.toPresheafedSpace
f₁ : X.presheaf.stalk x₁ ⟶ R
h₁ : IsLocalHom (CommRingCat.Hom.hom f₁)
x₂ : ↑↑X.toPresheafedSpace
f₂ : X.presheaf.stalk x₂ ⟶ R
h₂ : IsLocalHom (CommRingCat.Hom.hom f₂)
⊢ (∃ (h₁_1 : ⟨x₁, ⟨f₁, h₁⟩⟩.fst = ⟨x₂, ⟨f₂, h₂⟩⟩.fst),
      ↑⟨x₁, ⟨f₁, h₁⟩⟩.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑⟨x₂, ⟨f₂, h₂⟩⟩.snd) →
    ⟨x₁, ⟨f₁, h₁⟩⟩ = ⟨x₂, ⟨f₂, h₂⟩⟩

Proof state:
case mpr
X : Scheme
R : CommRingCat
f₁ f₂ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ (∃ (h₁ : f₁.fst = f₂.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₂.snd) → f₁ = f₂

Tactic:
obtain ⟨x₁, ⟨f₁, h₁⟩⟩ := f₁

Result:
case mpr.mk.mk
X : Scheme
R : CommRingCat
f₂ : (x : ↑↑X.toPresheafedSpace) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
x₁ : ↑↑X.toPresheafedSpace
f₁ : X.presheaf.stalk x₁ ⟶ R
h₁ : IsLocalHom (CommRingCat.Hom.hom f₁)
⊢ (∃ (h₁_1 : ⟨x₁, ⟨f₁, h₁⟩⟩.fst = f₂.fst), ↑⟨x₁, ⟨f₁, h₁⟩⟩.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₂.snd) →
    ⟨x₁, ⟨f₁, h₁⟩⟩ = f₂